Imported Upstream version 8.5~beta3+dfsg

1 files changed, 233 insertions, 144 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 7484139c..2a46efd8 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -109,6 +109,44 @@ let _ =
       optread  = (fun () -> !clear_hyp_by_default) ;
       optwrite = (fun b -> clear_hyp_by_default := b) }
 
+(* Compatibility option useful in developments using apply intensively
+   in ltac code *)
+
+let universal_lemma_under_conjunctions = ref false
+
+let accept_universal_lemma_under_conjunctions () =
+  !universal_lemma_under_conjunctions
+
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "trivial unification in tactics applying under conjunctions";
+      optkey   = ["Universal";"Lemma";"Under";"Conjunction"];
+      optread  = (fun () -> !universal_lemma_under_conjunctions) ;
+      optwrite = (fun b -> universal_lemma_under_conjunctions := b) }
+
+(* The following boolean governs what "intros []" do on examples such
+   as "forall x:nat*nat, x=x"; if true, it behaves as "intros [? ?]";
+   if false, it behaves as "intro H; case H; clear H" for fresh H.
+   Kept as false for compatibility.
+ *)
+
+let bracketing_last_or_and_intro_pattern = ref false
+
+let use_bracketing_last_or_and_intro_pattern () =
+  !bracketing_last_or_and_intro_pattern
+  && Flags.version_strictly_greater Flags.V8_4
+
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "bracketing last or-and introduction pattern";
+      optkey   = ["Bracketing";"Last";"Introduction";"Pattern"];
+      optread  = (fun () -> !bracketing_last_or_and_intro_pattern) ;
+      optwrite = (fun b -> bracketing_last_or_and_intro_pattern := b) }
+
 (*********************************************)
 (*                 Tactics                   *)
 (*********************************************)
@@ -139,7 +177,8 @@ let introduction ?(check=true) id =
     let store = Proofview.Goal.extra gl in
     let env = Proofview.Goal.env gl in
     let () = if check && mem_named_context id hyps then
-      error ("Variable " ^ Id.to_string id ^ " is already declared.")
+      errorlabstrm "Tactics.introduction"
+        (str "Variable " ++ pr_id id ++ str " is already declared.")
     in
     match kind_of_term (whd_evar sigma concl) with
     | Prod (_, t, b) -> unsafe_intro env store (id, None, t) b
@@ -157,7 +196,7 @@ let convert_concl ?(check=true) ty k =
     Proofview.Refine.refine ~unsafe:true begin fun sigma ->
       let sigma =
         if check then begin
-          ignore (Typing.type_of env sigma ty);
+          ignore (Typing.unsafe_type_of env sigma ty);
           let sigma,b = Reductionops.infer_conv env sigma ty conclty in
           if not b then error "Not convertible.";
           sigma
@@ -184,8 +223,9 @@ let convert_hyp_no_check = convert_hyp ~check:false
 let convert_gen pb x y =
   Proofview.Goal.enter begin fun gl ->
     try
-      let sigma = Tacmach.New.pf_apply Evd.conversion gl pb x y in
-      Proofview.Unsafe.tclEVARS sigma
+      let sigma, b = Tacmach.New.pf_apply (Reductionops.infer_conv ~pb) gl x y in
+      if b then Proofview.Unsafe.tclEVARS sigma
+      else Tacticals.New.tclFAIL 0 (str "Not convertible")
     with (* Reduction.NotConvertible *) _ ->
       (** FIXME: Sometimes an anomaly is raised from conversion *)
       Tacticals.New.tclFAIL 0 (str "Not convertible")
@@ -627,7 +667,7 @@ let change_on_subterm cv_pb deep t where env sigma c =
         env sigma c in
   if !mayneedglobalcheck then
     begin
-      try ignore (Typing.type_of env sigma c)
+      try ignore (Typing.unsafe_type_of env sigma c)
       with e when catchable_exception e ->
         error "Replacement would lead to an ill-typed term."
     end;
@@ -687,12 +727,11 @@ let reduction_clause redexp cl =
 let reduce redexp cl goal =
   let cl = concrete_clause_of (fun () -> pf_ids_of_hyps goal) cl in
   let redexps = reduction_clause redexp cl in
+  let check = match redexp with Fold _ | Pattern _ -> true | _ -> false in
   let tac = tclMAP (fun (where,redexp) ->
-    e_reduct_option ~check:true
+    e_reduct_option ~check
       (Redexpr.reduction_of_red_expr (pf_env goal) redexp) where) redexps in
-  match redexp with
-  | Fold _ | Pattern _ -> with_check tac goal
-  | _ -> tac goal
+  if check then with_check tac goal else tac goal
 
 (* Unfolding occurrences of a constant *)
 
@@ -751,8 +790,7 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
 	     (intro_then_gen name_flag move_flag false dep_flag tac))
           begin function (e, info) -> match e with
             | RefinerError IntroNeedsProduct ->
