From 15dc0ff339e01341e11c5dec63689ddc3e500e96 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 15 May 2015 15:00:59 +0200 Subject: Granting wish #4048: Locate Ltac prints the source of redefined Ltac. --- tactics/tacenv.ml | 36 +++++++++++++++++++++++++----------- tactics/tacenv.mli | 13 +++++++++++++ tactics/tacintern.ml | 17 +++++++++++++++-- 3 files changed, 53 insertions(+), 13 deletions(-) (limited to 'tactics') diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml index 08e8bc0112..09a98bc8cc 100644 --- a/tactics/tacenv.ml +++ b/tactics/tacenv.ml @@ -75,34 +75,48 @@ let interp_ml_tactic s = open Nametab open Libobject +type ltac_entry = { + tac_for_ml : bool; + tac_body : glob_tactic_expr; + tac_redef : ModPath.t list; +} + let mactab = - Summary.ref (KNmap.empty : (bool * glob_tactic_expr) KNmap.t) + Summary.ref (KNmap.empty : ltac_entry KNmap.t) ~name:"tactic-definition" -let interp_ltac r = snd (KNmap.find r !mactab) +let ltac_entries () = !mactab + +let interp_ltac r = (KNmap.find r !mactab).tac_body + +let is_ltac_for_ml_tactic r = (KNmap.find r !mactab).tac_for_ml -let is_ltac_for_ml_tactic r = fst (KNmap.find r !mactab) +let add kn b t = + let entry = { tac_for_ml = b; tac_body = t; tac_redef = [] } in + mactab := KNmap.add kn entry !mactab -(* Declaration of the TAC-DEFINITION object *) -let add (kn,td) = mactab := KNmap.add kn td !mactab +let replace kn path t = + let (path, _, _) = KerName.repr path in + let entry _ e = { e with tac_body = t; tac_redef = path :: e.tac_redef } in + mactab := KNmap.modify kn entry !mactab let load_md i ((sp, kn), (local, id, b, t)) = match id with | None -> let () = if not local then Nametab.push_tactic (Until i) sp kn in - add (kn, (b,t)) -| Some kn -> add (kn, (b,t)) + add kn b t +| Some kn0 -> replace kn0 kn t let open_md i ((sp, kn), (local, id, b, t)) = match id with | None -> let () = if not local then Nametab.push_tactic (Exactly i) sp kn in - add (kn, (b,t)) -| Some kn -> add (kn, (b,t)) + add kn b t +| Some kn0 -> replace kn0 kn t let cache_md ((sp, kn), (local, id ,b, t)) = match id with | None -> let () = Nametab.push_tactic (Until 1) sp kn in - add (kn, (b,t)) -| Some kn -> add (kn, (b,t)) + add kn b t +| Some kn0 -> replace kn0 kn t let subst_kind subst id = match id with | None -> None diff --git a/tactics/tacenv.mli b/tactics/tacenv.mli index 9410ccb389..2df6bb04a2 100644 --- a/tactics/tacenv.mli +++ b/tactics/tacenv.mli @@ -44,6 +44,19 @@ val interp_ltac : KerName.t -> glob_tactic_expr (** Find a user-defined tactic by name. Raise [Not_found] if it is absent. *) val is_ltac_for_ml_tactic : KerName.t -> bool +(** Whether the tactic is defined from ML-side *) + +type ltac_entry = { + tac_for_ml : bool; + (** Whether the tactic is defined from ML-side *) + tac_body : glob_tactic_expr; + (** The current body of the tactic *) + tac_redef : ModPath.t list; + (** List of modules redefining the tactic in reverse chronological order *) +} + +val ltac_entries : unit -> ltac_entry KNmap.t +(** Low-level access to all Ltac entries currently defined. *) (** {5 ML tactic extensions} *) diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 5cc4c835bc..d4c67b90fb 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -809,11 +809,24 @@ let pr_ltac_fun_arg = function let print_ltac id = try let kn = Nametab.locate_tactic id in - let l,t = split_ltac_fun (Tacenv.interp_ltac kn) in + let entries = Tacenv.ltac_entries () in + let tac = KNmap.find kn entries in + let filter mp = + try Some (Nametab.shortest_qualid_of_module mp) + with Not_found -> None + in + let mods = List.map_filter filter tac.Tacenv.tac_redef in + let redefined = match mods with + | [] -> mt () + | mods -> + let redef = prlist_with_sep fnl pr_qualid mods in + fnl () ++ str "Redefined by:" ++ fnl () ++ redef + in + let l,t = split_ltac_fun tac.Tacenv.tac_body in hv 2 ( hov 2 (str "Ltac" ++ spc() ++ pr_qualid id ++ prlist pr_ltac_fun_arg l ++ spc () ++ str ":=") - ++ spc() ++ Pptactic.pr_glob_tactic (Global.env ()) t) + ++ spc() ++ Pptactic.pr_glob_tactic (Global.env ()) t) ++ redefined with Not_found -> errorlabstrm "print_ltac" -- cgit v1.2.3 From b14d88c8cd17ad524898b31c1772a0e8f70f19f8 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 16 May 2015 12:33:32 +0200 Subject: Fixing bug #2814: "Anomaly: Uncaught exception Option.IsNone". --- tactics/tactics.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'tactics') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 2791d7c484..402a9e88a1 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3597,8 +3597,11 @@ let find_induction_type isrec elim hyp0 gl = if Option.is_empty scheme.indarg then error "Cannot find induction type"; let indsign = compute_scheme_signature scheme hyp0 ind_guess in let elim = ({elimindex = Some(-1); elimbody = elimc; elimrename = None},elimt) in - scheme, ElimUsing (elim,indsign) in - (Option.get scheme.indref,scheme.nparams, elim) + scheme, ElimUsing (elim,indsign) + in + match scheme.indref with + | None -> error_ind_scheme "" + | Some ref -> ref, scheme.nparams, elim let get_elim_signature elim hyp0 gl = compute_elim_signature (given_elim hyp0 elim gl) hyp0 -- cgit v1.2.3 From 866c41b9720413e00194ba7addb9c4277e114890 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 27 May 2015 11:43:11 +0200 Subject: Fix bug #4159 Some asynchronous constraints between initial universes and the ones at the end of a proof were forgotten. Also add a message to print universes indicating if all the constraints are processed already or not. --- tactics/extratactics.ml4 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics') diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 177be2c205..e4240cb5cc 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -268,7 +268,7 @@ let add_rewrite_hint bases ort t lcsr = let c, ctx = Constrintern.interp_constr env sigma ce in let ctx = if poly then - Evd.evar_universe_context_set ctx + Evd.evar_universe_context_set Univ.UContext.empty ctx else let cstrs = Evd.evar_universe_context_constraints ctx in (Global.add_constraints cstrs; Univ.ContextSet.empty) -- cgit v1.2.3