Merge branch 'v8.5'

5 files changed, 59 insertions, 16 deletions

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)
diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml
index 492b51f1a7..c1e4d72e38 100644
--- a/tactics/tacenv.ml
+++ b/tactics/tacenv.ml
@@ -77,34 +77,48 @@ let interp_ml_tactic { mltac_name = s; mltac_index = i } =
 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 7ee591cca7..47d9efda57 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"
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