-                Proofview.tclZERO 
-		  (Errors.UserError("Intro",str "No product even after head-reduction."))
+                Tacticals.New.tclZEROMSG (str "No product even after head-reduction.")
             | e -> Proofview.tclZERO ~info e
           end
   end
@@ -800,16 +838,23 @@ let intro_forthcoming_then_gen name_flag move_flag dep_flag n bound tac =
   aux n []
 
 let get_next_hyp_position id gl =
-  let rec get_next_hyp_position id = function
+  let rec aux = function
   | [] -> raise (RefinerError (NoSuchHyp id))
   | (hyp,_,_) :: right ->
     if Id.equal hyp id then
       match right with (id,_,_)::_ -> MoveBefore id | [] -> MoveLast
     else
-      get_next_hyp_position id right
+      aux right
+  in
+  aux (Proofview.Goal.hyps (Proofview.Goal.assume gl))
+
+let get_previous_hyp_position id gl =
+  let rec aux dest = function
+  | [] -> raise (RefinerError (NoSuchHyp id))
+  | (hyp,_,_) :: right ->
+    if Id.equal hyp id then dest else aux (MoveAfter hyp) right
   in
-  let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
-  get_next_hyp_position id hyps
+  aux MoveLast (Proofview.Goal.hyps (Proofview.Goal.assume gl))
 
 let intro_replacing id =
   Proofview.Goal.enter begin fun gl ->
@@ -979,7 +1024,7 @@ let cut c =
     let is_sort =
       try
         (** Backward compat: ensure that [c] is well-typed. *)
-        let typ = Typing.type_of env sigma c in
+        let typ = Typing.unsafe_type_of env sigma c in
         let typ = whd_betadeltaiota env sigma typ in
         match kind_of_term typ with
         | Sort _ -> true
@@ -1224,7 +1269,7 @@ let find_ind_eliminator ind s gl =
     evd, c
 
 let find_eliminator c gl =
-  let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl (Tacmach.New.pf_type_of gl c) in
+  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);
@@ -1332,7 +1377,7 @@ let make_projection env sigma params cstr sign elim i n c u =
 	(* to avoid surprising unifications, excludes flexible
 	projection types or lambda which will be instantiated by Meta/Evar *)
 	&& not (isEvar (fst (whd_betaiota_stack sigma t)))
-	&& not (isRel t && destRel t > n-i)
+	&& (accept_universal_lemma_under_conjunctions () || not (isRel t))
       then
         let t = lift (i+1-n) t in
 	let abselim = beta_applist (elim,params@[t;branch]) in
@@ -1358,7 +1403,7 @@ let make_projection env sigma params cstr sign elim i n c u =
       | None -> None
   in elim
 
-let descend_in_conjunctions avoid tac exit c =
+let descend_in_conjunctions avoid tac (err, info) c =
   Proofview.Goal.nf_enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
@@ -1392,9 +1437,8 @@ let descend_in_conjunctions avoid tac exit c =
 		 (* Might be ill-typed due to forbidden elimination. *)
 		 Tacticals.New.onLastHypId (tac (not isrec))]
            end))
-    | None ->
-	raise Exit
-  with RefinerError _|UserError _|Exit -> exit ()
+    | None -> Proofview.tclZERO ~info err
+  with RefinerError _|UserError _ -> Proofview.tclZERO ~info err
   end
 
 (****************************************************)
@@ -1417,7 +1461,15 @@ let solve_remaining_apply_goals =
     with Not_found -> Proofview.tclUNIT ()
   else Proofview.tclUNIT ()
   end
-  
+
+let tclORELSEOPT t k =
+  Proofview.tclORELSE t
+    (fun e -> match k e with
+    | None ->
+      let (e, info) = e in
+      Proofview.tclZERO ~info e
+    | Some tac -> tac)
+
 let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind)) =
   Proofview.Goal.nf_enter begin fun gl ->
   let concl = Proofview.Goal.concl gl in
@@ -1442,50 +1494,46 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind))
       with UserError _ as exn ->
         Proofview.tclZERO exn
     in
