Merge branch 'v8.5'

5 files changed, 38 insertions, 30 deletions

diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index e1c9c2de59..e6a8cbe3ad 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -21,7 +21,7 @@ open Ind_tables
 
 (* Induction/recursion schemes *)
 
-let optimize_non_type_induction_scheme kind dep sort ind =
+let optimize_non_type_induction_scheme kind dep sort _ ind =
   let env = Global.env () in
   let sigma = Evd.from_env env in
   if check_scheme kind ind then
@@ -68,15 +68,15 @@ let build_induction_scheme_in_type dep sort ind =
  
 let rect_scheme_kind_from_type =
   declare_individual_scheme_object "_rect_nodep"
-    (fun x -> build_induction_scheme_in_type false InType x, Declareops.no_seff)
+    (fun _ x -> build_induction_scheme_in_type false InType x, Declareops.no_seff)
 
 let rect_scheme_kind_from_prop =
   declare_individual_scheme_object "_rect" ~aux:"_rect_from_prop"
-    (fun x -> build_induction_scheme_in_type false InType x, Declareops.no_seff)
+    (fun _ x -> build_induction_scheme_in_type false InType x, Declareops.no_seff)
 
 let rect_dep_scheme_kind_from_type =
   declare_individual_scheme_object "_rect" ~aux:"_rect_from_type"
-    (fun x -> build_induction_scheme_in_type true InType x, Declareops.no_seff)
+    (fun _ x -> build_induction_scheme_in_type true InType x, Declareops.no_seff)
 
 let ind_scheme_kind_from_type =
   declare_individual_scheme_object "_ind_nodep"
@@ -109,24 +109,24 @@ let build_case_analysis_scheme_in_type dep sort ind =
 
 let case_scheme_kind_from_type =
   declare_individual_scheme_object "_case_nodep"
-  (fun x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff)
+  (fun _ x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff)
 
 let case_scheme_kind_from_prop =
   declare_individual_scheme_object "_case" ~aux:"_case_from_prop"
-  (fun x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff)
+  (fun _ x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff)
 
 let case_dep_scheme_kind_from_type =
   declare_individual_scheme_object "_case" ~aux:"_case_from_type"
-  (fun x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff)
+  (fun _ x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff)
 
 let case_dep_scheme_kind_from_type_in_prop =
   declare_individual_scheme_object "_casep_dep"
-  (fun x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff)
+  (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff)
 
 let case_dep_scheme_kind_from_prop =
   declare_individual_scheme_object "_case_dep"
-  (fun x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff)
+  (fun _ x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff)
 
 let case_dep_scheme_kind_from_prop_in_prop =
   declare_individual_scheme_object "_casep"
-  (fun x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff)
+  (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff)
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 8643fe10f0..f7d3ad5d0a 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -191,7 +191,7 @@ let build_sym_scheme env ind =
 
 let sym_scheme_kind =
   declare_individual_scheme_object "_sym_internal"
