diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 5 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 18 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 25 |
3 files changed, 33 insertions, 15 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index fedf91d534..4ac300827e 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -305,7 +305,10 @@ let subst_autohint (_,subst,(local,name,hintlist as obj)) = } in let subst_hint (lab,data as hint) = - let lab' = subst_global subst lab in + let lab',elab' = subst_global subst lab in + let lab' = + try head_of_constr_reference (List.hd (head_constr_bound elab' [])) + with Tactics.Bound -> lab' in let data' = match data.code with | Res_pf (c, clenv) -> let c' = subst_mps subst c in diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index edf99f175d..4068289eb9 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -14,6 +14,7 @@ open Pp open Pcoq open Genarg open Extraargs +open Mod_subst (* Equality *) open Equality @@ -348,7 +349,7 @@ let step left x tac = let l = List.map (fun lem -> tclTHENLAST - (apply_with_bindings (constr_of_reference lem, ImplicitBindings [x])) + (apply_with_bindings (lem, ImplicitBindings [x])) tac) !(if left then transitivity_left_table else transitivity_right_table) in @@ -362,7 +363,7 @@ let cache_transitivity_lemma (_,(left,lem)) = else transitivity_right_table := lem :: !transitivity_right_table -let subst_transitivity_lemma (_,subst,(b,ref)) = (b,subst_global subst ref) +let subst_transitivity_lemma (_,subst,(b,ref)) = (b,subst_mps subst ref) let (inTransitivity,_) = declare_object {(default_object "TRANSITIVITY-STEPS") with @@ -394,8 +395,9 @@ let _ = (* Main entry points *) -let add_transitivity_lemma left ref = - add_anonymous_leaf (inTransitivity (left,Nametab.global ref)) +let add_transitivity_lemma left lem = + let lem' = Constrintern.interp_constr Evd.empty (Global.env ()) lem in + add_anonymous_leaf (inTransitivity (left,lem')) (* Vernacular syntax *) @@ -410,11 +412,11 @@ TACTIC EXTEND Stepr END VERNAC COMMAND EXTEND AddStepl -| [ "Declare" "Left" "Step" global(id) ] -> - [ add_transitivity_lemma true id ] +| [ "Declare" "Left" "Step" constr(t) ] -> + [ add_transitivity_lemma true t ] END VERNAC COMMAND EXTEND AddStepr -| [ "Declare" "Right" "Step" global(id) ] -> - [ add_transitivity_lemma false id ] +| [ "Declare" "Right" "Step" constr(t) ] -> + [ add_transitivity_lemma false t ] END diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 8eb7982125..2c9b053ddd 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -42,6 +42,7 @@ open Hiddentac open Genarg open Decl_kinds open Mod_subst +open Printer let strip_meta id = (* For Grammar v7 compatibility *) let s = string_of_id id in @@ -116,8 +117,8 @@ let pr_value env = function | VVoid -> str "()" | VInteger n -> int n | VIntroPattern ipat -> pr_intro_pattern ipat - | VConstr c -> Printer.prterm_env env c - | VConstr_context c -> Printer.prterm_env env c + | VConstr c -> prterm_env env c + | VConstr_context c -> prterm_env env c | (VTactic _ | VRTactic _ | VFun _ | VRec _) -> str "<fun>" (* Transforms a named_context into a (string * constr) list *) @@ -236,7 +237,7 @@ let coerce_to_inductive = function | VConstr c -> reference_of_constr c | _ -> failwith "" in errorlabstrm "coerce_to_inductive" - (Printer.pr_global r ++ str " is not an inductive type") + (pr_global r ++ str " is not an inductive type") with _ -> errorlabstrm "coerce_to_inductive" (str "Found an argument which should be an inductive type") @@ -1841,7 +1842,7 @@ let subst_inductive subst (kn,i) = (subst_kn subst kn,i) let subst_rawconstr subst (c,e) = assert (e=None); (* e<>None only for toplevel tactics *) - (subst_raw subst c,None) + (Detyping.subst_raw subst c,None) let subst_binding subst (loc,b,c) = (loc,subst_quantified_hypothesis subst b,subst_rawconstr subst c) @@ -1872,11 +1873,23 @@ let subst_located f (_loc,id) = (loc,f id) let subst_reference subst = subst_or_var (subst_located (subst_kn subst)) +(*CSC: subst_global_reference is used "only" for RefArgType, that propagates + to the syntactic non-terminals "global", used in commands such as + Print. It is also used for non-evaluable references. *) let subst_global_reference subst = - subst_or_var (subst_located (subst_global subst)) + let subst_global ref = + let ref',t' = subst_global subst ref in + if not (eq_constr (constr_of_reference ref') t') then + ppnl (str "Warning: the reference " ++ pr_global ref ++ str " is not " ++ + str " expanded to \"" ++ prterm t' ++ str "\", but to " ++ + pr_global ref') ; + ref' + in + subst_or_var (subst_located subst_global) let subst_evaluable subst = - subst_or_var (subst_and_short_name (subst_evaluable_reference subst)) + let subst_eval_ref = subst_evaluable_reference subst in + subst_or_var (subst_and_short_name subst_eval_ref) let subst_unfold subst (l,e) = (l,subst_evaluable subst e) |