-    Proofview.tclORELSE
+    let rec try_red_apply thm_ty (exn0, info) =
+      try
+        (* Try to head-reduce the conclusion of the theorem *)
+        let red_thm = try_red_product env sigma thm_ty in
+        tclORELSEOPT
+          (try_apply red_thm concl_nprod)
+          (function (e, info) -> match e with
+          | PretypeError _|RefinerError _|UserError _|Failure _ ->
+            Some (try_red_apply red_thm (exn0, info))
+          | _ -> None)
+      with Redelimination ->
+        (* Last chance: if the head is a variable, apply may try
+            second order unification *)
+        let info = Loc.add_loc info loc in
+        let tac =
+          if with_destruct then
+            descend_in_conjunctions []
+              (fun b id ->
+                Tacticals.New.tclTHEN
+                  (try_main_apply b (mkVar id))
+                  (Proofview.V82.tactic (thin [id])))
+              (exn0, info) c
+          else
+            Proofview.tclZERO ~info exn0 in
+        if not (Int.equal concl_nprod 0) then
+          tclORELSEOPT
+            (try_apply thm_ty 0)
+            (function (e, info) -> match e with
+            | PretypeError _|RefinerError _|UserError _|Failure _->
+              Some tac
+            | _ -> None)
+        else
+          tac
+    in
+    tclORELSEOPT
       (try_apply thm_ty0 concl_nprod)
       (function (e, info) -> match e with
-        | PretypeError _|RefinerError _|UserError _|Failure _ as exn0 ->
-	let rec try_red_apply thm_ty =
-          try 
-            (* Try to head-reduce the conclusion of the theorem *)
-            let red_thm = try_red_product env sigma thm_ty in
-            Proofview.tclORELSE
-              (try_apply red_thm concl_nprod)
-              (function (e, info) -> match e with
-              | PretypeError _|RefinerError _|UserError _|Failure _ ->
-		try_red_apply red_thm
-              | exn -> iraise (exn, info))
-          with Redelimination ->
-            (* Last chance: if the head is a variable, apply may try
-	       second order unification *)
-            let tac =
-	      if with_destruct then
-                descend_in_conjunctions []
-                  (fun b id ->
-                    Tacticals.New.tclTHEN
-                      (try_main_apply b (mkVar id))
-                      (Proofview.V82.tactic (thin [id])))
-                  (fun _ ->
-                    let info = Loc.add_loc info loc in
-                    Proofview.tclZERO ~info exn0) c
-	      else
-                let info = Loc.add_loc info loc in
-		Proofview.tclZERO ~info exn0 in
-            if not (Int.equal concl_nprod 0) then
-              try
-                Proofview.tclORELSE
-                  (try_apply thm_ty 0)
-                  (function (e, info) -> match e with
-                  | PretypeError _|RefinerError _|UserError _|Failure _->
-                    tac
-                  | exn -> iraise (exn, info))
-              with UserError _ | Exit ->
-                tac
-            else
-              tac
-	in try_red_apply thm_ty0
-      | exn -> iraise (exn, info))
+      | PretypeError _|RefinerError _|UserError _|Failure _ ->
+        Some (try_red_apply thm_ty0 (e, info))
+      | _ -> None)
     end
   in
     Tacticals.New.tclTHENLIST [
@@ -1596,10 +1644,10 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming
             tac id
           ])
     with e when with_destruct && Errors.noncritical e ->
-      let e = Errors.push e in
+      let (e, info) = Errors.push e in
         (descend_in_conjunctions [targetid]
            (fun b id -> aux (id::idstoclear) b (mkVar id))
-           (fun _ -> iraise e) c)
+           (e, info) c)
     end
   in
   aux [] with_destruct d
@@ -1636,7 +1684,7 @@ let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars nam
 
 let cut_and_apply c =
   Proofview.Goal.nf_enter begin fun gl ->
-    match kind_of_term (Tacmach.New.pf_hnf_constr gl (Tacmach.New.pf_type_of gl c)) with
+    match kind_of_term (Tacmach.New.pf_hnf_constr gl (Tacmach.New.pf_unsafe_type_of gl c)) with
       | Prod (_,c1,c2) when not (dependent (mkRel 1) c2) ->
         let concl = Proofview.Goal.concl gl in
         let env = Tacmach.New.pf_env gl in
@@ -1669,7 +1717,7 @@ let exact_check c =
   let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
-  let sigma, ct = Typing.e_type_of env sigma c in
+  let sigma, ct = Typing.type_of env sigma c in
     Proofview.Unsafe.tclEVARS sigma <*>
       Tacticals.New.tclTHEN (convert_leq ct concl) (new_exact_no_check c)
   end
@@ -1818,7 +1866,7 @@ let specialize (c,lbind) g =
       let evd = Typeclasses.resolve_typeclasses (pf_env g) (project g) in
 	tclEVARS evd, nf_evar evd c
     else
-      let clause = pf_apply make_clenv_binding g (c,pf_type_of g c) lbind in
+      let clause = pf_apply make_clenv_binding g (c,pf_unsafe_type_of g c) lbind in
       let flags = { (default_unify_flags ()) with resolve_evars = true } in
       let clause = clenv_unify_meta_types ~flags clause in
       let (thd,tstack) = whd_nored_stack clause.evd (clenv_value clause) in
@@ -1838,11 +1886,11 @@ let specialize (c,lbind) g =
        | Var id when Id.List.mem id (pf_ids_of_hyps g) ->
 	   tclTHEN tac
 	     (tclTHENFIRST
-	       (fun g -> Proofview.V82.of_tactic (assert_before_replacing id (pf_type_of g term)) g)
+	       (fun g -> Proofview.V82.of_tactic (assert_before_replacing id (pf_unsafe_type_of g term)) g)
 	       (exact_no_check term)) g
        | _ -> tclTHEN tac
 	   (tclTHENLAST
-              (fun g -> Proofview.V82.of_tactic (cut (pf_type_of g term)) g)
+              (fun g -> Proofview.V82.of_tactic (cut (pf_unsafe_type_of g term)) g)
               (exact_no_check term)) g
 
 (* Keeping only a few hypotheses *)