-  (fun ind -> 
+  (fun _ ind ->
     let c, ctx = build_sym_scheme (Global.env() (* side-effect! *)) ind in
       (c, ctx), Declareops.no_seff)
 
@@ -262,7 +262,7 @@ let build_sym_involutive_scheme env ind =
 
 let sym_involutive_scheme_kind =
   declare_individual_scheme_object "_sym_involutive"
-  (fun ind -> 
+  (fun _ ind ->
     build_sym_involutive_scheme (Global.env() (* side-effect! *)) ind)
 
 (**********************************************************************)
@@ -650,7 +650,7 @@ let build_r2l_forward_rew_scheme = build_r2l_forward_rew_scheme
 (**********************************************************************)
 let rew_l2r_dep_scheme_kind =
   declare_individual_scheme_object "_rew_r_dep"
-  (fun ind -> build_l2r_rew_scheme true (Global.env()) ind InType)
+  (fun _ ind -> build_l2r_rew_scheme true (Global.env()) ind InType)
 
 (**********************************************************************)
 (* Dependent rewrite from right-to-left in conclusion                 *)
@@ -660,7 +660,7 @@ let rew_l2r_dep_scheme_kind =
 (**********************************************************************)
 let rew_r2l_dep_scheme_kind =
   declare_individual_scheme_object "_rew_dep"
-  (fun ind -> build_r2l_rew_scheme true (Global.env()) ind InType,Declareops.no_seff)
+  (fun _ ind -> build_r2l_rew_scheme true (Global.env()) ind InType,Declareops.no_seff)
 
 (**********************************************************************)
 (* Dependent rewrite from right-to-left in hypotheses                 *)
@@ -670,7 +670,7 @@ let rew_r2l_dep_scheme_kind =
 (**********************************************************************)
 let rew_r2l_forward_dep_scheme_kind =
   declare_individual_scheme_object "_rew_fwd_dep"
-  (fun ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff)
+  (fun _ ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff)
 
 (**********************************************************************)
 (* Dependent rewrite from left-to-right in hypotheses                 *)
@@ -680,7 +680,7 @@ let rew_r2l_forward_dep_scheme_kind =
 (**********************************************************************)
 let rew_l2r_forward_dep_scheme_kind =
   declare_individual_scheme_object "_rew_fwd_r_dep"
-  (fun ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff)
+  (fun _ ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff)
 
 (**********************************************************************)
 (* Non-dependent rewrite from either left-to-right in conclusion or   *)
@@ -693,7 +693,7 @@ let rew_l2r_forward_dep_scheme_kind =
 (**********************************************************************)
 let rew_l2r_scheme_kind =
   declare_individual_scheme_object "_rew_r"
-  (fun ind -> fix_r2l_forward_rew_scheme
+  (fun _ ind -> fix_r2l_forward_rew_scheme
      (build_r2l_forward_rew_scheme false (Global.env()) ind InType), Declareops.no_seff)
 
 (**********************************************************************)
@@ -704,7 +704,7 @@ let rew_l2r_scheme_kind =
 (**********************************************************************)
 let rew_r2l_scheme_kind =
   declare_individual_scheme_object "_rew"
-  (fun ind -> build_r2l_rew_scheme false (Global.env()) ind InType, Declareops.no_seff)
+  (fun _ ind -> build_r2l_rew_scheme false (Global.env()) ind InType, Declareops.no_seff)
 
 (* End of rewriting schemes *)
 
@@ -780,6 +780,6 @@ let build_congr env (eq,refl,ctx) ind =
   in c, Evd.evar_universe_context_of ctx
 
 let congr_scheme_kind = declare_individual_scheme_object "_congr"
-  (fun ind ->
+  (fun _ ind ->
     (* May fail if equality is not defined *)
     build_congr (Global.env()) (get_coq_eq Univ.ContextSet.empty) ind, Declareops.no_seff)
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index e4240cb5cc..af0870bc92 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -320,7 +320,7 @@ let project_hint pri l2r r =
     Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l"))
   in
   let ctx = Evd.universe_context_set sigma in
-  let c = Declare.declare_definition ~internal:Declare.KernelSilent id (c,ctx) in
+  let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in
     (pri,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c))
 
 let add_hints_iff l2r lc n bl =
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index aa057a3e86..c64a1226ab 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1542,7 +1542,7 @@ let newfail n s =
 
 let cl_rewrite_clause_newtac ?abs ?origsigma strat clause =
   let open Proofview.Notations in
-  let treat sigma (res, is_hyp) = 
+  let treat sigma res = 
     match res with
     | None -> newfail 0 (str "Nothing to rewrite")
     | Some None -> Proofview.tclUNIT ()
@@ -1550,7 +1550,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma strat clause =
         let (undef, prf, newt) = res in
         let fold ev _ accu = if Evd.mem sigma ev then accu else ev :: accu in
         let gls = List.rev (Evd.fold_undefined fold undef []) in
-	match is_hyp, prf with
+	match clause, prf with
 	| Some id, Some p ->
             let tac = Proofview.Refine.refine ~unsafe:false (fun h -> (h, p)) <*> Proofview.Unsafe.tclNEWGOALS gls in
             Proofview.Unsafe.tclEVARS undef <*>
@@ -1582,17 +1582,25 @@ let cl_rewrite_clause_newtac ?abs ?origsigma strat clause =
     let concl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
     let sigma = Proofview.Goal.sigma gl in
-    let ty, is_hyp =
-      match clause with
-      | Some id -> Environ.named_type id env, Some id
-      | None -> concl, None
+    let ty = match clause with
+    | None -> concl
+    | Some id -> Environ.named_type id env
+    in
+    let env = match clause with
+    | None -> env
+    | Some id ->
+      (** Only consider variables not depending on [id] *)
+      let ctx = Environ.named_context env in
+      let filter decl = not (occur_var_in_decl env id decl) in
+      let nctx = List.filter filter ctx in
+      Environ.reset_with_named_context (Environ.val_of_named_context nctx) env
     in
     try
       let res =
-        cl_rewrite_clause_aux ?abs strat env [] sigma ty is_hyp
+        cl_rewrite_clause_aux ?abs strat env [] sigma ty clause
       in
       let sigma = match origsigma with None -> sigma | Some sigma -> sigma in
-      treat sigma (res, is_hyp) <*>
+      treat sigma res <*>
       (** For compatibility *)
       beta <*> opt_beta <*> Proofview.shelve_unifiable
     with
@@ -1888,7 +1896,7 @@ let add_morphism_infer glob m n =
   let instance = build_morphism_signature m in
   let evd = Evd.empty (*FIXME *) in
     if Lib.is_modtype () then
-      let cst = Declare.declare_constant ~internal:Declare.KernelSilent instance_id
+      let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id
 				(Entries.ParameterEntry 
 				 (None,poly,(instance,Univ.UContext.empty),None), 
 				 Decl_kinds.IsAssumption Decl_kinds.Logical)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index fea7ab72e4..b5dc2dc8be 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4510,7 +4510,7 @@ let abstract_subproof id gk tac =
   let cd = Entries.DefinitionEntry const in
   let decl = (cd, IsProof Lemma) in
   (** ppedrot: seems legit to have abstracted subproofs as local*)
-  let cst = Declare.declare_constant ~internal:Declare.KernelSilent ~local:true id decl in
+  let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest ~local:true id decl in
   (* let evd, lem = Evd.fresh_global (Global.env ()) evd (ConstRef cst) in *)
   let lem, ctx = Universes.unsafe_constr_of_global (ConstRef cst) in
   let evd = Evd.set_universe_context evd ectx in