Merge remote-tracking branch 'origin/master' into stm+doc_hook

12 files changed, 376 insertions, 320 deletions

diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index 7a61deba0c..6dd9a976f9 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -158,9 +158,9 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
     (* do not compute the implicit arguments, it may be costly *)
     let () = Impargs.make_implicit_args false in
     (* ppedrot: seems legit to have abstracted subproofs as local*)
-    Declare.declare_constant ~internal:Declare.InternalTacticRequest ~local:true id decl
+    Declare.declare_private_constant ~role:Entries.Subproof ~internal:Declare.InternalTacticRequest ~local:true id decl
   in
-  let cst = Impargs.with_implicit_protection cst () in
+  let cst, eff = Impargs.with_implicit_protection cst () in
   let inst = match const.Entries.const_entry_universes with
   | Entries.Monomorphic_entry _ -> EInstance.empty
   | Entries.Polymorphic_entry (_, ctx) ->
@@ -174,7 +174,6 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
   let lem = mkConstU (cst, inst) in
   let evd = Evd.set_universe_context evd ectx in
   let open Safe_typing in
-  let eff = private_con_of_con (Global.safe_env ()) cst in
   let effs = concat_private eff
     Entries.(snd (Future.force const.const_entry_body)) in
   let solve =
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index c1ac7d201a..160e4f164e 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -548,7 +548,7 @@ let make_resolve_hyp env sigma st flags only_classes pri decl =
           make_apply_entry ~name env sigma flags pri false])
     else []
 
-let make_hints g st only_classes sign =
+let make_hints g (modes,st) only_classes sign =
   let hintlist =
     List.fold_left
       (fun hints hyp ->
@@ -565,7 +565,9 @@ let make_hints g st only_classes sign =
           in hint @ hints
         else hints)
       ([]) sign
-  in Hint_db.add_list (pf_env g) (project g) hintlist (Hint_db.empty st true)
+  in
+  let db = Hint_db.add_modes modes @@ Hint_db.empty st true in
+  Hint_db.add_list (pf_env g) (project g) hintlist db
 
 module Search = struct
   type autoinfo =
@@ -578,29 +580,29 @@ module Search = struct
 
   (** Local hints *)
   let autogoal_cache = Summary.ref ~name:"autogoal_cache"
