diff options
| author | herbelin | 2009-08-03 20:50:11 +0000 |
|---|---|---|
| committer | herbelin | 2009-08-03 20:50:11 +0000 |
| commit | f9f35dc36f5249a2de18005ab59ae934e0fa7075 (patch) | |
| tree | 4d3dd839db319df1945c8fef474284e6f4e5f3e3 /plugins/interface | |
| 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 'plugins/interface')
| -rw-r--r-- | plugins/interface/depends.ml | 3 | ||||
| -rw-r--r-- | plugins/interface/xlate.ml | 3 |
2 files changed, 4 insertions, 2 deletions
diff --git a/plugins/interface/depends.ml b/plugins/interface/depends.ml index 445b193f81..9e649a5a2f 100644 --- a/plugins/interface/depends.ml +++ b/plugins/interface/depends.ml @@ -357,7 +357,8 @@ let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of (* Equivalence relations *) | TacReflexivity | TacSymmetry _ -> acc - | TacTransitivity c -> depends_of_'constr c acc + | TacTransitivity (Some c) -> depends_of_'constr c acc + | TacTransitivity None -> acc (* Equality and inversion *) | TacRewrite (_,cbl,_,_) -> list_union_map (o depends_of_'constr_with_bindings (fun (_,_,x)->x)) cbl acc diff --git a/plugins/interface/xlate.ml b/plugins/interface/xlate.ml index bff8cae260..9629fa923c 100644 --- a/plugins/interface/xlate.ml +++ b/plugins/interface/xlate.ml @@ -1066,7 +1066,8 @@ and xlate_tac = (out_gen (wit_list1 rawwit_ident) l))) | TacReflexivity -> CT_reflexivity | TacSymmetry cls -> CT_symmetry(xlate_clause cls) - | TacTransitivity c -> CT_transitivity (xlate_formula c) + | TacTransitivity (Some c) -> CT_transitivity (xlate_formula c) + | TacTransitivity None -> xlate_error "TODO: etransitivity" | TacAssumption -> CT_assumption | TacExact c -> CT_exact (xlate_formula c) | TacExactNoCheck c -> CT_exact_no_check (xlate_formula c) |