@@ -1871,8 +1919,8 @@ let check_number_of_constructors expctdnumopt i nconstr =
   if Int.equal i 0 then error "The constructors are numbered starting from 1.";
   begin match expctdnumopt with
     | Some n when not (Int.equal n nconstr) ->
-	error ("Not an inductive goal with "^
-	       string_of_int n ^ String.plural n " constructor"^".")
+	errorlabstrm "Tactics.check_number_of_constructors"
+          (str "Not an inductive goal with " ++ int n ++ str (String.plural n " constructor") ++ str ".")
     | _ -> ()
   end;
   if i > nconstr then error "Not enough constructors."
@@ -1977,7 +2025,7 @@ let my_find_eq_data_decompose gl t =
 let intro_decomp_eq loc l thin tac id =
   Proofview.Goal.nf_enter begin fun gl ->
   let c = mkVar id in
-  let t = Tacmach.New.pf_type_of gl c in
+  let t = Tacmach.New.pf_unsafe_type_of gl c in
   let _,t = Tacmach.New.pf_reduce_to_quantified_ind gl t in
   match my_find_eq_data_decompose gl t with
   | Some (eq,u,eq_args) ->
@@ -1991,7 +2039,7 @@ let intro_decomp_eq loc l thin tac id =
 let intro_or_and_pattern loc bracketed ll thin tac id =
   Proofview.Goal.enter begin fun gl ->
   let c = mkVar id in
-  let t = Tacmach.New.pf_type_of gl c in
+  let t = Tacmach.New.pf_unsafe_type_of gl c in
   let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl t in
   let nv = constructors_nrealargs ind in
   let ll = fix_empty_or_and_pattern (Array.length nv) ll in
@@ -2010,7 +2058,7 @@ let rewrite_hyp assert_style l2r id =
   let clear_var_and_eq c = tclTHEN (clear [id]) (clear [destVar c]) in
   Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
-    let type_of = Tacmach.New.pf_type_of gl in
+    let type_of = Tacmach.New.pf_unsafe_type_of gl in
     let whd_betadeltaiota = Tacmach.New.pf_apply whd_betadeltaiota gl in
     let t = whd_betadeltaiota (type_of (mkVar id)) in
     match match_with_equality_type t with
@@ -2074,7 +2122,7 @@ let make_tmp_naming avoid l = function
      case of IntroFresh, we should use check_thin_clash_then anyway to
      prevent the case of an IntroFresh precisely using the wild_id *)
   | IntroWildcard -> NamingBasedOn (wild_id,avoid@explicit_intro_names l)
-  | _ -> NamingAvoid(avoid@explicit_intro_names l)
+  | pat -> NamingAvoid(avoid@explicit_intro_names ((dloc,IntroAction pat)::l))
 
 let fit_bound n = function
   | None -> true
@@ -2088,6 +2136,21 @@ let exceed_bound n = function
      to ensure that dependent hypotheses are cleared in the right
      dependency order (see bug #1000); we use fresh names, not used in
      the tactic, for the hyps to clear *)
+  (* In [intro_patterns_core b avoid ids thin destopt bound n tac patl]:
+     [b]: compatibility flag, if false at toplevel, do not complete incomplete
+          trailing toplevel or_and patterns (as in "intros []", see
+          [bracketing_last_or_and_intro_pattern])
+     [avoid]: names to avoid when creating an internal name
+     [ids]: collect introduced names for possible use by the [tac] continuation
+     [thin]: collect names to erase at the end
+     [destopt]: position in the context where to introduce the hypotheses
+     [bound]: number of pending intros to do in the current or-and pattern,
+              with remembering of [b] flag if at toplevel
+     [n]: number of introduction done in the current or-and pattern
+     [tac]: continuation tactic
+     [patl]: introduction patterns to interpret
+  *)
+
 let rec intro_patterns_core b avoid ids thin destopt bound n tac = function
   | [] when fit_bound n bound ->
       tac ids thin
@@ -2105,31 +2168,33 @@ let rec intro_patterns_core b avoid ids thin destopt bound n tac = function
           (n+List.length ids) tac l)
   | IntroAction pat ->
       intro_then_gen (make_tmp_naming avoid l pat)
-	MoveLast true false
+	destopt true false
         (intro_pattern_action loc (b || not (List.is_empty l)) false pat thin
+          destopt
           (fun thin bound' -> intro_patterns_core b avoid ids thin destopt bound' 0
             (fun ids thin ->
               intro_patterns_core b avoid ids thin destopt bound (n+1) tac l)))
   | IntroNaming pat ->
