diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml4 | 32 |
1 files changed, 17 insertions, 15 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index e051d1aad..33bc17624 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -71,6 +71,8 @@ let e_give_exact flags c gl = if occur_existential t1 or occur_existential t2 then tclTHEN (Clenvtac.unify (* ~flags *) t1) (exact_check c) gl else exact_check c gl +(* let t1 = (pf_type_of gl c) in *) +(* tclTHEN (Clenvtac.unify ~flags t1) (exact_check c) gl *) let assumption flags id = e_give_exact flags (mkVar id) @@ -1242,7 +1244,7 @@ let declare_an_instance n s args = let declare_instance a aeq n s = declare_an_instance n s [a;aeq] let anew_instance binders instance fields = - new_instance binders instance fields ~generalize:false None + new_instance binders instance (CRecord (dummy_loc,None,fields)) ~generalize:false None let require_library dirpath = let qualid = (dummy_loc, Libnames.qualid_of_dirpath (Libnames.dirpath_of_string dirpath)) in @@ -1251,17 +1253,17 @@ let require_library dirpath = let declare_instance_refl binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive" in anew_instance binders instance - [((dummy_loc,id_of_string "reflexivity"),[],lemma)] + [((dummy_loc,id_of_string "reflexivity"),lemma)] let declare_instance_sym binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Symmetric") "Coq.Classes.RelationClasses.Symmetric" in anew_instance binders instance - [((dummy_loc,id_of_string "symmetry"),[],lemma)] + [((dummy_loc,id_of_string "symmetry"),lemma)] let declare_instance_trans binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Transitive") "Coq.Classes.RelationClasses.Transitive" in anew_instance binders instance - [((dummy_loc,id_of_string "transitivity"),[],lemma)] + [((dummy_loc,id_of_string "transitivity"),lemma)] let constr_tac = Tacinterp.interp (Tacexpr.TacAtom (dummy_loc, Tacexpr.TacAnyConstructor (false,None))) @@ -1286,16 +1288,16 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans = let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder" in ignore( anew_instance binders instance - [((dummy_loc,id_of_string "PreOrder_Reflexive"), [], lemma1); - ((dummy_loc,id_of_string "PreOrder_Transitive"),[], lemma3)]) + [((dummy_loc,id_of_string "PreOrder_Reflexive"), lemma1); + ((dummy_loc,id_of_string "PreOrder_Transitive"),lemma3)]) | (None, Some lemma2, Some lemma3) -> let _lemma_sym = declare_instance_sym binders a aeq n lemma2 in let _lemma_trans = declare_instance_trans binders a aeq n lemma3 in let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER" in ignore( anew_instance binders instance - [((dummy_loc,id_of_string "PER_Symmetric"), [], lemma2); - ((dummy_loc,id_of_string "PER_Transitive"),[], lemma3)]) + [((dummy_loc,id_of_string "PER_Symmetric"), lemma2); + ((dummy_loc,id_of_string "PER_Transitive"),lemma3)]) | (Some lemma1, Some lemma2, Some lemma3) -> let _lemma_refl = declare_instance_refl binders a aeq n lemma1 in let _lemma_sym = declare_instance_sym binders a aeq n lemma2 in @@ -1303,9 +1305,9 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans = let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in ignore( anew_instance binders instance - [((dummy_loc,id_of_string "Equivalence_Reflexive"), [], lemma1); - ((dummy_loc,id_of_string "Equivalence_Symmetric"), [], lemma2); - ((dummy_loc,id_of_string "Equivalence_Transitive"),[], lemma3)]) + [((dummy_loc,id_of_string "Equivalence_Reflexive"), lemma1); + ((dummy_loc,id_of_string "Equivalence_Symmetric"), lemma2); + ((dummy_loc,id_of_string "Equivalence_Transitive"), lemma3)]) type 'a binders_let_argtype = (local_binder list, 'a) Genarg.abstract_argument_type @@ -1483,9 +1485,9 @@ let add_setoid binders a aeq t n = let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in ignore( anew_instance binders instance - [((dummy_loc,id_of_string "Equivalence_Reflexive"), [], mkappc "Seq_refl" [a;aeq;t]); - ((dummy_loc,id_of_string "Equivalence_Symmetric"), [], mkappc "Seq_sym" [a;aeq;t]); - ((dummy_loc,id_of_string "Equivalence_Transitive"),[], mkappc "Seq_trans" [a;aeq;t])]) + [((dummy_loc,id_of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]); + ((dummy_loc,id_of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]); + ((dummy_loc,id_of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])]) let add_morphism_infer m n = init_setoid (); @@ -1520,7 +1522,7 @@ let add_morphism binders m s n = [cHole; s; m])) in let tac = Tacinterp.interp <:tactic<add_morphism_tactic>> in - ignore(new_instance binders instance [] + ignore(new_instance binders instance (CRecord (dummy_loc,None,[])) ~generalize:false ~tac ~hook:(fun cst -> declare_projection n instance_id (ConstRef cst)) None) |