diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/field/field.ml4 | 10 | ||||
| -rw-r--r-- | plugins/interface/depends.ml | 3 | ||||
| -rw-r--r-- | plugins/interface/xlate.ml | 3 | ||||
| -rw-r--r-- | plugins/ring/ring.ml | 20 |
4 files changed, 21 insertions, 15 deletions
diff --git a/plugins/field/field.ml4 b/plugins/field/field.ml4 index 93de6118b6..c9b993690f 100644 --- a/plugins/field/field.ml4 +++ b/plugins/field/field.ml4 @@ -154,10 +154,12 @@ END (* Guesses the type and calls field_gen with the right theory *) let field g = Coqlib.check_required_library ["Coq";"field";"LegacyField"]; - let typ = - match Hipattern.match_with_equation (pf_concl g) with - | Some (eq,t::args) when eq = (Coqlib.build_coq_eq_data()).Coqlib.eq -> t - | _ -> error "The statement is not built from Leibniz' equality" in + let typ = + try match Hipattern.match_with_equation (pf_concl g) with + | _,_,Hipattern.PolymorphicLeibnizEq (t,_,_) -> t + | _ -> raise Exit + with Hipattern.NoEquationFound | Exit -> + error "The statement is not built from Leibniz' equality" in let th = VConstr (lookup (pf_env g) typ) in (interp_tac_gen [(id_of_string "FT",th)] [] (get_debug ()) <:tactic< match goal with |- (@eq _ _ _) => field_gen FT end >>) g 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) diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml index adcf51fe85..6dcc1e8725 100644 --- a/plugins/ring/ring.ml +++ b/plugins/ring/ring.ml @@ -892,16 +892,18 @@ let polynom lc gl = do "Ring c1 c2 ... cn" and then try to apply the simplification theorems declared for the relation *) | [] -> - (match Hipattern.match_with_equation (pf_concl gl) with - | Some (eq,t::args) -> + (try + match Hipattern.match_with_equation (pf_concl gl) with + | _,_,Hipattern.PolymorphicLeibnizEq (t,c1,c2) -> let th = guess_theory t in - if List.exists - (fun c1 -> not (safe_pf_conv_x gl t (pf_type_of gl c1))) args - then - errorlabstrm "Ring :" - (str" All terms must have the same type"); - (tclTHEN (raw_polynom th None args) (guess_eq_tac th)) gl - | _ -> (match match_with_equiv (pf_concl gl) with + (tclTHEN (raw_polynom th None [c1;c2]) (guess_eq_tac th)) gl + | _,_,Hipattern.HeterogenousEq (t1,c1,t2,c2) + when safe_pf_conv_x gl t1 t2 -> + let th = guess_theory t1 in + (tclTHEN (raw_polynom th None [c1;c2]) (guess_eq_tac th)) gl + | _ -> raise Exit + with Hipattern.NoEquationFound | Exit -> + (match match_with_equiv (pf_concl gl) with | Some (equiv, c1::args) -> let t = (pf_type_of gl c1) in let th = (guess_theory t) in |