diff options
Diffstat (limited to 'tactics')
-rw-r--r-- | tactics/hiddentac.ml | 2 | ||||
-rw-r--r-- | tactics/hiddentac.mli | 2 | ||||
-rw-r--r-- | tactics/tacinterp.ml | 7 | ||||
-rw-r--r-- | tactics/tactics.ml | 21 | ||||
-rw-r--r-- | tactics/tactics.mli | 3 |
5 files changed, 28 insertions, 7 deletions
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index 9024123f3..0e8725c6a 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -87,7 +87,7 @@ let h_change oc c cl = abstract_tactic (TacChange (oc,c,cl)) (change oc c cl) (* Equivalence relations *) let h_reflexivity = abstract_tactic TacReflexivity intros_reflexivity -let h_symmetry = abstract_tactic TacSymmetry intros_symmetry +let h_symmetry c = abstract_tactic (TacSymmetry c) (intros_symmetry c) let h_transitivity c = abstract_tactic (TacTransitivity c) (intros_transitivity c) diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index c01eca7f2..dba9908a9 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -95,7 +95,7 @@ val h_change : (* Equivalence relations *) val h_reflexivity : tactic -val h_symmetry : tactic +val h_symmetry : Tacticals.clause -> tactic val h_transitivity : constr -> tactic val h_simplest_apply : constr -> tactic diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index f92eefff0..84d8d84ac 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -623,7 +623,8 @@ let rec intern_atomic lf ist x = (* Equivalence relations *) | TacReflexivity -> TacReflexivity - | TacSymmetry -> TacSymmetry + | TacSymmetry idopt -> + TacSymmetry (option_app (intern_hyp_or_metaid ist) idopt) | TacTransitivity c -> TacTransitivity (intern_constr ist c) (* For extensions *) @@ -1644,7 +1645,7 @@ and interp_atomic ist gl = function (* Equivalence relations *) | TacReflexivity -> h_reflexivity - | TacSymmetry -> h_symmetry + | TacSymmetry c -> h_symmetry (option_app (interp_hyp ist gl) c) | TacTransitivity c -> h_transitivity (pf_interp_constr ist gl c) (* For extensions *) @@ -1848,7 +1849,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with subst_rawconstr subst c, cl) (* Equivalence relations *) - | TacReflexivity | TacSymmetry as x -> x + | TacReflexivity | TacSymmetry _ as x -> x | TacTransitivity c -> TacTransitivity (subst_rawconstr subst c) (* For extensions *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 126e61ec2..1b9f86023 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1606,7 +1606,26 @@ let symmetry gl = gl end -let intros_symmetry = (tclTHEN intros symmetry) +let symmetry_in id gl = + let ctype = pf_type_of gl (mkVar id) in + let sign,t = decompose_prod_assum ctype in + match match_with_equation t with + | None -> (* Do not deal with setoids yet *) + error "The term provided does not end with an equation" + | Some (hdcncl,args) -> + let symccl = match args with + | [t1; c1; t2; c2] -> mkApp (hdcncl, [| t2; c2; t1; c1 |]) + | [typ;c1;c2] -> mkApp (hdcncl, [| typ; c2; c1 |]) + | [c1;c2] -> mkApp (hdcncl, [| c2; c1 |]) + | _ -> assert false in + tclTHENS (cut (it_mkProd_or_LetIn symccl sign)) + [ intro_replacing id; + tclTHENLIST [ intros; symmetry; apply (mkVar id); assumption ] ] + gl + +let intros_symmetry = function + | None -> tclTHEN intros symmetry + | Some id -> symmetry_in id (* Transitivity tactics *) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 5ff744e3f..38c31f015 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -222,7 +222,8 @@ val reflexivity : tactic val intros_reflexivity : tactic val symmetry : tactic -val intros_symmetry : tactic +val symmetry_in : identifier -> tactic +val intros_symmetry : clause -> tactic val transitivity : constr -> tactic val intros_transitivity : constr -> tactic |