-      intro_pattern_naming loc b avoid ids pat thin destopt bound n tac l
+      intro_pattern_naming loc b avoid ids pat thin destopt bound (n+1) tac l
 
+  (* Pi-introduction rule, used backwards *)
 and intro_pattern_naming loc b avoid ids pat thin destopt bound n tac l =
   match pat with
   | IntroIdentifier id ->
       check_thin_clash_then id thin avoid (fun thin ->
         intro_then_gen (NamingMustBe (loc,id)) destopt true false
-          (fun id -> intro_patterns_core b avoid (id::ids) thin destopt bound (n+1) tac l))
+          (fun id -> intro_patterns_core b avoid (id::ids) thin destopt bound n tac l))
   | IntroAnonymous ->
       intro_then_gen (NamingAvoid (avoid@explicit_intro_names l))
 	destopt true false
-        (fun id -> intro_patterns_core b avoid (id::ids) thin destopt bound (n+1) tac l)
+        (fun id -> intro_patterns_core b avoid (id::ids) thin destopt bound n tac l)
   | IntroFresh id ->
       (* todo: avoid thinned names to interfere with generation of fresh name *)
       intro_then_gen (NamingBasedOn (id, avoid@explicit_intro_names l))
 	destopt true false
-        (fun id -> intro_patterns_core b avoid (id::ids) thin destopt bound (n+1) tac l)
+        (fun id -> intro_patterns_core b avoid (id::ids) thin destopt bound n tac l)
 
-and intro_pattern_action loc b style pat thin tac id = match pat with
+and intro_pattern_action loc b style pat thin destopt tac id = match pat with
   | IntroWildcard ->
       tac ((loc,id)::thin) None []
   | IntroOrAndPattern ll ->
@@ -2142,7 +2207,13 @@ and intro_pattern_action loc b style pat thin tac id = match pat with
 	(rewrite_hyp style l2r id)
         (tac thin None [])
   | IntroApplyOn (f,(loc,pat)) ->
-      let naming,tac_ipat = prepare_intros_loc loc (IntroIdentifier id) pat in
+      let naming,tac_ipat =
+        prepare_intros_loc loc (IntroIdentifier id) destopt pat in
+      let doclear =
+        if naming = NamingMustBe (loc,id) then
+          Proofview.tclUNIT () (* apply_in_once do a replacement *)
+        else
+          Proofview.V82.tactic (clear [id]) in
       Proofview.Goal.enter begin fun gl ->
         let sigma = Proofview.Goal.sigma gl in
         let env = Proofview.Goal.env gl in
@@ -2151,36 +2222,31 @@ and intro_pattern_action loc b style pat thin tac id = match pat with
           (Tacticals.New.tclTHENFIRST
              (* Skip the side conditions of the apply *)
              (apply_in_once false true true true naming id
-                (None,(sigma,(c,NoBindings))) tac_ipat) (tac thin None []))
+                (None,(sigma,(c,NoBindings)))
+                (fun id -> Tacticals.New.tclTHEN doclear (tac_ipat id)))
+             (tac thin None []))
           sigma
       end
 
-and prepare_intros_loc loc dft = function
+and prepare_intros_loc loc dft destopt = function
   | IntroNaming ipat ->
       prepare_naming loc ipat,
-      (fun _ -> Proofview.tclUNIT ())
+      (fun id -> Proofview.V82.tactic (move_hyp id destopt))
   | IntroAction ipat ->
       prepare_naming loc dft,
       (let tac thin bound =
-        intro_patterns_core true [] [] thin MoveLast bound 0
+        intro_patterns_core true [] [] thin destopt bound 0
           (fun _ l -> clear_wildcards l) in
-      fun id -> intro_pattern_action loc true true ipat [] tac id)
+      fun id -> intro_pattern_action loc true true ipat [] destopt tac id)
   | IntroForthcoming _ -> user_err_loc
       (loc,"",str "Introduction pattern for one hypothesis expected.")
 
 let intro_patterns_bound_to n destopt =
   intro_patterns_core true [] [] [] destopt
-    (Some (true,n)) 0 (fun _ -> clear_wildcards)
-
-(* The following boolean governs what "intros []" do on examples such
-   as "forall x:nat*nat, x=x"; if true, it behaves as "intros [? ?]";
-   if false, it behaves as "intro H; case H; clear H" for fresh H.
-   Kept as false for compatibility.
- *)
-let bracketing_last_or_and_intro_pattern = false 
+    (Some (true,n)) 0 (fun _ l -> clear_wildcards l)
 
 let intro_patterns_to destopt =
-  intro_patterns_core bracketing_last_or_and_intro_pattern
+  intro_patterns_core (use_bracketing_last_or_and_intro_pattern ())
     [] [] [] destopt None 0 (fun _ l -> clear_wildcards l)
 
 let intro_pattern_to destopt pat =
