search

math-comp / math-comp

Mathematical Components
https://math-comp.github.io
573 stars 112 forks source link

Error when factorising code on subgoals #45

Open thery opened 8 years ago

thery commented 8 years ago

On 8.5 ssreflect 1.5 this works:

From mathcomp Require Import all_ssreflect. Goal forall n : nat, [|| n == 1, n == 2 | n ==3] -> n < 4. by move=> n /or3P[] /eqP ->.

but this fails

Goal forall n : nat, [|| n == 1, n == 2 | n ==3] -> n < 4. move=> n H. have /or3P[] /eqP-> := H.

with

Anomaly: The global environment cannot be accessed during parsing. Please report.

gares commented 8 years ago

Thanks for reporting the issue!

ggonthier commented 8 years ago

The have should fail, because you are allowed only a single intro pattern (with clear & views before and simpl switches after) in a have, as additional identifiers are interpreted as introduced variables (you can get around this limitation by using a /wrap view). The error message is nevertheless obviously wrong.

Thanks, Georges

From: Laurent Théry [mailto:notifications@github.com] Sent: 17 May 2016 15:18 To: math-comp/math-comp math-comp@noreply.github.com Subject: [math-comp/math-comp] Error when factorising code on subgoals (#45)

On 8.5 ssreflect 1.5 this works:

From mathcomp Require Import all_ssreflect. Goal forall n : nat, [|| n == 1, n == 2 | n ==3] -> n < 4. by move=> n /or3P[] /eqP ->.

but this fails

Goal forall n : nat, [|| n == 1, n == 2 | n ==3] -> n < 4. move=> n H. have /or3P[] /eqP-> := H.

with

Anomaly: The global environment cannot be accessed during parsing. Please report.

— You are receiving this because you are subscribed to this thread. Reply to this email directly or view it on GitHubhttps://github.com/math-comp/math-comp/issues/45

CohenCyril commented 2 years ago

Find the right error message to display and move to Coq @gares