diff options
| -rwxr-xr-x | contrib/interface/blast.ml | 4 | ||||
| -rw-r--r-- | kernel/mod_subst.ml | 4 | ||||
| -rw-r--r-- | kernel/mod_subst.mli | 3 | ||||
| -rw-r--r-- | parsing/printer.ml | 5 | ||||
| -rw-r--r-- | parsing/printer.mli | 1 | ||||
| -rw-r--r-- | tactics/auto.ml | 28 | ||||
| -rw-r--r-- | tactics/auto.mli | 2 | ||||
| -rw-r--r-- | tactics/eauto.ml4 | 2 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 4 |
9 files changed, 35 insertions, 18 deletions
diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml index 72875cc9b..09b918be5 100755 --- a/contrib/interface/blast.ml +++ b/contrib/interface/blast.ml @@ -187,7 +187,7 @@ and e_my_find_search db_list local_db hdc concl = | Res_pf_THEN_trivial_fail (term,cl) -> tclTHEN (unify_e_resolve (term,cl)) (e_trivial_fail_db db_list local_db) - | Unfold_nth c -> unfold_constr c + | Unfold_nth c -> unfold_in_concl [[],c] | Extern tacast -> Auto.conclPattern concl (out_some p) tacast in @@ -405,7 +405,7 @@ and my_find_search db_list local_db hdc concl = tclTHEN (unify_resolve (term,cl)) (trivial_fail_db db_list local_db) - | Unfold_nth c -> unfold_constr c + | Unfold_nth c -> unfold_in_concl [[],c] | Extern tacast -> conclPattern concl (out_some p) tacast)) tacl diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index ba186d06e..48bb9933c 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -123,6 +123,10 @@ let subst_con sub con = let mp' = subst_mp sub mp in if mp==mp' then con else make_con mp' dir l +let subst_evaluable_reference subst = function + | EvalVarRef id -> EvalVarRef id + | EvalConstRef kn -> EvalConstRef (subst_con subst kn) + (* map_kn : (kernel_name -> kernel_name) -> constr -> constr diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index fa37c2509..f4003c7f9 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -55,6 +55,9 @@ val occur_mbid : mod_bound_id -> substitution -> bool val subst_kn : substitution -> kernel_name -> kernel_name val subst_con : substitution -> constant -> constant +val subst_evaluable_reference : + substitution -> evaluable_global_reference -> evaluable_global_reference + (* [subst_mps sub c] performs the substitution [sub] on all kernel names appearing in [c] *) diff --git a/parsing/printer.ml b/parsing/printer.ml index dcaac5697..84734351f 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -136,6 +136,11 @@ let pr_existential env ev = prterm_env env (mkEvar ev) let pr_inductive env ind = prterm_env env (mkInd ind) let pr_constructor env cstr = prterm_env env (mkConstruct cstr) let pr_global = pr_global Idset.empty +let pr_evaluable_reference ref = + let ref' = match ref with + | EvalConstRef const -> ConstRef const + | EvalVarRef sp -> VarRef sp in + pr_global ref' let pr_rawterm t = if !Options.v7 then gentermpr (Termast.ast_of_rawconstr t) diff --git a/parsing/printer.mli b/parsing/printer.mli index 22b5daa17..01b691a13 100644 --- a/parsing/printer.mli +++ b/parsing/printer.mli @@ -45,6 +45,7 @@ val pr_existential : env -> existential -> std_ppcmds val pr_constructor : env -> constructor -> std_ppcmds val pr_inductive : env -> inductive -> std_ppcmds val pr_global : global_reference -> std_ppcmds +val pr_evaluable_reference : evaluable_global_reference -> std_ppcmds val pr_pattern : constr_pattern -> std_ppcmds val pr_pattern_env : env -> names_context -> constr_pattern -> std_ppcmds diff --git a/tactics/auto.ml b/tactics/auto.ml index 7c4661929..fedf91d53 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -50,7 +50,7 @@ type auto_tactic = | ERes_pf of constr * clausenv (* Hint EApply *) | Give_exact of constr | Res_pf_THEN_trivial_fail of constr * clausenv (* Hint Immediate *) - | Unfold_nth of global_reference (* Hint Unfold *) + | Unfold_nth of evaluable_global_reference (* Hint Unfold *) | Extern of glob_tactic_expr (* Hint Extern *) type pri_auto_tactic = { @@ -248,12 +248,12 @@ let make_resolve_hyp env sigma (hname,_,htyp) = | e when Logic.catchable_exception e -> anomaly "make_resolve_hyp" (* REM : in most cases hintname = id *) -let make_unfold (hintname, ref) = +let make_unfold (hintname, ref, eref) = (ref, { hname = hintname; pri = 4; pat = None; - code = Unfold_nth ref }) + code = Unfold_nth eref }) let make_extern name pri pat tacast = let hdconstr = try_head_pattern pat in @@ -325,9 +325,9 @@ let subst_autohint (_,subst,(local,name,hintlist as obj)) = let code' = Res_pf_THEN_trivial_fail (c', trans_clenv clenv) in trans_data data code' | Unfold_nth ref -> - let ref' = subst_global subst ref in - if ref==ref' then data else - trans_data data (Unfold_nth ref') + let ref' = subst_evaluable_reference subst ref in + if ref==ref' then data else + trans_data data (Unfold_nth ref') | Extern tac -> let tac' = !forward_subst_tactic subst tac in if tac==tac' then data else @@ -441,7 +441,15 @@ let add_hints local dbnames0 h = let n = match n with | None -> id_of_global r | Some n -> n in - (n,r) in + let r' = match r with + | ConstRef c -> EvalConstRef c + | VarRef c -> EvalVarRef c + | _ -> + errorlabstrm "evalref_of_ref" + (str "Cannot coerce" ++ spc () ++ pr_global r ++ spc () ++ + str "to an evaluable reference") + in + (n,r,r') in add_unfolds (List.map f lhints) local dbnames | HintsConstructors (hintname, lqid) -> let add_one qid = @@ -478,7 +486,7 @@ let fmt_autotactic = | Give_exact c -> (str"Exact " ++ prterm c) | Res_pf_THEN_trivial_fail (c,clenv) -> (str"Apply " ++ prterm c ++ str" ; Trivial") - | Unfold_nth c -> (str"Unfold " ++ pr_global c) + | Unfold_nth c -> (str"Unfold " ++ pr_evaluable_reference c) | Extern tac -> (str "Extern " ++ Pptactic.pr_glob_tactic tac) else function @@ -487,7 +495,7 @@ let fmt_autotactic = | Give_exact c -> (str"exact " ++ prterm c) | Res_pf_THEN_trivial_fail (c,clenv) -> (str"apply " ++ prterm c ++ str" ; trivial") - | Unfold_nth c -> (str"unfold " ++ pr_global c) + | Unfold_nth c -> (str"unfold " ++ pr_evaluable_reference c) | Extern tac -> (str "(external) " ++ Pptacticnew.pr_glob_tactic (Global.env()) tac) @@ -669,7 +677,7 @@ and my_find_search db_list local_db hdc concl = tclTHEN (unify_resolve (term,cl)) (trivial_fail_db db_list local_db) - | Unfold_nth c -> unfold_constr c + | Unfold_nth c -> unfold_in_concl [[],c] | Extern tacast -> conclPattern concl (out_some p) tacast)) tacl diff --git a/tactics/auto.mli b/tactics/auto.mli index 88be710c6..5c1959169 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -29,7 +29,7 @@ type auto_tactic = | ERes_pf of constr * clausenv (* Hint EApply *) | Give_exact of constr | Res_pf_THEN_trivial_fail of constr * clausenv (* Hint Immediate *) - | Unfold_nth of global_reference (* Hint Unfold *) + | Unfold_nth of evaluable_global_reference (* Hint Unfold *) | Extern of Tacexpr.glob_tactic_expr (* Hint Extern *) open Rawterm diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 64188d3b8..79753ac73 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -227,7 +227,7 @@ and e_my_find_search db_list local_db hdc concl = | Res_pf_THEN_trivial_fail (term,cl) -> tclTHEN (unify_e_resolve (term,cl)) (e_trivial_fail_db db_list local_db) - | Unfold_nth c -> unfold_constr c + | Unfold_nth c -> unfold_in_concl [[],c] | Extern tacast -> conclPattern concl (out_some p) tacast in diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 3c4130e79..a53724b64 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1858,10 +1858,6 @@ let subst_induction_arg subst = function | ElimOnAnonHyp n as x -> x | ElimOnIdent id as x -> x -let subst_evaluable_reference subst = function - | EvalVarRef id -> EvalVarRef id - | EvalConstRef kn -> EvalConstRef (subst_con subst kn) - let subst_and_short_name f (c,n) = assert (n=None); (* since tacdef are strictly globalized *) (f c,None) |