-      (DirPath.empty, true, Context.Named.empty,
+      (DirPath.empty, true, Context.Named.empty, GlobRef.Map.empty,
        Hint_db.empty TransparentState.full true)
 
-  let make_autogoal_hints only_classes ?(st=TransparentState.full) g =
+  let make_autogoal_hints only_classes (modes,st as mst) g =
     let open Proofview in
     let open Tacmach.New in
     let sign = Goal.hyps g in
-    let (dir, onlyc, sign', cached_hints) = !autogoal_cache in
+    let (dir, onlyc, sign', cached_modes, cached_hints) = !autogoal_cache in
     let cwd = Lib.cwd () in
     let eq c1 c2 = EConstr.eq_constr (project g) c1 c2 in
     if DirPath.equal cwd dir &&
          (onlyc == only_classes) &&
            Context.Named.equal eq sign sign' &&
-             Hint_db.transparent_state cached_hints == st
+             cached_modes == modes
     then cached_hints
     else
       let hints = make_hints {it = Goal.goal g; sigma = project g}
-                             st only_classes sign
+                             mst only_classes sign
       in
-      autogoal_cache := (cwd, only_classes, sign, hints); hints
+      autogoal_cache := (cwd, only_classes, sign, modes, hints); hints
 
-  let make_autogoal ?(st=TransparentState.full) only_classes dep cut i g =
-    let hints = make_autogoal_hints only_classes ~st g in
+  let make_autogoal mst only_classes dep cut i g =
+    let hints = make_autogoal_hints only_classes mst g in
     { search_hints = hints;
       search_depth = [i]; last_tac = lazy (str"none");
       search_dep = dep;
@@ -695,7 +697,8 @@ module Search = struct
           if b && not (Context.Named.equal eq (Goal.hyps gl') (Goal.hyps gl))
           then
             let st = Hint_db.transparent_state info.search_hints in
-            make_autogoal_hints info.search_only_classes ~st gl'
+            let modes = Hint_db.modes info.search_hints in
+            make_autogoal_hints info.search_only_classes (modes,st) gl'
           else info.search_hints
         in
         let dep' = info.search_dep || Proofview.unifiable sigma' (Goal.goal gl') gls in
@@ -830,19 +833,19 @@ module Search = struct
                       (fun e' -> let (e, info) = merge_exceptions e e' in
                               Proofview.tclZERO ~info e))
 
-  let search_tac_gl ?st only_classes dep hints depth i sigma gls gl :
+  let search_tac_gl mst only_classes dep hints depth i sigma gls gl :
         unit Proofview.tactic =
     let open Proofview in
     let dep = dep || Proofview.unifiable sigma (Goal.goal gl) gls in
-    let info = make_autogoal ?st only_classes dep (cut_of_hints hints) i gl in
+    let info = make_autogoal mst only_classes dep (cut_of_hints hints) i gl in
     search_tac hints depth 1 info
 
-  let search_tac ?(st=TransparentState.full) only_classes dep hints depth =
+  let search_tac mst only_classes dep hints depth =
     let open Proofview in
     let tac sigma gls i =
       Goal.enter
         begin fun gl ->
-          search_tac_gl ~st only_classes dep hints depth (succ i) sigma gls gl end
+          search_tac_gl mst only_classes dep hints depth (succ i) sigma gls gl end
     in
       Proofview.Unsafe.tclGETGOALS >>= fun gls ->
       let gls = CList.map Proofview.drop_state gls in
@@ -867,11 +870,11 @@ module Search = struct
                                    | (e,ie) -> Proofview.tclZERO ~info:ie e)
     in aux 1
 
-  let eauto_tac ?(st=TransparentState.full) ?(unique=false)
+  let eauto_tac mst ?(unique=false)
                 ~only_classes ?strategy ~depth ~dep hints =
     let open Proofview in
     let tac =
-      let search = search_tac ~st only_classes dep hints in
+      let search = search_tac mst only_classes dep hints in
       let dfs =
         match strategy with
         | None -> not (get_typeclasses_iterative_deepening ())
@@ -915,8 +918,8 @@ module Search = struct
                                             | Some i -> str ", with depth limit " ++ int i));
     tac
 
-  let eauto_tac ?st ?unique ~only_classes ?strategy ~depth ~dep hints =
-    Hints.wrap_hint_warning @@ eauto_tac ?st ?unique ~only_classes ?strategy ~depth ~dep hints
+  let eauto_tac mst ?unique ~only_classes ?strategy ~depth ~dep hints =
+    Hints.wrap_hint_warning @@ eauto_tac mst ?unique ~only_classes ?strategy ~depth ~dep hints
 
   let run_on_evars env evm p tac =
     match evars_to_goals p evm with
@@ -968,8 +971,8 @@ module Search = struct
          else raise Not_found
        with Logic_monad.TacticFailure _ -> raise Not_found
 
-  let evars_eauto env evd depth only_classes unique dep st hints p =
-    let eauto_tac = eauto_tac ~st ~unique ~only_classes ~depth ~dep:(unique || dep) hints in
+  let evars_eauto env evd depth only_classes unique dep mst hints p =
+    let eauto_tac = eauto_tac mst ~unique ~only_classes ~depth ~dep:(unique || dep) hints in
     let res = run_on_evars env evd p eauto_tac in
     match res with
     | None -> evd
@@ -983,11 +986,11 @@ module Search = struct
 
   let typeclasses_resolve env evd debug depth unique p =
     let db = searchtable_map typeclasses_db in
-    typeclasses_eauto env evd ?depth unique (Hint_db.transparent_state db) [db] p
+    let st = Hint_db.transparent_state db in
+    let modes = Hint_db.modes db in
+    typeclasses_eauto env evd ?depth unique (modes,st) [db] p
 end
 
-(** Binding to either V85 or Search implementations. *)
-
 let typeclasses_eauto ?(only_classes=false) ?(st=TransparentState.full)
                       ?strategy ~depth dbs =
   let dbs = List.map_filter
@@ -996,8 +999,10 @@ let typeclasses_eauto ?(only_classes=false) ?(st=TransparentState.full)
               dbs
   in
   let st = match dbs with x :: _ -> Hint_db.transparent_state x | _ -> st in
+  let modes = List.map Hint_db.modes dbs in
+  let modes = List.fold_left (GlobRef.Map.union (fun _ m1 m2 -> Some (m1@m2))) GlobRef.Map.empty modes in
   let depth = match depth with None -> get_typeclasses_depth () | Some l -> Some l in
-  Search.eauto_tac ~st ~only_classes ?strategy ~depth ~dep:true dbs
+  Search.eauto_tac (modes,st) ~only_classes ?strategy ~depth ~dep:true dbs
 
 (** We compute dependencies via a union-find algorithm.
     Beware of the imperative effects on the partition structure,
@@ -1140,11 +1145,12 @@ let resolve_one_typeclass env ?(sigma=Evd.from_env env) gl unique =
   let gls = { it = gl ; sigma = sigma; } in
   let hints = searchtable_map typeclasses_db in
   let st = Hint_db.transparent_state hints in
+  let modes = Hint_db.modes hints in
   let depth = get_typeclasses_depth () in
   let gls' =
       try
         Proofview.V82.of_tactic
-        (Search.eauto_tac ~st ~only_classes:true ~depth [hints] ~dep:true) gls
+        (Search.eauto_tac (modes,st) ~only_classes:true ~depth [hints] ~dep:true) gls
       with Refiner.FailError _ -> raise Not_found
   in
   let evd = sig_sig gls' in
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli
index c950e3de3d..b9291f6124 100644
--- a/tactics/class_tactics.mli
+++ b/tactics/class_tactics.mli
@@ -27,9 +27,18 @@ type search_strategy = Dfs | Bfs
 
 val set_typeclasses_strategy : search_strategy -> unit
 
-val typeclasses_eauto : ?only_classes:bool -> ?st:TransparentState.t -> ?strategy:search_strategy ->
-                        depth:(Int.t option) ->
-                        Hints.hint_db_name list -> unit Proofview.tactic
+val typeclasses_eauto :
+  ?only_classes:bool
+  (** Should non-class goals be shelved and resolved at the end *)
+  -> ?st:TransparentState.t
+  (** The transparent_state used when working with local hypotheses  *)
+  -> ?strategy:search_strategy
+  (** Is a traversing-strategy specified? *)
+  -> depth:(Int.t option)
+  (** Bounded or unbounded search *)
+  -> Hints.hint_db_name list
+  (** The list of hint databases to use *)
+  -> unit Proofview.tactic
 
 val head_of_constr : Id.t -> constr -> unit Proofview.tactic
 
@@ -41,8 +50,8 @@ val autoapply : constr -> Hints.hint_db_name -> unit Proofview.tactic
 
 module Search : sig
   val eauto_tac :
-    ?st:TransparentState.t
-    (** The transparent_state used when working with local hypotheses  *)
+    Hints.hint_mode array list GlobRef.Map.t * TransparentState.t
+    (** The transparent_state and modes used when working with local hypotheses  *)
     -> ?unique:bool
     (** Should we force a unique solution *)
     -> only_classes:bool
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 3019fc0231..0857c05968 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -514,7 +514,7 @@ let autounfold_one db cl =
   in
     if did then
       match cl with
-      | Some hyp -> change_in_hyp None (make_change_arg c') hyp
-      | None -> convert_concl_no_check c' DEFAULTcast
+      | Some hyp -> change_in_hyp ~check:true None (make_change_arg c') hyp
+      | None -> convert_concl ~check:false c' DEFAULTcast
     else Tacticals.New.tclFAIL 0 (str "Nothing to unfold")
   end
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 3d760f1c3d..45a4799ea1 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -417,7 +417,7 @@ let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars d
   find_elim hdcncl lft2rgt dep cls (Some t) >>= fun elim ->
       general_elim_clause with_evars frzevars tac cls c t l
       (match lft2rgt with None -> false | Some b -> b)
-      {elimindex = None; elimbody = (elim,NoBindings); elimrename = None}
+      {elimindex = None; elimbody = (elim,NoBindings) }
   end
 
 let adjust_rewriting_direction args lft2rgt =
@@ -1613,10 +1613,10 @@ let cutSubstInHyp l2r eqn id =
   tclTHEN (Proofview.Unsafe.tclEVARS sigma)
     (tclTHENFIRST
     (tclTHENLIST [
-       (change_in_hyp None (make_change_arg typ) (id,InHypTypeOnly));
+       (change_in_hyp ~check:true None (make_change_arg typ) (id,InHypTypeOnly));
        (replace_core (onHyp id) l2r eqn)
     ])
-    (change_in_hyp None (make_change_arg expected) (id,InHypTypeOnly)))
+    (change_in_hyp ~check:true None (make_change_arg expected) (id,InHypTypeOnly)))
   end
 
 let try_rewrite tac =
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 11a8816159..cc56c1c425 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -289,8 +289,6 @@ let lookup_tacs sigma concl st se =
   let sl' = List.stable_sort pri_order_int l' in
   List.merge pri_order_int se.sentry_nopat sl'
 
-module Constr_map = Map.Make(GlobRef.Ordered)
-
 let is_transparent_gr ts = function
   | VarRef id -> TransparentState.is_transparent_variable ts id
   | ConstRef cst -> TransparentState.is_transparent_constant ts cst
@@ -520,6 +518,8 @@ val add_cut : hints_path -> t -> t
 val add_mode : GlobRef.t -> hint_mode array -> t -> t
 val cut : t -> hints_path
 val unfolds : t -> Id.Set.t * Cset.t
+val add_modes : hint_mode array list GlobRef.Map.t -> t -> t
+val modes : t -> hint_mode array list GlobRef.Map.t
 val fold : (GlobRef.t option -> hint_mode array list -> full_hint list -> 'a -> 'a) ->
   t -> 'a -> 'a
 
@@ -532,7 +532,7 @@ struct
     hintdb_unfolds : Id.Set.t * Cset.t;
     hintdb_max_id : int;
     use_dn : bool;
-    hintdb_map : search_entry Constr_map.t;
+    hintdb_map : search_entry GlobRef.Map.t;
     (* A list of unindexed entries starting with an unfoldable constant
        or with no associated pattern. *)
     hintdb_nopat : (GlobRef.t option * stored_data) list;
@@ -548,12 +548,12 @@ struct
 			  hintdb_unfolds = (Id.Set.empty, Cset.empty);
 			  hintdb_max_id = 0;
 			  use_dn = use_dn;
-			  hintdb_map = Constr_map.empty;
+                          hintdb_map = GlobRef.Map.empty;
 			  hintdb_nopat = [];
 			  hintdb_name = name; }
 
   let find key db =
-    try Constr_map.find key db.hintdb_map
+    try GlobRef.Map.find key db.hintdb_map
     with Not_found -> empty_se
  
   let realize_tac secvars (id,tac) =
@@ -650,11 +650,11 @@ struct
 	  else db
       | Some gr ->
 	  let oval = find gr db in
-	    { db with hintdb_map = Constr_map.add gr (add_tac pat idv dnst oval) db.hintdb_map }
+            { db with hintdb_map = GlobRef.Map.add gr (add_tac pat idv dnst oval) db.hintdb_map }
 
   let rebuild_db st' db =
     let db' =
-      { db with hintdb_map = Constr_map.map (rebuild_dn st') db.hintdb_map;
+      { db with hintdb_map = GlobRef.Map.map (rebuild_dn st') db.hintdb_map;
 	hintdb_state = st'; hintdb_nopat = [] }
     in
       List.fold_left (fun db (gr,(id,v)) -> addkv gr id v db) db' db.hintdb_nopat
@@ -693,7 +693,7 @@ struct
   let remove_list grs db =
     let filter (_, h) =
       match h.name with PathHints [gr] -> not (List.mem_f GlobRef.equal gr grs) | _ -> true in
-    let hintmap = Constr_map.map (remove_he db.hintdb_state filter) db.hintdb_map in
+    let hintmap = GlobRef.Map.map (remove_he db.hintdb_state filter) db.hintdb_map in
     let hintnopat = List.filter (fun (ge, sd) -> filter sd) db.hintdb_nopat in
       { db with hintdb_map = hintmap; hintdb_nopat = hintnopat }
 
@@ -706,11 +706,11 @@ struct
   let iter f db =
     let iter_se k se = f (Some k) se.sentry_mode (get_entry se) in
     f None [] (List.map (fun x -> snd (snd x)) db.hintdb_nopat);
-    Constr_map.iter iter_se db.hintdb_map
+    GlobRef.Map.iter iter_se db.hintdb_map
 
   let fold f db accu =
     let accu = f None [] (List.map (fun x -> snd (snd x)) db.hintdb_nopat) accu in
-    Constr_map.fold (fun k se -> f (Some k) se.sentry_mode (get_entry se)) db.hintdb_map accu
+    GlobRef.Map.fold (fun k se -> f (Some k) se.sentry_mode (get_entry se)) db.hintdb_map accu
 
   let transparent_state db = db.hintdb_state
 
@@ -724,12 +724,21 @@ struct
   let add_mode gr m db =
     let se = find gr db in
     let se = { se with sentry_mode = m :: se.sentry_mode } in
-    { db with hintdb_map = Constr_map.add gr se db.hintdb_map }
+    { db with hintdb_map = GlobRef.Map.add gr se db.hintdb_map }
 
   let cut db = db.hintdb_cut
 
   let unfolds db = db.hintdb_unfolds
 
+  let add_modes modes db =
+    let f gr e me =
+      Some { e with sentry_mode = me.sentry_mode @ e.sentry_mode }
+    in
+    let mode_entries = GlobRef.Map.map (fun m -> { empty_se with sentry_mode = m }) modes in
+    { db with hintdb_map = GlobRef.Map.union f db.hintdb_map mode_entries }
+
+  let modes db = GlobRef.Map.map (fun se -> se.sentry_mode) db.hintdb_map
+
   let use_dn db = db.use_dn
 
 end
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 90a8b7fe52..7b8f96cdd8 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -162,6 +162,9 @@ module Hint_db :
     val cut : t -> hints_path
 
     val unfolds : t -> Id.Set.t * Cset.t
+
+    val add_modes : hint_mode array list GlobRef.Map.t -> t -> t
+    val modes : t -> hint_mode array list GlobRef.Map.t
   end
 
 type hint_db = Hint_db.t
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index 16829482e5..b9485b8823 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -116,8 +116,7 @@ let compute_name internal id =
   | InternalTacticRequest ->
       Namegen.next_ident_away_from (add_prefix "internal_" id) is_visible_name
 
-let define internal id c poly univs =
-  let fd = declare_constant ~internal in
+let define internal role id c poly univs =
   let id = compute_name internal id in
   let ctx = UState.minimize univs in
   let c = UnivSubst.nf_evars_and_universes_opt_subst (fun _ -> None) (UState.subst ctx) c in
@@ -133,12 +132,12 @@ let define internal id c poly univs =
     const_entry_inline_code = false;
     const_entry_feedback = None;
   } in
-  let kn = fd id (DefinitionEntry entry, Decl_kinds.IsDefinition Scheme) in
+  let kn, eff = declare_private_constant ~role ~internal id (DefinitionEntry entry, Decl_kinds.IsDefinition Scheme) in
   let () = match internal with
     | InternalTacticRequest -> ()
     | _-> definition_message id
   in
-  kn
+  kn, eff
 
 let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) =
   let (c, ctx), eff = f mode ind in
@@ -146,10 +145,10 @@ let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) =
   let id = match idopt with
     | Some id -> id
     | None -> add_suffix mib.mind_packets.(i).mind_typename suff in
-  let const = define mode id c (Declareops.inductive_is_polymorphic mib) ctx in
+  let role = Entries.Schema (ind, kind) in
+  let const, neff = define mode role id c (Declareops.inductive_is_polymorphic mib) ctx in
   declare_scheme kind [|ind,const|];
-  const, Safe_typing.concat_private
-     (Safe_typing.private_con_of_scheme ~kind (Global.safe_env()) [ind,const]) eff
+  const, Safe_typing.concat_private neff eff
 
 let define_individual_scheme kind mode names (mind,i as ind) =
   match Hashtbl.find scheme_object_table kind with
@@ -163,15 +162,15 @@ let define_mutual_scheme_base kind suff f mode names mind =
   let ids = Array.init (Array.length mib.mind_packets) (fun i ->
       try Int.List.assoc i names
       with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in
-  let consts = Array.map2 (fun id cl -> 
-     define mode id cl (Declareops.inductive_is_polymorphic mib) ctx) ids cl in
+  let fold i effs id cl =
+    let role = Entries.Schema ((mind, i), kind)in
+    let cst, neff = define mode role id cl (Declareops.inductive_is_polymorphic mib) ctx in
+    (Safe_typing.concat_private neff effs, cst)
+  in
+  let (eff, consts) = Array.fold_left2_map_i fold eff ids cl in
   let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in
   declare_scheme kind schemes;
-  consts,
-  Safe_typing.concat_private
-    (Safe_typing.private_con_of_scheme
-      ~kind (Global.safe_env()) (Array.to_list schemes))
-    eff 
+  consts, eff
 
 let define_mutual_scheme kind mode names mind =
   match Hashtbl.find scheme_object_table kind with
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 4aa4d13e1e..6efa1ece9c 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -204,10 +204,7 @@ let inversion_scheme ~name ~poly env sigma t sort dep_option inv_op =
     (str"Computed inversion goal was not closed in initial signature.");
   *)
   let pf = Proof.start ~name ~poly (Evd.from_ctx (evar_universe_context sigma)) [invEnv,invGoal] in
-  let pf =
-    fst (Proof.run_tactic env (
-      tclTHEN intro (onLastHypId inv_op)) pf)
-  in
+  let pf, _, () = Proof.run_tactic env (tclTHEN intro (onLastHypId inv_op)) pf in
   let pfterm = List.hd (Proof.partial_proof pf) in
   let global_named_context = Global.named_context_val () in
   let ownSign = ref begin
diff --git a/tactics/ppred.mli b/tactics/ppred.mli
index be21236f4e..c68fab5296 100644
--- a/tactics/ppred.mli
+++ b/tactics/ppred.mli
@@ -6,11 +6,6 @@ val pr_with_occurrences :
 val pr_short_red_flag : ('a -> Pp.t) -> 'a glob_red_flag -> Pp.t
 val pr_red_flag : ('a -> Pp.t) -> 'a glob_red_flag -> Pp.t
 
-val pr_red_expr :
-  ('a -> Pp.t) * ('a -> Pp.t) * ('b -> Pp.t) * ('c -> Pp.t) ->
-  (string -> Pp.t) -> ('a,'b,'c) red_expr_gen -> Pp.t
-  [@@ocaml.deprecated "Use pr_red_expr_env instead"]
-
 val pr_red_expr_env : Environ.env -> Evd.evar_map ->
   (Environ.env -> Evd.evar_map -> 'a -> Pp.t) *
   (Environ.env -> Evd.evar_map -> 'a -> Pp.t) *
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 066b9c7794..9dafa8bad9 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -145,7 +145,7 @@ let introduction id =
 
 let error msg = CErrors.user_err Pp.(str msg)
 
-let convert_concl ?(check=true) ty k =
+let convert_concl ~check ty k =
   Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     let conclty = Proofview.Goal.concl gl in
@@ -163,12 +163,12 @@ let convert_concl ?(check=true) ty k =
     end
   end
 
-let convert_hyp ?(check=true) d =
+let convert_hyp ~check ~reorder d =
   Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
     let ty = Proofview.Goal.concl gl in
-    let sign = convert_hyp check (named_context_val env) sigma d in
+    let sign = convert_hyp ~check ~reorder env sigma d in
     let env = reset_with_named_context sign env in
     Refine.refine ~typecheck:false begin fun sigma ->
       Evarutil.new_evar env sigma ~principal:true ty
@@ -176,7 +176,7 @@ let convert_hyp ?(check=true) d =
   end
 
 let convert_concl_no_check = convert_concl ~check:false
-let convert_hyp_no_check = convert_hyp ~check:false
+let convert_hyp_no_check = convert_hyp ~check:false ~reorder:false
 
 let convert_gen pb x y =
   Proofview.Goal.enter begin fun gl ->
@@ -614,18 +614,22 @@ let cofix id = mutual_cofix id [] 0
 type tactic_reduction = Reductionops.reduction_function
 type e_tactic_reduction = Reductionops.e_reduction_function
 
-let pf_reduce_decl redfun where decl gl =
+let e_pf_change_decl (redfun : bool -> e_reduction_function) where env sigma decl =
   let open Context.Named.Declaration in
-  let redfun' c = Tacmach.New.pf_apply redfun gl c in
   match decl with
   | LocalAssum (id,ty) ->
       if where == InHypValueOnly then
         user_err  (Id.print id.binder_name ++ str " has no value.");
-      LocalAssum (id,redfun' ty)
+    let (sigma, ty') = redfun false env sigma ty in
+    (sigma, LocalAssum (id, ty'))
   | LocalDef (id,b,ty) ->
-      let b' = if where != InHypTypeOnly then redfun' b else b in
-      let ty' =	if where != InHypValueOnly then redfun' ty else ty in
-      LocalDef (id,b',ty')
+      let (sigma, b') =
+        if where != InHypTypeOnly then redfun true env sigma b else (sigma, b)
+      in
+      let (sigma, ty') =
+        if where != InHypValueOnly then redfun false env sigma ty else (sigma, ty)
+      in
+      (sigma, LocalDef (id,b',ty'))
 
 (* Possibly equip a reduction with the occurrences mentioned in an
    occurrence clause *)
@@ -695,41 +699,9 @@ let bind_red_expr_occurrences occs nbcl redexp =
    reduction function either to the conclusion or to a
    certain hypothesis *)
 
-let reduct_in_concl (redfun,sty) =
-  Proofview.Goal.enter begin fun gl ->
-    convert_concl_no_check (Tacmach.New.pf_apply redfun gl (Tacmach.New.pf_concl gl)) sty
-  end
-
-let reduct_in_hyp ?(check=false) redfun (id,where) =
-  Proofview.Goal.enter begin fun gl ->
-  convert_hyp ~check (pf_reduce_decl redfun where (Tacmach.New.pf_get_hyp id gl) gl)
-  end
-
-let revert_cast (redfun,kind as r) =
-  if kind == DEFAULTcast then (redfun,REVERTcast) else r
-
-let reduct_option ?(check=false) redfun = function
-  | Some id -> reduct_in_hyp ~check (fst redfun) id
-  | None    -> reduct_in_concl (revert_cast redfun)
-
 (** Tactic reduction modulo evars (for universes essentially) *)
 
-let pf_e_reduce_decl redfun where decl gl =
-  let open Context.Named.Declaration in
-  let sigma = Proofview.Goal.sigma gl in
-  let redfun sigma c = redfun (Tacmach.New.pf_env gl) sigma c in
-  match decl with
-  | LocalAssum (id,ty) ->
-      if where == InHypValueOnly then
-        user_err  (Id.print id.binder_name ++ str " has no value.");
-    let (sigma, ty') = redfun sigma ty in
-    (sigma, LocalAssum (id, ty'))
-  | LocalDef (id,b,ty) ->
-      let (sigma, b') = if where != InHypTypeOnly then redfun sigma b else (sigma, b) in
-      let (sigma, ty') = if where != InHypValueOnly then redfun sigma ty else (sigma, ty) in
-      (sigma, LocalDef (id, b', ty'))
-
-let e_reduct_in_concl ~check (redfun, sty) =
+let e_change_in_concl ~check (redfun, sty) =
   Proofview.Goal.enter begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
     let (sigma, c') = redfun (Tacmach.New.pf_env gl) sigma (Tacmach.New.pf_concl gl) in
@@ -737,54 +709,98 @@ let e_reduct_in_concl ~check (redfun, sty) =
     (convert_concl ~check c' sty)
   end
 
-let e_reduct_in_hyp ?(check=false) redfun (id, where) =
+let e_change_in_hyp ~check ~reorder redfun (id,where) =
   Proofview.Goal.enter begin fun gl ->
-    let (sigma, decl') = pf_e_reduce_decl redfun where (Tacmach.New.pf_get_hyp id gl) gl in
+    let sigma = Proofview.Goal.sigma gl in
+    let hyp = Tacmach.New.pf_get_hyp id gl in
+    let (sigma, c) = e_pf_change_decl redfun where (Proofview.Goal.env gl) sigma hyp in
     Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
-    (convert_hyp ~check decl')
+    (convert_hyp ~check ~reorder c)
   end
 
-let e_reduct_option ?(check=false) redfun = function
-  | Some id -> e_reduct_in_hyp ~check (fst redfun) id
-  | None    -> e_reduct_in_concl ~check (revert_cast redfun)
+type hyp_conversion =
+| AnyHypConv (** Arbitrary conversion *)
+| StableHypConv (** Does not introduce new dependencies on variables *)
+| LocalHypConv (** Same as above plus no dependence on the named environment *)
 
-(** Versions with evars to maintain the unification of universes resulting
-    from conversions. *)
-
-let e_change_in_concl (redfun,sty) =
+let e_change_in_hyps ~check ~reorder f args =
   Proofview.Goal.enter begin fun gl ->
-    let sigma = Proofview.Goal.sigma gl in
-    let (sigma, c) = redfun (Proofview.Goal.env gl) sigma (Proofview.Goal.concl gl) in
-    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
-    (convert_concl_no_check c sty)
-  end
-
-let e_pf_change_decl (redfun : bool -> e_reduction_function) where decl env sigma =
-  let open Context.Named.Declaration in
-  match decl with
-  | LocalAssum (id,ty) ->
-      if where == InHypValueOnly then
-        user_err  (Id.print id.binder_name ++ str " has no value.");
-    let (sigma, ty') = redfun false env sigma ty in
-    (sigma, LocalAssum (id, ty'))
-  | LocalDef (id,b,ty) ->
-      let (sigma, b') =
-	if where != InHypTypeOnly then redfun true env sigma b else (sigma, b)
+    let env = Proofview.Goal.env gl in
+    let sigma = Tacmach.New.project gl in
+    let (env, sigma) = match reorder with
+    | LocalHypConv ->
+      (* If the reduction function is known not to depend on the named
+          context, then we can perform it in parallel. *)
+      let fold accu arg =
+        let (id, redfun) = f arg in
+        let old = try Id.Map.find id accu with Not_found -> [] in
+        Id.Map.add id (redfun :: old) accu
       in
-      let (sigma, ty') =
-	if where != InHypValueOnly then redfun false env sigma ty else (sigma, ty)
+      let reds = List.fold_left fold Id.Map.empty args in
+      let evdref = ref sigma in
+      let map d =
+        let id = NamedDecl.get_id d in
+        match Id.Map.find id reds with
+        | reds ->
+          let d = EConstr.of_named_decl d in
+          let fold redfun (sigma, d) = redfun env sigma d in
+          let (sigma, d) = List.fold_right fold reds (sigma, d) in
+          let () = evdref := sigma in
+          EConstr.Unsafe.to_named_decl d
+        | exception Not_found -> d
       in
-      (sigma, LocalDef (id,b',ty'))
-
-let e_change_in_hyp redfun (id,where) =
-  Proofview.Goal.enter begin fun gl ->
-    let sigma = Proofview.Goal.sigma gl in
-    let hyp = Tacmach.New.pf_get_hyp id gl in
-    let (sigma, c) = e_pf_change_decl redfun where hyp (Proofview.Goal.env gl) sigma in
-    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
-    (convert_hyp c)
+      let sign = Environ.map_named_val map (Environ.named_context_val env) in
+      let env = reset_with_named_context sign env in
+      (env, !evdref)
+    | StableHypConv | AnyHypConv ->
+      let reorder = reorder == AnyHypConv in
+      let fold (env, sigma) arg =
+        let (id, redfun) = f arg in
+        let hyp =
+          try lookup_named id env
+          with Not_found ->
+            raise (RefinerError (env, sigma, NoSuchHyp id))
+        in
+        let (sigma, d) = redfun env sigma hyp in
+        let sign = Logic.convert_hyp ~check ~reorder env sigma d in
+        let env = reset_with_named_context sign env in
+        (env, sigma)
+      in
+      List.fold_left fold (env, sigma) args
+    in
+    let ty = Proofview.Goal.concl gl in
+    Proofview.Unsafe.tclEVARS sigma
+    <*>
+    Refine.refine ~typecheck:false begin fun sigma ->
+      Evarutil.new_evar env sigma ~principal:true ty
+    end
   end
 
+let e_reduct_in_concl = e_change_in_concl
+
+let reduct_in_concl ~check (redfun, sty) =
+  let redfun env sigma c = (sigma, redfun env sigma c) in
+  e_change_in_concl ~check (redfun, sty)
+
+let e_reduct_in_hyp ~check ~reorder redfun (id, where) =
+  let redfun _ env sigma c = redfun env sigma c in
+  e_change_in_hyp ~check ~reorder redfun (id, where)
+
+let reduct_in_hyp ~check ~reorder redfun (id, where) =
+  let redfun _ env sigma c = (sigma, redfun env sigma c) in
+  e_change_in_hyp ~check ~reorder redfun (id, where)
+
+let revert_cast (redfun,kind as r) =
+  if kind == DEFAULTcast then (redfun,REVERTcast) else r
+
+let e_reduct_option ~check redfun = function
+  | Some id -> e_reduct_in_hyp ~check ~reorder:check (fst redfun) id
+  | None    -> e_change_in_concl ~check (revert_cast redfun)
+
+let reduct_option ~check (redfun, sty) where =
+  let redfun env sigma c = (sigma, redfun env sigma c) in
+  e_reduct_option ~check (redfun, sty) where
+
 type change_arg = Ltac_pretype.patvar_map -> env -> evar_map -> evar_map * EConstr.constr
 
 let make_change_arg c pats env sigma = (sigma, replace_vars (Id.Map.bindings pats) c)
@@ -819,15 +835,21 @@ let change_and_check cv_pb mayneedglobalcheck deep t env sigma c =
   | Some sigma -> (sigma, t')
 
 (* Use cumulativity only if changing the conclusion not a subterm *)
-let change_on_subterm cv_pb deep t where env sigma c =
+let change_on_subterm ~check cv_pb deep t where env sigma c =
   let mayneedglobalcheck = ref false in
   let (sigma, c) = match where with
-  | None -> change_and_check cv_pb mayneedglobalcheck deep (t Id.Map.empty) env sigma c
+  | None ->
+      if check then
+        change_and_check cv_pb mayneedglobalcheck deep (t Id.Map.empty) env sigma c
+      else
+        t Id.Map.empty env sigma
   | Some occl ->
       e_contextually false occl
         (fun subst ->
-          change_and_check Reduction.CONV mayneedglobalcheck true (t subst))
-        env sigma c in
+          if check then
+            change_and_check Reduction.CONV mayneedglobalcheck true (t subst)
+          else
+            fun env sigma _c -> t subst env sigma) env sigma c in
   if !mayneedglobalcheck then
     begin
       try ignore (Typing.unsafe_type_of env sigma c)
@@ -836,58 +858,79 @@ let change_on_subterm cv_pb deep t where env sigma c =
     end;
   (sigma, c)
 
-let change_in_concl occl t =
-  e_change_in_concl ((change_on_subterm Reduction.CUMUL false t occl),DEFAULTcast)
+let change_in_concl ~check occl t =
+  (* No need to check in e_change_in_concl, the check is done in change_on_subterm *)
+  e_change_in_concl ~check:false ((change_on_subterm ~check Reduction.CUMUL false t occl),DEFAULTcast)
 
-let change_in_hyp occl t id  =
-  e_change_in_hyp (fun x -> change_on_subterm Reduction.CONV x t occl) id
+let change_in_hyp ~check occl t id  =
+  (* Same as above *)
+  e_change_in_hyp ~check:false ~reorder:check (fun x -> change_on_subterm ~check Reduction.CONV x t occl) id
 
-let change_option occl t = function
-  | Some id -> change_in_hyp occl t id
-  | None -> change_in_concl occl t
+let concrete_clause_of enum_hyps cl = match cl.onhyps with
+| None ->
+  let f id = (id, AllOccurrences, InHyp) in
+  List.map f (enum_hyps ())
+| Some l ->
+  List.map (fun ((occs, id), w) -> (id, occs, w)) l
 
-let change chg c cls =
+let change ~check chg c cls =
   Proofview.Goal.enter begin fun gl ->
-    let cls = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cls in
-    Tacticals.New.tclMAP (function
-    | OnHyp (id,occs,where) ->
-       change_option (bind_change_occurrences occs chg) c (Some (id,where))
-    | OnConcl occs ->
-       change_option (bind_change_occurrences occs chg) c None)
-    cls
+    let hyps = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cls in
+    begin match cls.concl_occs with
+    | NoOccurrences -> Proofview.tclUNIT ()
+    | occs -> change_in_concl ~check (bind_change_occurrences occs chg) c
+    end
+    <*>
+    let f (id, occs, where) =
+      let occl = bind_change_occurrences occs chg in
+      let redfun deep env sigma t = change_on_subterm ~check Reduction.CONV deep c occl env sigma t in
+      let redfun env sigma d = e_pf_change_decl redfun where env sigma d in
+      (id, redfun)
+    in
+    let reorder = if check then AnyHypConv else StableHypConv in
+    (* Don't check, we do it already in [change_on_subterm] *)
+    e_change_in_hyps ~check:false ~reorder f hyps
   end
 
 let change_concl t = 
-  change_in_concl None (make_change_arg t)
+  change_in_concl ~check:true None (make_change_arg t)
 
 (* Pour usage interne (le niveau User est pris en compte par reduce) *)
-let red_in_concl        = reduct_in_concl (red_product,REVERTcast)
-let red_in_hyp          = reduct_in_hyp    red_product
-let red_option          = reduct_option   (red_product,REVERTcast)
-let hnf_in_concl        = reduct_in_concl (hnf_constr,REVERTcast)
-let hnf_in_hyp          = reduct_in_hyp    hnf_constr
-let hnf_option          = reduct_option   (hnf_constr,REVERTcast)
-let simpl_in_concl      = reduct_in_concl (simpl,REVERTcast)
-let simpl_in_hyp        = reduct_in_hyp    simpl
-let simpl_option        = reduct_option   (simpl,REVERTcast)
-let normalise_in_concl  = reduct_in_concl (compute,REVERTcast)
-let normalise_in_hyp    = reduct_in_hyp    compute
-let normalise_option    = reduct_option   (compute,REVERTcast)
-let normalise_vm_in_concl = reduct_in_concl (Redexpr.cbv_vm,VMcast)
-let unfold_in_concl loccname = reduct_in_concl (unfoldn loccname,REVERTcast)
-let unfold_in_hyp   loccname = reduct_in_hyp   (unfoldn loccname)
-let unfold_option   loccname = reduct_option (unfoldn loccname,DEFAULTcast)
-let pattern_option l = e_reduct_option (pattern_occs l,DEFAULTcast)
+let red_in_concl        = reduct_in_concl ~check:false (red_product,REVERTcast)
+let red_in_hyp          = reduct_in_hyp ~check:false ~reorder:false red_product
+let red_option          = reduct_option ~check:false (red_product,REVERTcast)
+let hnf_in_concl        = reduct_in_concl ~check:false (hnf_constr,REVERTcast)
+let hnf_in_hyp          = reduct_in_hyp ~check:false ~reorder:false hnf_constr
+let hnf_option          = reduct_option ~check:false (hnf_constr,REVERTcast)
+let simpl_in_concl      = reduct_in_concl ~check:false (simpl,REVERTcast)
+let simpl_in_hyp        = reduct_in_hyp ~check:false ~reorder:false simpl
+let simpl_option        = reduct_option ~check:false (simpl,REVERTcast)
+let normalise_in_concl  = reduct_in_concl ~check:false (compute,REVERTcast)
+let normalise_in_hyp    = reduct_in_hyp ~check:false ~reorder:false compute
+let normalise_option    = reduct_option ~check:false (compute,REVERTcast)
+let normalise_vm_in_concl = reduct_in_concl ~check:false (Redexpr.cbv_vm,VMcast)
+let unfold_in_concl loccname = reduct_in_concl ~check:false (unfoldn loccname,REVERTcast)
+let unfold_in_hyp   loccname = reduct_in_hyp ~check:false ~reorder:false (unfoldn loccname)
+let unfold_option   loccname = reduct_option ~check:false (unfoldn loccname,DEFAULTcast)
+let pattern_option l = e_reduct_option ~check:false (pattern_occs l,DEFAULTcast)
 
 (* The main reduction function *)
 
-let reduction_clause redexp cl =
-  let nbcl = List.length cl in
-  List.map (function
-    | OnHyp (id,occs,where) ->
-	(Some (id,where), bind_red_expr_occurrences occs nbcl redexp)
-    | OnConcl occs ->
-	(None, bind_red_expr_occurrences occs nbcl redexp)) cl
+let is_local_flag env flags =
+  if flags.rDelta then false
+  else
+    let check = function
+    | EvalVarRef _ -> false
+    | EvalConstRef c -> Id.Set.is_empty (Environ.vars_of_global env (ConstRef c))
+    in
+    List.for_all check flags.rConst
+
+let is_local_unfold env flags =
+  let check (_, c) = match c with
+  | EvalVarRef _ -> false
+  | EvalConstRef c -> Id.Set.is_empty (Environ.vars_of_global env (ConstRef c))
+  in
+  List.for_all check flags
 
 let reduce redexp cl =
   let trace env sigma =
@@ -897,12 +940,35 @@ let reduce redexp cl =
   in
   Proofview.Trace.name_tactic trace begin
   Proofview.Goal.enter begin fun gl ->
-  let cl' = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cl in
-  let redexps = reduction_clause redexp cl' in
+  let env = Proofview.Goal.env gl in
+  let hyps = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cl in
+  let nbcl = (if cl.concl_occs = NoOccurrences then 0 else 1) + List.length hyps in
   let check = match redexp with Fold _ | Pattern _ -> true | _ -> false in
-  Tacticals.New.tclMAP (fun (where,redexp) ->
-    e_reduct_option ~check
-      (Redexpr.reduction_of_red_expr (Tacmach.New.pf_env gl) redexp) where) redexps
+  let reorder = match redexp with
+  | Fold _ | Pattern _ -> AnyHypConv
+  | Simpl (flags, _) | Cbv flags | Cbn flags | Lazy flags ->
+    if is_local_flag env flags then LocalHypConv else StableHypConv
+  | Unfold flags ->
+    if is_local_unfold env flags then LocalHypConv else StableHypConv
+  | Red _ | Hnf | CbvVm _ | CbvNative _ -> StableHypConv
+  | ExtraRedExpr _ -> StableHypConv (* Should we be that lenient ?*)
+  in
+  begin match cl.concl_occs with
+  | NoOccurrences -> Proofview.tclUNIT ()
+  | occs ->
+    let redexp = bind_red_expr_occurrences occs nbcl redexp in
+    let redfun = Redexpr.reduction_of_red_expr env redexp in
+    e_change_in_concl ~check (revert_cast redfun)
+  end
+  <*>
+  let f (id, occs, where) =
+    let redexp = bind_red_expr_occurrences occs nbcl redexp in
+    let (redfun, _) = Redexpr.reduction_of_red_expr env redexp in
+    let redfun _ env sigma c = redfun env sigma c in
+    let redfun env sigma d = e_pf_change_decl redfun where env sigma d in
+    (id, redfun)
+  in
+  e_change_in_hyps ~check ~reorder f hyps
   end
   end
 
@@ -1297,14 +1363,11 @@ let do_replace id = function
    [Ti] and the first one (resp last one) being [G] whose hypothesis
    [id] is replaced by P using the proof given by [tac] *)
 
-let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) 
-    targetid id sigma0 clenv tac =
+let clenv_refine_in with_evars targetid id sigma0 clenv tac =
   let clenv = Clenvtac.clenv_pose_dependent_evars ~with_evars clenv in
   let clenv =
-    if with_classes then
       { clenv with evd = Typeclasses.resolve_typeclasses 
 	  ~fail:(not with_evars) clenv.env clenv.evd }
-    else clenv
   in
   let new_hyp_typ = clenv_type clenv in
   if not with_evars then check_unresolved_evars_of_metas sigma0 clenv;
@@ -1316,11 +1379,7 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true)
   let with_clear = do_replace (Some id) naming in
   Tacticals.New.tclTHEN
     (Proofview.Unsafe.tclEVARS (clear_metas clenv.evd))
-    (if sidecond_first then
-       Tacticals.New.tclTHENFIRST
-         (assert_before_then_gen with_clear naming new_hyp_typ tac) exact_tac
-     else
-       Tacticals.New.tclTHENLAST
+    (Tacticals.New.tclTHENLAST
          (assert_after_then_gen with_clear naming new_hyp_typ tac) exact_tac)
 
 (********************************************)
@@ -1355,22 +1414,25 @@ let rec contract_letin_in_lam_header sigma c =
   | LetIn (x,b,t,c) -> contract_letin_in_lam_header sigma (subst1 b c)
   | _ -> c
 
-let elimination_clause_scheme with_evars ?(with_classes=true) ?(flags=elim_flags ()) 
-    rename i (elim, elimty, bindings) indclause =
-  Proofview.Goal.enter begin fun gl ->
-  let env = Proofview.Goal.env gl in
-  let sigma = Tacmach.New.project gl in
-  let elim = contract_letin_in_lam_header sigma elim in
-  let elimclause = make_clenv_binding env sigma (elim, elimty) bindings in
-  let indmv =
-    (match EConstr.kind sigma (nth_arg sigma i elimclause.templval.rebus) with
-       | Meta mv -> mv
-       | _  -> user_err ~hdr:"elimination_clause"
-             (str "The type of elimination clause is not well-formed."))
+let elimination_in_clause_scheme env sigma with_evars ~flags
+    id hypmv elimclause =
+  let hyp = mkVar id in
+  let hyp_typ = Retyping.get_type_of env sigma hyp in
+  let hypclause = mk_clenv_from_env env sigma (Some 0) (hyp, hyp_typ) in
+  let elimclause'' =
+    (* The evarmap of elimclause is assumed to be an extension of hypclause, so
+      we do not need to merge the universes coming from hypclause. *)
+    try clenv_fchain ~with_univs:false ~flags hypmv elimclause hypclause
+    with PretypeError (env,evd,NoOccurrenceFound (op,_)) ->
+      (* Set the hypothesis name in the message *)
+      raise (PretypeError (env,evd,NoOccurrenceFound (op,Some id)))
   in
-  let elimclause' = clenv_fchain ~flags indmv elimclause indclause in
-  Clenvtac.res_pf elimclause' ~with_evars ~with_classes ~flags
-  end
+  let new_hyp_typ  = clenv_type elimclause'' in
+  if EConstr.eq_constr sigma hyp_typ new_hyp_typ then
+    user_err ~hdr:"general_rewrite_in"
+      (str "Nothing to rewrite in " ++ Id.print id ++ str".");
+  clenv_refine_in with_evars id id sigma elimclause''
+    (fun id -> Proofview.tclUNIT ())
 
 (*
  * Elimination tactic with bindings and using an arbitrary
@@ -1382,11 +1444,10 @@ let elimination_clause_scheme with_evars ?(with_classes=true) ?(flags=elim_flags
 
 type eliminator = {
   elimindex : int option;  (* None = find it automatically *)
-  elimrename : (bool * int array) option; (** None = don't rename Prop hyps with H-names *)
   elimbody : EConstr.constr with_bindings
 }
 
-let general_elim_clause_gen elimtac indclause elim =
+let general_elim_clause with_evars flags where indclause elim =
   Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
@@ -1394,7 +1455,27 @@ let general_elim_clause_gen elimtac indclause elim =
   let elimt = Retyping.get_type_of env sigma elimc in
   let i =
     match elim.elimindex with None -> index_of_ind_arg sigma elimt | Some i -> i in
-  elimtac elim.elimrename i (elimc, elimt, lbindelimc) indclause
+  let elimc = contract_letin_in_lam_header sigma elimc in
+  let elimclause = make_clenv_binding env sigma (elimc, elimt) lbindelimc in
+  let indmv =
+    (match EConstr.kind sigma (nth_arg sigma i elimclause.templval.rebus) with
+       | Meta mv -> mv
+       | _  -> user_err ~hdr:"elimination_clause"
+             (str "The type of elimination clause is not well-formed."))
+  in
+  match where with
+  | None ->
+    let elimclause = clenv_fchain ~flags indmv elimclause indclause in
+    Clenvtac.res_pf elimclause ~with_evars ~with_classes:true ~flags
+  | Some id ->
+    let hypmv =
+      match List.remove Int.equal indmv (clenv_independent elimclause) with
+      | [a] -> a
+      | _ -> user_err ~hdr:"elimination_clause"
+              (str "The type of elimination clause is not well-formed.")
+    in
+    let elimclause = clenv_fchain ~flags indmv elimclause indclause in
+    elimination_in_clause_scheme env sigma with_evars ~flags id hypmv elimclause
   end
 
 let general_elim with_evars clear_flag (c, lbindc) elim =
@@ -1403,12 +1484,12 @@ let general_elim with_evars clear_flag (c, lbindc) elim =
   let sigma = Tacmach.New.project gl in
   let ct = Retyping.get_type_of env sigma c in
   let t = try snd (reduce_to_quantified_ind env sigma ct) with UserError _ -> ct in
-  let elimtac = elimination_clause_scheme with_evars in
   let indclause  = make_clenv_binding env sigma (c, t) lbindc in
   let sigma = meta_merge sigma (clear_metas indclause.evd) in
+  let flags = elim_flags () in
   Proofview.Unsafe.tclEVARS sigma <*>
   Tacticals.New.tclTHEN
-    (general_elim_clause_gen elimtac indclause elim)
+    (general_elim_clause with_evars flags None indclause elim)
     (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c)
   end
 
@@ -1431,8 +1512,7 @@ let general_case_analysis_in_context with_evars clear_flag (c,lbindc) =
   let elim = EConstr.of_constr elim in
   Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
   (general_elim with_evars clear_flag (c,lbindc)
-   {elimindex = None; elimbody = (elim,NoBindings);
-    elimrename = Some (false, constructors_nrealdecls env (fst mind))})
+   {elimindex = None; elimbody = (elim,NoBindings); })
   end
 
 let general_case_analysis with_evars clear_flag (c,lbindc as cx) =
@@ -1463,8 +1543,7 @@ let find_eliminator c gl =
   let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl (Tacmach.New.pf_unsafe_type_of gl c) in
   if is_nonrec ind then raise IsNonrec;
   let evd, c = find_ind_eliminator ind (Tacticals.New.elimination_sort_of_goal gl) gl in
-    evd, {elimindex = None; elimbody = (c,NoBindings);
-          elimrename = Some (true, constructors_nrealdecls (Global.env()) ind)}
+    evd, { elimindex = None; elimbody = (c,NoBindings) }
 
 let default_elim with_evars clear_flag (c,_ as cx) =
   Proofview.tclORELSE
@@ -1484,7 +1563,7 @@ let default_elim with_evars clear_flag (c,_ as cx) =
 let elim_in_context with_evars clear_flag c = function
   | Some elim ->
       general_elim with_evars clear_flag c
-        {elimindex = Some (-1); elimbody = elim; elimrename = None}
+        { elimindex = Some (-1); elimbody = elim }
   | None -> default_elim with_evars clear_flag c
 
 let elim with_evars clear_flag (c,lbindc as cx) elim =
@@ -1510,48 +1589,6 @@ let simplest_elim c = default_elim false None (c,NoBindings)
    (e.g. it could replace id:A->B->C by id:C, knowing A/\B)
 *)
 
-let clenv_fchain_in id ?(flags=elim_flags ()) mv elimclause hypclause =
-  (* The evarmap of elimclause is assumed to be an extension of hypclause, so
-     we do not need to merge the universes coming from hypclause. *)
-  try clenv_fchain ~with_univs:false ~flags mv elimclause hypclause
-  with PretypeError (env,evd,NoOccurrenceFound (op,_)) ->
-    (* Set the hypothesis name in the message *)
-    raise (PretypeError (env,evd,NoOccurrenceFound (op,Some id)))
-
-let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) 
-    id rename i (elim, elimty, bindings) indclause =
-  Proofview.Goal.enter begin fun gl ->
-  let env = Proofview.Goal.env gl in
-  let sigma = Tacmach.New.project gl in
-  let elim = contract_letin_in_lam_header sigma elim in
-  let elimclause = make_clenv_binding env sigma (elim, elimty) bindings in
-  let indmv = destMeta sigma (nth_arg sigma i elimclause.templval.rebus) in
-  let hypmv =
-    match List.remove Int.equal indmv (clenv_independent elimclause) with
-    | [a] -> a
-    | _ -> user_err ~hdr:"elimination_clause"
-             (str "The type of elimination clause is not well-formed.")
-  in
-  let elimclause'  = clenv_fchain ~flags indmv elimclause indclause in
-  let hyp = mkVar id in
-  let hyp_typ = Retyping.get_type_of env sigma hyp in
-  let hypclause = mk_clenv_from_env env sigma (Some 0) (hyp, hyp_typ) in
-  let elimclause'' = clenv_fchain_in id ~flags hypmv elimclause' hypclause in
-  let new_hyp_typ  = clenv_type elimclause'' in
-  if EConstr.eq_constr sigma hyp_typ new_hyp_typ then
-    user_err ~hdr:"general_rewrite_in"
-      (str "Nothing to rewrite in " ++ Id.print id ++ str".");
-  clenv_refine_in with_evars id id sigma elimclause''
-    (fun id -> Proofview.tclUNIT ())
-  end
-
-let general_elim_clause with_evars flags id c e =
-  let elim = match id with
-  | None -> elimination_clause_scheme with_evars ~with_classes:true ~flags
-  | Some id -> elimination_in_clause_scheme with_evars ~flags id
-  in
-  general_elim_clause_gen elim c e
-
 (* Apply a tactic below the products of the conclusion of a lemma *)
 
 type conjunction_status =
@@ -1823,7 +1860,7 @@ let apply_in_once_main flags innerclause env sigma (loc,d,lbind) =
   in
   aux (make_clenv_binding env sigma (d,thm) lbind)
 
-let apply_in_once ?(respect_opaque = false) sidecond_first with_delta
+let apply_in_once ?(respect_opaque = false) with_delta
     with_destruct with_evars naming id (clear_flag,{ CAst.loc; v= d,lbind}) tac =
   let open Context.Rel.Declaration in
   Proofview.Goal.enter begin fun gl ->
@@ -1844,7 +1881,7 @@ let apply_in_once ?(respect_opaque = false) sidecond_first with_delta
       if with_delta then default_unify_flags () else default_no_delta_unify_flags ts in
     try
       let clause = apply_in_once_main flags innerclause env sigma (loc,c,lbind) in
-      clenv_refine_in ~sidecond_first with_evars targetid id sigma clause
+      clenv_refine_in with_evars targetid id sigma clause
         (fun id ->
           Tacticals.New.tclTHENLIST [
             apply_clear_request clear_flag false c;
@@ -1861,14 +1898,14 @@ let apply_in_once ?(respect_opaque = false) sidecond_first with_delta
   aux [] with_destruct d
   end
 
-let apply_in_delayed_once ?(respect_opaque = false) sidecond_first with_delta
+let apply_in_delayed_once ?(respect_opaque = false) with_delta
     with_destruct with_evars naming id (clear_flag,{CAst.loc;v=f}) tac =
   Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
     let (sigma, c) = f env sigma in
     Tacticals.New.tclWITHHOLES with_evars 
-      (apply_in_once ~respect_opaque sidecond_first with_delta with_destruct with_evars
+      (apply_in_once ~respect_opaque with_delta with_destruct with_evars
          naming id (clear_flag,CAst.(make ?loc c)) tac)
       sigma
   end
@@ -2174,7 +2211,7 @@ let constructor_tac with_evars expctdnumopt i lbind =
     let nconstr = Array.length (snd (Global.lookup_inductive ind)).mind_consnames in
     check_number_of_constructors expctdnumopt i nconstr;
     Tacticals.New.tclTHENLIST [
-      convert_concl_no_check redcl DEFAULTcast;
+      convert_concl ~check:false redcl DEFAULTcast;
       intros;
       constructor_core with_evars (ind, i) lbind
     ]
@@ -2203,7 +2240,7 @@ let any_constructor with_evars tacopt =
       Array.length (snd (Global.lookup_inductive ind)).mind_consnames in
     if Int.equal nconstr 0 then error "The type has no constructors.";
     Tacticals.New.tclTHENLIST [
-      convert_concl_no_check redcl DEFAULTcast;
+      convert_concl ~check:false redcl DEFAULTcast;
       intros;
       any_constr ind nconstr 1 ()
     ]
@@ -2488,7 +2525,7 @@ and intro_pattern_action ?loc with_evars b style pat thin destopt tac id =
           clear [id] in
       let f env sigma = let (sigma, c) = f env sigma in (sigma,(c, NoBindings))
       in
-      apply_in_delayed_once false true true with_evars naming id (None,CAst.make ?loc:loc' f)
+      apply_in_delayed_once true true with_evars naming id (None,CAst.make ?loc:loc' f)
         (fun id -> Tacticals.New.tclTHENLIST [doclear; tac_ipat id; tac thin None []])
 
 and prepare_intros ?loc with_evars dft destopt = function
@@ -2556,10 +2593,10 @@ let assert_as first hd ipat t =
 
 (* apply in as *)
 
-let general_apply_in ?(respect_opaque=false) sidecond_first with_delta
+let general_apply_in ?(respect_opaque=false) with_delta
     with_destruct with_evars id lemmas ipat =
   let tac (naming,lemma) tac id =
-    apply_in_delayed_once ~respect_opaque sidecond_first with_delta
+    apply_in_delayed_once ~respect_opaque with_delta
       with_destruct with_evars naming id lemma tac in
   Proofview.Goal.enter begin fun gl ->
   let destopt =
@@ -2588,10 +2625,10 @@ let general_apply_in ?(respect_opaque=false) sidecond_first with_delta
 
 let apply_in simple with_evars id lemmas ipat =
   let lemmas = List.map (fun (k,{CAst.loc;v=l}) -> k, CAst.make ?loc (fun _ sigma -> (sigma,l))) lemmas in
-  general_apply_in false simple simple with_evars id lemmas ipat
+  general_apply_in simple simple with_evars id lemmas ipat
 
 let apply_delayed_in simple with_evars id lemmas ipat =
-  general_apply_in ~respect_opaque:true false simple simple with_evars id lemmas ipat
+  general_apply_in ~respect_opaque:true simple simple with_evars id lemmas ipat
 
 (*****************************)
 (* Tactics abstracting terms *)
@@ -2647,9 +2684,9 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty =
     in
       Tacticals.New.tclTHENLIST
       [ Proofview.Unsafe.tclEVARS sigma;
-        convert_concl_no_check newcl DEFAULTcast;
+        convert_concl ~check:false newcl DEFAULTcast;
         intro_gen (NamingMustBe (CAst.make id)) (decode_hyp lastlhyp) true false;
-        Tacticals.New.tclMAP convert_hyp_no_check depdecls;
+        Tacticals.New.tclMAP (convert_hyp ~check:false ~reorder:false) depdecls;
         eq_tac ]
   end
 
@@ -2858,17 +2895,21 @@ let generalize_dep ?(with_let=false) c =
       | _ -> tothin
   in
   let cl' = it_mkNamedProd_or_LetIn (pf_concl gl) to_quantify in
-  let body =
-    if with_let then
-      match EConstr.kind sigma c with
-      | Var id -> id |> (fun id -> pf_get_hyp id gl) |> NamedDecl.get_value
-      | _ -> None
-    else None
+  let is_var, body = match EConstr.kind sigma c with
+  | Var id ->
+    let body = NamedDecl.get_value (pf_get_hyp id gl) in
+    let is_var = Option.is_empty body && not (List.mem id init_ids) in
+    if with_let then is_var, body else is_var, None
+  | _ -> false, None
   in
   let cl'',evd = generalize_goal gl 0 ((AllOccurrences,c,body),Anonymous)
     (cl',project gl) in
   (* Check that the generalization is indeed well-typed *)
-  let (evd, _) = Typing.type_of env evd cl'' in
+  let evd =
+    (* No need to retype for variables, term is statically well-typed *)
+    if is_var then evd
+    else fst (Typing.type_of env evd cl'')
+  in
   let args = Context.Named.to_instance mkVar to_quantify_rev in
   tclTHENLIST
     [ Proofview.Unsafe.tclEVARS evd;
@@ -3052,8 +3093,8 @@ let unfold_body x =
   Tacticals.New.afterHyp x begin fun aft ->
   let hl = List.fold_right (fun decl cl -> (NamedDecl.get_id decl, InHyp) :: cl) aft [] in
   let rfun _ _ c = replace_vars [x, xval] c in
-  let reducth h = reduct_in_hyp rfun h in
-  let reductc = reduct_in_concl (rfun, DEFAULTcast) in
+  let reducth h = reduct_in_hyp ~check:false ~reorder:false rfun h in
+  let reductc = reduct_in_concl ~check:false (rfun, DEFAULTcast) in
   Tacticals.New.tclTHENLIST [Tacticals.New.tclMAP reducth hl; reductc]
   end
   end
@@ -3282,7 +3323,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac =
     if Int.equal i nparams then
       let t = applist (hd, params@args) in
       Tacticals.New.tclTHEN
-        (change_in_hyp None (make_change_arg t) (hyp0,InHypTypeOnly))
+        (change_in_hyp ~check:false None (make_change_arg t) (hyp0,InHypTypeOnly))
         (tac avoid)
     else
       let c = List.nth argl (i-1) in
@@ -4174,7 +4215,7 @@ let find_induction_type isrec elim hyp0 gl =
 	let scheme = compute_elim_sig sigma ~elimc elimt in
 	if Option.is_empty scheme.indarg then error "Cannot find induction type";
 	let indsign = compute_scheme_signature evd scheme hyp0 ind_guess in
-	let elim = ({elimindex = Some(-1); elimbody = elimc; elimrename = None},elimt) in
+        let elim = ({ elimindex = Some(-1); elimbody = elimc },elimt) in
 	scheme, ElimUsing (elim,indsign)
   in
   match scheme.indref with
@@ -4201,10 +4242,7 @@ let get_eliminator elim dep s gl =
   | ElimOver (isrec,id) ->
       let evd, (elimc,elimt),_ as elims = guess_elim isrec dep s id gl in
       let _, (l, s) = compute_elim_signature elims id in
-      let branchlengthes = List.map (fun d -> assert (RelDecl.is_local_assum d); pi1 (decompose_prod_letin (Tacmach.New.project gl) (RelDecl.get_type d)))
-                                    (List.rev s.branches)
-      in
-      evd, isrec, ({elimindex = None; elimbody = elimc; elimrename = Some (isrec,Array.of_list branchlengthes)}, elimt), l
+      evd, isrec, ({ elimindex = None; elimbody = elimc }, elimt), l
 
 (* Instantiate all meta variables of elimclause using lid, some elts
    of lid are parameters (first ones), the other are
@@ -4248,7 +4286,7 @@ let recolle_clenv i params args elimclause gl =
 let induction_tac with_evars params indvars elim =
   Proofview.Goal.enter begin fun gl ->
   let sigma = Tacmach.New.project gl in
-  let ({elimindex=i;elimbody=(elimc,lbindelimc);elimrename=rename},elimt) = elim in
+  let ({ elimindex=i;elimbody=(elimc,lbindelimc) },elimt) = elim in
   let i = match i with None -> index_of_ind_arg sigma elimt | Some i -> i in
   (* elimclause contains this: (elimc ?i ?j ?k...?l) *)
   let elimc = contract_letin_in_lam_header sigma elimc in
@@ -4353,7 +4391,7 @@ let induction_without_atomization isrec with_evars elim names lid =
     (* FIXME: Tester ca avec un principe dependant et non-dependant *)
     induction_tac with_evars params realindvars elim;
   ] in
-  let elim = ElimUsing (({elimindex = Some (-1); elimbody = Option.get scheme.elimc; elimrename = None}, scheme.elimt), indsign) in
+  let elim = ElimUsing (({ elimindex = Some (-1); elimbody = Option.get scheme.elimc }, scheme.elimt), indsign) in
   apply_induction_in_context with_evars None [] elim indvars names induct_tac
   end
 
@@ -4799,7 +4837,7 @@ let symmetry_red allowred =
   match with_eqn with
   | Some eq_data,_,_ ->
       Tacticals.New.tclTHEN
-        (convert_concl_no_check concl DEFAULTcast)
+        (convert_concl ~check:false concl DEFAULTcast)
         (Tacticals.New.pf_constr_of_global eq_data.sym >>= apply)
   | None,eq,eq_kind -> prove_symmetry eq eq_kind
   end
@@ -4894,7 +4932,7 @@ let transitivity_red allowred t =
   match with_eqn with
   | Some eq_data,_,_ ->
       Tacticals.New.tclTHEN
-        (convert_concl_no_check concl DEFAULTcast)
+        (convert_concl ~check:false concl DEFAULTcast)
         (match t with
 	  | None -> Tacticals.New.pf_constr_of_global eq_data.trans >>= eapply
 	  | Some t -> Tacticals.New.pf_constr_of_global eq_data.trans >>= fun trans -> apply_list [trans; t])
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 75b5caaa36..32c64bacf6 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -33,10 +33,12 @@ val is_quantified_hypothesis : Id.t -> Proofview.Goal.t -> bool
 (** {6 Primitive tactics. } *)
 
 val introduction    : Id.t -> unit Proofview.tactic
-val convert_concl   : ?check:bool -> types -> cast_kind -> unit Proofview.tactic
-val convert_hyp     : ?check:bool -> named_declaration -> unit Proofview.tactic
+val convert_concl   : check:bool -> types -> cast_kind -> unit Proofview.tactic
+val convert_hyp     : check:bool -> reorder:bool -> named_declaration -> unit Proofview.tactic
 val convert_concl_no_check : types -> cast_kind -> unit Proofview.tactic
+[@@ocaml.deprecated "use [Tactics.convert_concl]"]
 val convert_hyp_no_check : named_declaration -> unit Proofview.tactic
+[@@ocaml.deprecated "use [Tactics.convert_hyp]"]
 val mutual_fix      :
   Id.t -> int -> (Id.t * int * constr) list -> int -> unit Proofview.tactic
 val fix             : Id.t -> int -> unit Proofview.tactic
@@ -150,13 +152,13 @@ type e_tactic_reduction = Reductionops.e_reduction_function
 type change_arg = patvar_map -> env -> evar_map -> evar_map * constr
 
 val make_change_arg   : constr -> change_arg
-val reduct_in_hyp     : ?check:bool -> tactic_reduction -> hyp_location -> unit Proofview.tactic
-val reduct_option     : ?check:bool -> tactic_reduction * cast_kind -> goal_location -> unit Proofview.tactic
-val reduct_in_concl   : tactic_reduction * cast_kind -> unit Proofview.tactic
+val reduct_in_hyp     : check:bool -> reorder:bool -> tactic_reduction -> hyp_location -> unit Proofview.tactic
+val reduct_option     : check:bool -> tactic_reduction * cast_kind -> goal_location -> unit Proofview.tactic
+val reduct_in_concl   : check:bool -> tactic_reduction * cast_kind -> unit Proofview.tactic
 val e_reduct_in_concl   : check:bool -> e_tactic_reduction * cast_kind -> unit Proofview.tactic
-val change_in_concl   : (occurrences * constr_pattern) option -> change_arg -> unit Proofview.tactic
+val change_in_concl   : check:bool -> (occurrences * constr_pattern) option -> change_arg -> unit Proofview.tactic
 val change_concl      : constr -> unit Proofview.tactic
-val change_in_hyp     : (occurrences * constr_pattern) option -> change_arg ->
+val change_in_hyp     : check:bool -> (occurrences * constr_pattern) option -> change_arg ->
                         hyp_location -> unit Proofview.tactic
 val red_in_concl      : unit Proofview.tactic
 val red_in_hyp        : hyp_location -> unit Proofview.tactic
@@ -178,7 +180,7 @@ val unfold_in_hyp     :
 val unfold_option     :
   (occurrences * evaluable_global_reference) list -> goal_location -> unit Proofview.tactic
 val change            :
-  constr_pattern option -> change_arg -> clause -> unit Proofview.tactic
+  check:bool -> constr_pattern option -> change_arg -> clause -> unit Proofview.tactic
 val pattern_option    :
   (occurrences * constr) list -> goal_location -> unit Proofview.tactic
 val reduce            : red_expr -> clause -> unit Proofview.tactic
@@ -280,7 +282,6 @@ val compute_elim_sig : evar_map -> ?elimc:constr with_bindings -> types -> elim_
 (** elim principle with the index of its inductive arg *)
 type eliminator = {
   elimindex : int option;  (** None = find it automatically *)
-  elimrename : (bool * int array) option; (** None = don't rename Prop hyps with H-names *)
   elimbody : constr with_bindings
 }