@@ -2197,23 +2263,24 @@ let intros_patterns = function
 (*   Forward reasoning    *)
 (**************************)
 
-let prepare_intros dft = function
+let prepare_intros dft destopt = function
   | None -> prepare_naming dloc dft, (fun _id -> Proofview.tclUNIT ())
-  | Some (loc,ipat) -> prepare_intros_loc loc dft ipat
+  | Some (loc,ipat) -> prepare_intros_loc loc dft destopt ipat
 
 let ipat_of_name = function
   | Anonymous -> None
   | Name id -> Some (dloc, IntroNaming (IntroIdentifier id))
 
- let head_ident c =
+let head_ident c =
    let c = fst (decompose_app ((strip_lam_assum c))) in
    if isVar c then Some (destVar c) else None
 
-let assert_as first ipat c =
-  let naming,tac = prepare_intros IntroAnonymous ipat in
-  let repl = do_replace (head_ident c) naming in
-  if first then assert_before_then_gen repl naming c tac
-  else assert_after_then_gen repl naming c tac
+let assert_as first hd ipat t =
+  let naming,tac = prepare_intros IntroAnonymous MoveLast ipat in
+  let repl = do_replace hd naming in
+  let tac = if repl then (fun id -> Proofview.tclUNIT ()) else tac in
+  if first then assert_before_then_gen repl naming t tac
+  else assert_after_then_gen repl naming t tac
 
 (* apply in as *)
 
@@ -2222,13 +2289,18 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars
   let tac (naming,lemma) tac id =
     apply_in_delayed_once sidecond_first with_delta with_destruct with_evars
       naming id lemma tac in
-  let naming,ipat_tac = prepare_intros (IntroIdentifier id) ipat in
+  Proofview.Goal.enter begin fun gl ->
+  let destopt =
+    if with_evars then MoveLast (* evars would depend on the whole context *)
+    else get_previous_hyp_position id gl in
+  let naming,ipat_tac = prepare_intros (IntroIdentifier id) destopt ipat in
   let lemmas_target, last_lemma_target =
     let last,first = List.sep_last lemmas in
     List.map (fun lem -> (NamingMustBe (dloc,id),lem)) first, (naming,last)
   in
   (* We chain apply_in_once, ending with an intro pattern *)
   List.fold_right tac lemmas_target (tac last_lemma_target ipat_tac) id
+  end
 
 (*
   if sidecond_first then
@@ -2287,7 +2359,7 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty =
           let eq = applist (eq,args) in
           let refl = applist (refl, [t;mkVar id]) in
 	  let term = mkNamedLetIn id c t (mkLetIn (Name heq, refl, eq, ccl)) in
-	  let sigma, _ = Typing.e_type_of env sigma term in
+	  let sigma, _ = Typing.type_of env sigma term in
             sigma, term,
             Tacticals.New.tclTHEN
 	      (intro_gen (NamingMustBe (loc,heq)) (decode_hyp lastlhyp) true false)
@@ -2373,16 +2445,17 @@ let forward b usetac ipat c =
   match usetac with
   | None ->
       Proofview.Goal.enter begin fun gl ->
-      let t = Tacmach.New.pf_type_of gl  c in
-      Tacticals.New.tclTHENFIRST (assert_as true ipat t)
+      let t = Tacmach.New.pf_unsafe_type_of gl c in
+      let hd = head_ident c in
+      Tacticals.New.tclTHENFIRST (assert_as true hd ipat t)
 	(Proofview.V82.tactic (exact_no_check c))
       end
   | Some tac ->
       if b then
-        Tacticals.New.tclTHENFIRST (assert_as b ipat c) tac
+        Tacticals.New.tclTHENFIRST (assert_as b None ipat c) tac
       else
         Tacticals.New.tclTHENS3PARTS
-          (assert_as b ipat c) [||] tac [|Tacticals.New.tclIDTAC|]
+          (assert_as b None ipat c) [||] tac [|Tacticals.New.tclIDTAC|]
 
 let pose_proof na c = forward true None (ipat_of_name na) c
 let assert_by na t tac = forward true (Some tac) (ipat_of_name na) t
@@ -2408,11 +2481,13 @@ let bring_hyps hyps =
   else
     Proofview.Goal.enter begin fun gl ->
       let env = Proofview.Goal.env gl in
+      let store = Proofview.Goal.extra gl in
       let concl = Tacmach.New.pf_nf_concl gl in
       let newcl = List.fold_right mkNamedProd_or_LetIn hyps concl in
       let args = Array.of_list (instance_from_named_context hyps) in
       Proofview.Refine.refine begin fun sigma ->
-        let (sigma, ev) = Evarutil.new_evar env sigma newcl in
+        let (sigma, ev) =
+          Evarutil.new_evar env sigma ~principal:true ~store newcl in
         (sigma, (mkApp (ev, args)))
       end
     end
@@ -2456,7 +2531,7 @@ let generalize_goal_gen env ids i ((occs,c,b),na) t (cl,evd) =
     mkProd_or_LetIn (na,b,t) cl', evd'
 
 let generalize_goal gl i ((occs,c,b),na as o) cl =
-  let t = pf_type_of gl c in
+  let t = pf_unsafe_type_of gl c in
   let env = pf_env gl in
     generalize_goal_gen env (pf_ids_of_hyps gl) i o t cl
 
@@ -2517,7 +2592,7 @@ let new_generalize_gen_let lconstr =
     let (newcl, sigma), args =
       List.fold_right_i 
 	(fun i ((_,c,b),_ as o) (cl, args) ->
-	  let t = Tacmach.New.pf_type_of gl c in
+	  let t = Tacmach.New.pf_unsafe_type_of gl c in
 	  let args = if Option.is_empty b then c :: args else args in
 	    generalize_goal_gen env ids i o t cl, args)
 	0 lconstr ((concl, sigma), [])
@@ -2794,7 +2869,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac =
             let id = match kind_of_term c with
             | Var id -> id
             | _ ->
-            let type_of = Tacmach.New.pf_type_of gl in
+            let type_of = Tacmach.New.pf_unsafe_type_of gl in
             id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in
             let x = fresh_id_in_env avoid id env in
 	    Tacticals.New.tclTHEN
@@ -3043,7 +3118,7 @@ let make_up_names n ind_opt cname =
 
 let error_ind_scheme s =
   let s = if not (String.is_empty s) then s^" " else s in
-  error ("Cannot recognize "^s^"an induction scheme.")
+  errorlabstrm "Tactics" (str "Cannot recognize " ++ str s ++ str "an induction scheme.")
 
 let glob = Universes.constr_of_global
 
@@ -3178,7 +3253,7 @@ let is_defined_variable env id = match lookup_named id env with
 | (_, Some _, _) -> true
 
 let abstract_args gl generalize_vars dep id defined f args =
-  let sigma = project gl in
+  let sigma = ref (project gl) in
   let env = pf_env gl in
   let concl = pf_concl gl in
   let dep = dep || dependent (mkVar id) concl in
@@ -3195,11 +3270,12 @@ let abstract_args gl generalize_vars dep id defined f args =
     *)
   let aux (prod, ctx, ctxenv, c, args, eqs, refls, nongenvars, vars, env) arg =
     let (name, _, ty), arity =
