diff options
| author | Arnaud Spiwack | 2013-11-26 11:53:09 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2013-12-04 14:14:32 +0100 |
| commit | db65876404c7c3a1343623cc9b4d6c2a7164dd95 (patch) | |
| tree | 2f73652c1014775aa0fc171f9a64a8807ede7ac5 /tactics | |
| parent | eef907ed0a200e912ab2eddc0fcea41b5f61c145 (diff) | |
Vernac classification: allow for commands which start proofs but must be synchrone.
The previous heuristic is to check whether the proof ends with Qed or not. This modification allows for commands which start proof but may produce transparent term even when the function ends with Qed.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/g_rewrite.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/g_rewrite.ml4 b/tactics/g_rewrite.ml4 index 846bba1d46..31defcafb3 100644 --- a/tactics/g_rewrite.ml4 +++ b/tactics/g_rewrite.ml4 @@ -244,11 +244,11 @@ VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF => [ Vernacexpr.VtUnknown, Vernacexpr.VtNow ] -> [ add_morphism_infer (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) m n ] | [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] - => [ Vernacexpr.VtStartProof("Classic",[n]), Vernacexpr.VtLater ] + => [ Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) ] -> [ add_morphism (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) [] m s n ] | [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] - => [ Vernacexpr.VtStartProof("Classic",[n]), Vernacexpr.VtLater ] + => [ Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) ] -> [ add_morphism (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) binders m s n ] END |