diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-08-03 20:50:11 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-08-03 20:50:11 +0000 |
| commit | f9f35dc36f5249a2de18005ab59ae934e0fa7075 (patch) | |
| tree | 4d3dd839db319df1945c8fef474284e6f4e5f3e3 /parsing | |
| parent | 25dde2366a4db47e5da13b2bbe4d03a31235706f (diff) | |
Added "etransitivity".
Added support for "injection" and "discriminate" on JMeq.
Seized the opportunity to update coqlib.ml and to rely more on it for
finding the equality lemmas.
Fixed typos in coqcompat.ml.
Propagated symmetry convert_concl fix to transitivity (see 11521).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12259 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_tactic.ml4 | 3 | ||||
| -rw-r--r-- | parsing/pptactic.ml | 3 | ||||
| -rw-r--r-- | parsing/q_coqast.ml4 | 2 |
3 files changed, 5 insertions, 3 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index c0a3f2e77..d5d32ce5b 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -616,7 +616,8 @@ GEXTEND Gram (* Equivalence relations *) | IDENT "reflexivity" -> TacReflexivity | IDENT "symmetry"; cl = clause_dft_concl -> TacSymmetry cl - | IDENT "transitivity"; c = constr -> TacTransitivity c + | IDENT "transitivity"; c = constr -> TacTransitivity (Some c) + | IDENT "etransitivity" -> TacTransitivity None (* Equality and inversion *) | IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ","; diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 357a572be..bdd9241e3 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -844,7 +844,8 @@ and pr_atom1 = function (* Equivalence relations *) | TacReflexivity as x -> pr_atom0 x | TacSymmetry cls -> str "symmetry " ++ pr_clauses pr_ident cls - | TacTransitivity c -> str "transitivity" ++ pr_constrarg c + | TacTransitivity (Some c) -> str "transitivity" ++ pr_constrarg c + | TacTransitivity None -> str "etransitivity" (* Equality and inversion *) | TacRewrite (ev,l,cl,by) -> diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index a494738f9..606b652c2 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -413,7 +413,7 @@ let rec mlexpr_of_atomic_tactic = function (* Equivalence relations *) | Tacexpr.TacReflexivity -> <:expr< Tacexpr.TacReflexivity >> | Tacexpr.TacSymmetry ido -> <:expr< Tacexpr.TacSymmetry $mlexpr_of_clause ido$ >> - | Tacexpr.TacTransitivity c -> <:expr< Tacexpr.TacTransitivity $mlexpr_of_constr c$ >> + | Tacexpr.TacTransitivity c -> <:expr< Tacexpr.TacTransitivity $mlexpr_of_option mlexpr_of_constr c$ >> (* Automation tactics *) | Tacexpr.TacAuto (n,lems,l) -> |