-      let rel, c = Reductionops.splay_prod_n env sigma 1 prod in
+      let rel, c = Reductionops.splay_prod_n env !sigma 1 prod in
 	List.hd rel, c
     in
-    let argty = pf_type_of gl arg in
-    let ty = (* refresh_universes_strict *) ty in
+    let argty = pf_unsafe_type_of gl arg in
+    let sigma', ty = Evarsolve.refresh_universes (Some true) env !sigma ty in
+    let () = sigma := sigma' in
     let lenctx = List.length ctx in
     let liftargty = lift lenctx argty in
     let leq = constr_cmp Reduction.CUMUL liftargty ty in
@@ -3238,8 +3314,9 @@ let abstract_args gl generalize_vars dep id defined f args =
 	      true, mkApp (f', before), after
   in
     if dogen then
+      let tyf' = pf_unsafe_type_of gl f' in
       let arity, ctx, ctxenv, c', args, eqs, refls, nogen, vars, env =
-	Array.fold_left aux (pf_type_of gl f',[],env,f',[],[],[],Id.Set.empty,Id.Set.empty,env) args'
+	Array.fold_left aux (tyf',[],env,f',[],[],[],Id.Set.empty,Id.Set.empty,env) args'
       in
       let args, refls = List.rev args, List.rev refls in
       let vars =
@@ -3248,9 +3325,12 @@ let abstract_args gl generalize_vars dep id defined f args =
 	    hyps_of_vars (pf_env gl) (pf_hyps gl) nogen vars
 	else []
       in
-      let body, c' = if defined then Some c', typ_of ctxenv Evd.empty c' else None, c' in
-	Some (make_abstract_generalize gl id concl dep ctx body c' eqs args refls,
-	     dep, succ (List.length ctx), vars)
+      let body, c' =
+	if defined then Some c', typ_of ctxenv !sigma c'
+	else None, c'
+      in
+      let term = make_abstract_generalize {gl with sigma = !sigma} id concl dep ctx body c' eqs args refls in
+	Some (term, !sigma, dep, succ (List.length ctx), vars)
     else None
 
 let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id =
@@ -3272,20 +3352,26 @@ let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id =
     let newc = Tacmach.New.of_old (fun gl -> abstract_args gl generalize_vars force_dep id def f args) gl in
       match newc with
       | None -> Proofview.tclUNIT ()
-      | Some (newc, dep, n, vars) ->
+      | Some (newc, sigma, dep, n, vars) ->
 	  let tac =
 	    if dep then
-	      Tacticals.New.tclTHENLIST [Proofview.V82.tactic (refine newc); rename_hyp [(id, oldid)]; Tacticals.New.tclDO n intro;
-			   Proofview.V82.tactic (generalize_dep ~with_let:true (mkVar oldid))]
-	    else
-	      Tacticals.New.tclTHENLIST [Proofview.V82.tactic (refine newc); Proofview.V82.tactic (clear [id]); Tacticals.New.tclDO n intro]
+	      Tacticals.New.tclTHENLIST
+		[Proofview.Unsafe.tclEVARS sigma;
+		 Proofview.V82.tactic (refine newc);
+		 rename_hyp [(id, oldid)]; Tacticals.New.tclDO n intro;
+		 Proofview.V82.tactic (generalize_dep ~with_let:true (mkVar oldid))]
+	    else Tacticals.New.tclTHENLIST
+		   [Proofview.Unsafe.tclEVARS sigma;
+		    Proofview.V82.tactic (refine newc);
+		    Proofview.V82.tactic (clear [id]);
+		    Tacticals.New.tclDO n intro]
 	  in
 	    if List.is_empty vars then tac
 	    else Tacticals.New.tclTHEN tac
               (Tacticals.New.tclFIRST
                 [revert vars ;
 		 Proofview.V82.tactic (fun gl -> tclMAP (fun id ->
-				     tclTRY (generalize_dep ~with_let:true (mkVar id))) vars gl)])
+		      tclTRY (generalize_dep ~with_let:true (mkVar id))) vars gl)])
   end
 
 let rec compare_upto_variables x y =
