From 11bf7edb003eda8f8f5f0adcd215e7eeb9d80303 Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 7 Mar 2008 23:52:56 +0000 Subject: f_equal, revert, specialize in ML, contradict in better Ltac (+doc) * "f_equal" is now a tactic in ML (placed alongside congruence since it uses it). Normally, it should be completely compatible with the former Ltac version, except that it doesn't suffer anymore from the "up to 5 args" earlier limitation. * "revert" also becomes an ML tactic. This doesn't bring any real improvement, just some more uniformity with clear and generalize. * The experimental "narrow" tactic is removed from Tactics.v, and replaced by an evolution of the old & undocumented "specialize" ML tactic: - when specialize is called on an hyp H, the specialization is now done in place on H. For instance "specialize (H t u v)" removes the three leading forall of H and intantiates them by t u and v. - otherwise specialize still works as before (i.e. as a kind of generalize). See the RefMan and test-suite/accept/specialize.v for more infos. Btw, specialize can still accept an optional number for specifying how many premises to instantiate. This number should normally be useless now (some autodetection mecanism added). Hence this feature is left undocumented. For the happy few still using specialize in the old manner, beware of the slight incompatibities... * finally, "contradict" is left as Ltac in Tactics.v, but it has now a better shape (accepts unfolded nots and/or things in Type), and also some documentation in the RefMan git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10637 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/interface/depends.ml | 3 ++- contrib/interface/xlate.ml | 2 ++ 2 files changed, 4 insertions(+), 1 deletion(-) (limited to 'contrib/interface') diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml index a0cbe22b36..16357fc472 100644 --- a/contrib/interface/depends.ml +++ b/contrib/interface/depends.ml @@ -340,7 +340,8 @@ let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of | TacClear _ | TacClearBody _ | TacMove _ - | TacRename _ -> acc + | TacRename _ + | TacRevert _ -> acc (* Constructors *) | TacLeft cb diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index c5a8c756a8..2219e327ca 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1187,6 +1187,7 @@ and xlate_tac = let idl' = List.map xlate_hyp idl in CT_clear (CT_id_ne_list (xlate_hyp id, idl')) | TacClear (true,_) -> xlate_error "TODO: 'clear - idl' and 'clear'" + | TacRevert _ -> xlate_error "TODO: revert" | (*For translating tactics/Inv.v *) TacInversion (NonDepInversion (k,idl,l),quant_hyp) -> CT_inversion(compute_INV_TYPE k, xlate_quantified_hypothesis quant_hyp, @@ -1248,6 +1249,7 @@ and xlate_tac = (CT_formula_list (List.map xlate_formula (out_gen (wit_list0 rawwit_constr) args))) + | TacExtend (_, "f_equal", _) -> xlate_error "TODO: f_equal" | TacExtend (_,id, l) -> print_endline ("Extratactics : "^ id); CT_user_tac (CT_ident id, CT_targ_list (List.map coerce_genarg_to_TARG l)) -- cgit v1.2.3