@@ -3563,13 +3649,13 @@ let guess_elim isrec dep s hyp0 gl =
 	Tacmach.New.pf_apply build_case_analysis_scheme gl mind true s
       else
 	Tacmach.New.pf_apply build_case_analysis_scheme_default gl mind s in
-  let elimt = Tacmach.New.pf_type_of gl elimc in
+  let elimt = Tacmach.New.pf_unsafe_type_of gl elimc in
     evd, ((elimc, NoBindings), elimt), mkIndU mind
 
 let given_elim hyp0 (elimc,lbind as e) gl =
   let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in
   let ind_type_guess,_ = decompose_app ((strip_prod tmptyp0)) in
-  Proofview.Goal.sigma gl, (e, Tacmach.New.pf_type_of gl elimc), ind_type_guess
+  Proofview.Goal.sigma gl, (e, Tacmach.New.pf_unsafe_type_of gl elimc), ind_type_guess
 
 type scheme_signature =
     (Id.t list * (elim_arg_kind * bool * Id.t) list) array
@@ -3594,14 +3680,17 @@ 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
 
 let is_functional_induction elimc gl =
-  let scheme = compute_elim_sig ~elimc (Tacmach.New.pf_type_of gl (fst elimc)) in
+  let scheme = compute_elim_sig ~elimc (Tacmach.New.pf_unsafe_type_of gl (fst elimc)) in
   (* The test is not safe: with non-functional induction on non-standard
      induction scheme, this may fail *)
   Option.is_empty scheme.indarg
@@ -3960,7 +4049,7 @@ let induction_gen_l isrec with_evars elim names lc =
 
 	    | _ ->
                 Proofview.Goal.enter begin fun gl ->
-                let type_of = Tacmach.New.pf_type_of gl in
+                let type_of = Tacmach.New.pf_unsafe_type_of gl in
                 let x =
 		  id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in
 
@@ -4222,7 +4311,7 @@ let (forward_setoid_symmetry_in, setoid_symmetry_in) = Hook.make ()
 
 let symmetry_in id =
   Proofview.Goal.enter begin fun gl ->
-  let ctype = Tacmach.New.pf_type_of gl (mkVar id) in
+  let ctype = Tacmach.New.pf_unsafe_type_of gl (mkVar id) in
   let sign,t = decompose_prod_assum ctype in
   Proofview.tclORELSE
     begin
@@ -4273,7 +4362,7 @@ let prove_transitivity hdcncl eq_kind t =
   | HeterogenousEq (typ1,c1,typ2,c2) ->
       let env = Proofview.Goal.env gl in
       let sigma = Proofview.Goal.sigma gl in
-      let type_of = Typing.type_of env sigma in
+      let type_of = Typing.unsafe_type_of env sigma in
       let typt = type_of t in
         (mkApp(hdcncl, [| typ1; c1; typt ;t |]),
          mkApp(hdcncl, [| typt; t; typ2; c2 |]))
@@ -4374,13 +4463,13 @@ 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
-  let open Declareops in
-  let eff = Safe_typing.sideff_of_con (Global.safe_env ()) cst in
-  let effs = cons_side_effects eff
+  let open Safe_typing in
+  let eff = private_con_of_con (Global.safe_env ()) cst in
+  let effs = add_private eff
     Entries.(snd (Future.force const.const_entry_body)) in
   let args = List.rev (instance_from_named_context sign) in
   let solve =