Imported Upstream version 8.9.0upstream/8.9.0upstream

28 files changed, 453 insertions, 251 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 03ff580a..95e908c4 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -13,8 +13,8 @@ open CErrors
 open Util
 open Names
 open Nameops
-open Term
 open Termops
+open Constr
 open Namegen
 open Environ
 open Evd
@@ -26,7 +26,7 @@ open Tacred
 open Pretype_errors
 open Evarutil
 open Unification
-open Misctypes
+open Tactypes
 
 (******************************************************************)
 (* Clausal environments *)
@@ -62,9 +62,6 @@ let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) c
 
 exception NotExtensibleClause
 
-let mk_freelisted c =
-  map_fl EConstr.of_constr (mk_freelisted (EConstr.Unsafe.to_constr c))
-
 let clenv_push_prod cl =
   let typ = whd_all (cl_env cl) (cl_sigma cl) (clenv_type cl) in
   let rec clrec typ = match EConstr.kind cl.evd typ with
@@ -73,7 +70,7 @@ let clenv_push_prod cl =
 	let mv = new_meta () in
 	let dep = not (noccurn (cl_sigma cl) 1 u) in
 	let na' = if dep then na else Anonymous in
-	let e' = meta_declare mv (EConstr.Unsafe.to_constr t) ~name:na' cl.evd in
+        let e' = meta_declare mv t ~name:na' cl.evd in
 	let concl = if dep then subst1 (mkMeta mv) u else u in
 	let def = applist (cl.templval.rebus,[mkMeta mv]) in
 	{ templval = mk_freelisted def;
@@ -107,8 +104,7 @@ let clenv_environments evd bound t =
 	  let mv = new_meta () in
 	  let dep = not (noccurn evd 1 t2) in
 	  let na' = if dep then na else Anonymous in
-	  let t1 = EConstr.Unsafe.to_constr t1 in
-	  let e' = meta_declare mv t1 ~name:na' e in
+          let e' = meta_declare mv t1 ~name:na' e in
 	  clrec (e', (mkMeta mv)::metas) (Option.map ((+) (-1)) n)
 	    (if dep then (subst1 (mkMeta mv) t2) else t2)
       | (n, LetIn (na,b,_,t)) -> clrec (e,metas) n (subst1 b t)
@@ -167,13 +163,13 @@ let clenv_assign mv rhs clenv =
     user_err Pp.(str "clenv_assign: circularity in unification");
   try
     if meta_defined clenv.evd mv then
-      if not (EConstr.eq_constr clenv.evd (EConstr.of_constr (fst (meta_fvalue clenv.evd mv)).rebus) rhs) then
+      if not (EConstr.eq_constr clenv.evd (fst (meta_fvalue clenv.evd mv)).rebus rhs) then
         error_incompatible_inst clenv mv
       else
 	clenv
     else
       let st = (Conv,TypeNotProcessed) in
-      {clenv with evd = meta_assign mv (EConstr.Unsafe.to_constr rhs_fls.rebus,st) clenv.evd}
+      {clenv with evd = meta_assign mv (rhs_fls.rebus,st) clenv.evd}
   with Not_found ->
     user_err Pp.(str "clenv_assign: undefined meta")
 
@@ -218,7 +214,7 @@ let clenv_assign mv rhs clenv =
 *)
 
 let clenv_metas_in_type_of_meta evd mv =
-  (mk_freelisted (meta_instance evd (map_fl EConstr.of_constr (meta_ftype evd mv)))).freemetas
+  (mk_freelisted (meta_instance evd (meta_ftype evd mv))).freemetas
 
 let dependent_in_type_of_metas clenv mvs =
   List.fold_right
@@ -288,11 +284,11 @@ let adjust_meta_source evd mv = function
        in situations like "ex_intro (fun x => P) ?ev p" *)
     let f = function (mv',(Cltyp (_,t) | Clval (_,_,t))) ->
       if Metaset.mem mv t.freemetas then
-        let f,l = decompose_app evd (EConstr.of_constr t.rebus) in
+        let f,l = decompose_app evd t.rebus in
         match EConstr.kind evd f with
         | Meta mv'' ->
           (match meta_opt_fvalue evd mv'' with
-          | Some (c,_) -> match_name (EConstr.of_constr c.rebus) l
+          | Some (c,_) -> match_name c.rebus l
           | None -> None)
         | _ -> None
       else None in
@@ -502,7 +498,6 @@ let clenv_assign_binding clenv k c =
   let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
   let c_typ = nf_betaiota clenv.env clenv.evd (clenv_get_type_of clenv c) in
   let status,clenv',c = clenv_unify_binding_type clenv c c_typ k_typ in
-  let c = EConstr.Unsafe.to_constr c in
   { clenv' with evd = meta_assign k (c,(Conv,status)) clenv'.evd }
 
 let clenv_match_args bl clenv =
@@ -515,7 +510,7 @@ let clenv_match_args bl clenv =
       (fun clenv {CAst.loc;v=(b,c)} ->
 	let k = meta_of_binder clenv loc mvs b in
         if meta_defined clenv.evd k then
-          if EConstr.eq_constr clenv.evd (EConstr.of_constr (fst (meta_fvalue clenv.evd k)).rebus) c then clenv
+          if EConstr.eq_constr clenv.evd (fst (meta_fvalue clenv.evd k)).rebus c then clenv
           else error_already_defined b
         else
 	  clenv_assign_binding clenv k c)
@@ -580,8 +575,8 @@ let make_clenv_binding env sigma = make_clenv_binding_gen false None env sigma
 
 let pr_clenv clenv =
   h 0
-    (str"TEMPL: " ++ print_constr clenv.templval.rebus ++
-     str" : " ++ print_constr clenv.templtyp.rebus ++ fnl () ++
+    (str"TEMPL: " ++ Termops.Internal.print_constr_env clenv.env clenv.evd clenv.templval.rebus ++
+     str" : " ++ Termops.Internal.print_constr_env clenv.env clenv.evd clenv.templtyp.rebus ++ fnl () ++
      pr_evar_map (Some 2) clenv.evd)
 
 (****************************************************************)
@@ -677,7 +672,7 @@ let define_with_type sigma env ev c =
   let j = Environ.make_judge c ty in
   let (sigma, j) = Coercion.inh_conv_coerce_to true env sigma j t in
   let (ev, _) = destEvar sigma ev in
-  let sigma = Evd.define ev (EConstr.Unsafe.to_constr j.Environ.uj_val) sigma in
+  let sigma = Evd.define ev j.Environ.uj_val sigma in
   sigma
 
 let solve_evar_clause env sigma hyp_only clause = function
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index b85c4fc5..f9506290 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -18,7 +18,7 @@ open Environ
 open Evd
 open EConstr
 open Unification
-open Misctypes
+open Tactypes
 
 (** {6 The Type of Constructions clausale environments.} *)
 
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 209104ac..544175c6 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -10,7 +10,7 @@
 
 open Util
 open Names
-open Term
+open Constr
 open Termops
 open Evd
 open EConstr
@@ -54,7 +54,7 @@ let clenv_cast_meta clenv =
 let clenv_value_cast_meta clenv =
     clenv_cast_meta clenv (clenv_value clenv)
 
-let clenv_pose_dependent_evars with_evars clenv =
+let clenv_pose_dependent_evars ?(with_evars=false) clenv =
   let dep_mvs = clenv_dependent clenv in
   let env, sigma = clenv.env, clenv.evd in
   if not (List.is_empty dep_mvs) && not with_evars then
@@ -75,12 +75,12 @@ let check_tc evd =
   let has_typeclass = Evar.Map.exists check (Evd.undefined_map evd) in
   (has_typeclass, !has_resolvable)
 
-let clenv_refine with_evars ?(with_classes=true) clenv =
+let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv =
   (** ppedrot: a Goal.enter here breaks things, because the tactic below may
       solve goals by side effects, while the compatibility layer keeps those
       useless goals. That deserves a FIXME. *)
   Proofview.V82.tactic begin fun gl ->
-  let clenv = clenv_pose_dependent_evars with_evars clenv in
+  let clenv = clenv_pose_dependent_evars ~with_evars clenv in
   let evd' =
     if with_classes then
       let (has_typeclass, has_resolvable) = check_tc clenv.evd in
@@ -105,10 +105,10 @@ open Unification
 
 let dft = default_unify_flags
 
-let res_pf ?(with_evars=false) ?(with_classes=true) ?(flags=dft ()) clenv =
+let res_pf ?with_evars ?(with_classes=true) ?(flags=dft ()) clenv =
   Proofview.Goal.enter begin fun gl ->
     let clenv = clenv_unique_resolver ~flags clenv gl in
-    clenv_refine with_evars ~with_classes clenv
+    clenv_refine ?with_evars ~with_classes clenv
   end
 
 (* [unifyTerms] et [unify] ne semble pas gérer les Meta, en
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index 7c1e300b..d1784784 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -13,12 +13,11 @@
 open Clenv
 open EConstr
 open Unification
-open Misctypes
 
 (** Tactics *)
 val unify : ?flags:unify_flags -> constr -> unit Proofview.tactic
-val clenv_refine : evars_flag -> ?with_classes:bool -> clausenv -> unit Proofview.tactic
-val res_pf : ?with_evars:evars_flag -> ?with_classes:bool -> ?flags:unify_flags -> clausenv -> unit Proofview.tactic
+val clenv_refine : ?with_evars:bool -> ?with_classes:bool -> clausenv -> unit Proofview.tactic
+val res_pf : ?with_evars:bool -> ?with_classes:bool -> ?flags:unify_flags -> clausenv -> unit Proofview.tactic
 
-val clenv_pose_dependent_evars : evars_flag -> clausenv -> clausenv
+val clenv_pose_dependent_evars : ?with_evars:bool -> clausenv -> clausenv
 val clenv_value_cast_meta : clausenv -> constr
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 0d197c92..c80f370f 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -25,8 +25,6 @@ open Ltac_pretype
 type glob_constr_ltac_closure = ltac_var_map * glob_constr
 
 let depends_on_evar sigma evk _ (pbty,_,t1,t2) =
-  let t1 = EConstr.of_constr t1 in
-  let t2 = EConstr.of_constr t2 in
   try Evar.equal (head_evar sigma t1) evk
   with NoHeadEvar ->
   try Evar.equal (head_evar sigma t2) evk
@@ -35,12 +33,12 @@ let depends_on_evar sigma evk _ (pbty,_,t1,t2) =
 let define_and_solve_constraints evk c env evd =
   if Termops.occur_evar evd evk c then
     Pretype_errors.error_occur_check env evd evk c;
-  let evd = define evk (EConstr.Unsafe.to_constr c) evd in
+  let evd = define evk c evd in
   let (evd,pbs) = extract_changed_conv_pbs evd (depends_on_evar evd evk) in
   match
     List.fold_left
       (fun p (pbty,env,t1,t2) -> match p with
-	| Success evd -> Evarconv.evar_conv_x full_transparent_state env evd pbty (EConstr.of_constr t1) (EConstr.of_constr t2)
+        | Success evd -> Evarconv.evar_conv_x full_transparent_state env evd pbty t1 t2
 	| UnifFailure _ as x -> x) (Success evd)
       pbs
   with
@@ -59,7 +57,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
       Pretyping.fail_evar = false;
       Pretyping.expand_evars = true } in
     try Pretyping.understand_ltac flags
-      env sigma ltac_var (Pretyping.OfType (EConstr.of_constr evi.evar_concl)) rawc
+      env sigma ltac_var (Pretyping.OfType evi.evar_concl) rawc
     with e when CErrors.noncritical e ->
       let loc = Glob_ops.loc_of_glob_constr rawc in
       user_err ?loc 
diff --git a/proofs/goal.ml b/proofs/goal.ml
index ba7e458f..c14c0a8a 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -48,7 +48,7 @@ module V82 = struct
   (* Access to ".evar_concl" *)
   let concl evars gl =
     let evi = Evd.find evars gl in
-    EConstr.of_constr evi.Evd.evar_concl
+    evi.Evd.evar_concl
 
   (* Access to ".evar_extra" *)
   let extra evars gl =
@@ -61,7 +61,6 @@ module V82 = struct
        be shelved. It must not appear as a future_goal, so the future
        goals are restored to their initial value after the evar is
        created. *)
-    let concl = EConstr.Unsafe.to_constr concl in
     let prev_future_goals = Evd.save_future_goals evars in
     let evi = { Evd.evar_hyps = hyps;
 		Evd.evar_concl = concl;
@@ -86,7 +85,7 @@ module V82 = struct
       if not (Evarutil.occur_evar_upto sigma evk c) then ()
       else Pretype_errors.error_occur_check Environ.empty_env sigma evk c
     in
-    Evd.define evk (EConstr.Unsafe.to_constr c) sigma
+    Evd.define evk c sigma
 
   (* Instantiates a goal with an open term, using name of goal for evk' *)
   let partial_solution_to sigma evk evk' c =
@@ -100,7 +99,9 @@ module V82 = struct
   let same_goal evars1 gl1 evars2 gl2 =
     let evi1 = Evd.find evars1 gl1 in
     let evi2 = Evd.find evars2 gl2 in
-    Constr.equal evi1.Evd.evar_concl evi2.Evd.evar_concl &&
+    let c1 = EConstr.Unsafe.to_constr evi1.Evd.evar_concl in
+    let c2 = EConstr.Unsafe.to_constr evi2.Evd.evar_concl in
+    Constr.equal c1 c2 &&
     Environ.eq_named_context_val evi1.Evd.evar_hyps evi2.Evd.evar_hyps
 
   let weak_progress glss gls =
@@ -117,20 +118,6 @@ module V82 = struct
        with a good implementation of them.
     *)
 
-  (* Used for congruence closure  *)
-  let new_goal_with sigma gl extra_hyps =
-    let evi = Evd.find sigma gl in
-    let hyps = evi.Evd.evar_hyps in
-    let new_hyps =
-      List.fold_right Environ.push_named_context_val extra_hyps hyps in
-    let filter = evi.Evd.evar_filter in
-    let new_filter = Evd.Filter.extend (List.length extra_hyps) filter in
-    let new_evi =
-      { evi with Evd.evar_hyps = new_hyps; Evd.evar_filter = new_filter } in
-    let new_evi = Typeclasses.mark_unresolvable new_evi in
-    let (sigma, evk) = Evarutil.new_pure_evar_full Evd.empty new_evi in
-    { Evd.it = evk ; sigma = sigma; }
-
   (* Used by the compatibility layer and typeclasses *)
   let nf_evar sigma gl =
     let evi = Evd.find sigma gl in
@@ -156,3 +143,5 @@ module V82 = struct
 				       ) ~init:(concl sigma gl) env
 
 end
+
+module Set = Set.Make(struct type t = goal let compare = Evar.compare end)
diff --git a/proofs/goal.mli b/proofs/goal.mli
index dc986315..a033d6da 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -64,9 +64,6 @@ module V82 : sig
  (* Principal part of tclNOTSAMEGOAL *)
   val same_goal : Evd.evar_map -> goal -> Evd.evar_map -> goal -> bool
 
- (* Used for congruence closure *)
-  val new_goal_with : Evd.evar_map -> goal -> Context.Named.t -> goal Evd.sigma
-
   (* Used by the compatibility layer and typeclasses *)
   val nf_evar : Evd.evar_map -> goal -> goal * Evd.evar_map
 
@@ -74,3 +71,5 @@ module V82 : sig
   val abstract_type : Evd.evar_map -> goal -> EConstr.types 
 
 end
+
+module Set : sig include Set.S with type elt = goal end
diff --git a/proofs/goal_select.ml b/proofs/goal_select.ml
new file mode 100644
index 00000000..65a94a2c
--- /dev/null
+++ b/proofs/goal_select.ml
@@ -0,0 +1,68 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Names
+
+(* spiwack: I'm choosing, for now, to have [goal_selector] be a
+   different type than [goal_reference] mostly because if it makes sense
+   to print a goal that is out of focus (or already solved) it doesn't
+   make sense to apply a tactic to it. Hence it the types may look very
+   similar, they do not seem to mean the same thing. *)
+type t =
+  | SelectAlreadyFocused
+  | SelectNth of int
+  | SelectList of (int * int) list
+  | SelectId of Id.t
+  | SelectAll
+
+(* Default goal selector: selector chosen when a tactic is applied
+   without an explicit selector. *)
+let default_goal_selector = ref (SelectNth 1)
+let get_default_goal_selector () = !default_goal_selector
+
+let pr_range_selector (i, j) =
+  if i = j then Pp.int i
+  else Pp.(int i ++ str "-" ++ int j)
+
+let pr_goal_selector = function
+  | SelectAlreadyFocused -> Pp.str "!"
+  | SelectAll -> Pp.str "all"
+  | SelectNth i -> Pp.int i
+  | SelectList l ->
+    Pp.(str "["
+     ++ prlist_with_sep pr_comma pr_range_selector l
+     ++ str "]")
+  | SelectId id -> Names.Id.print id
+
+let parse_goal_selector = function
+  | "!" -> SelectAlreadyFocused
+  | "all" -> SelectAll
+  | i ->
+      let err_msg = "The default selector must be \"all\" or a natural number." in
+      begin try
+              let i = int_of_string i in
+              if i < 0 then CErrors.user_err Pp.(str err_msg);
+              SelectNth i
+        with Failure _ -> CErrors.user_err Pp.(str err_msg)
+      end
+
+let _ = let open Goptions in
+  declare_string_option
+    { optdepr = false;
+      optname = "default goal selector" ;
+      optkey  = ["Default";"Goal";"Selector"] ;
+      optread = begin fun () ->
+        Pp.string_of_ppcmds
+          (pr_goal_selector !default_goal_selector)
+      end;
+      optwrite = begin fun n ->
+        default_goal_selector := parse_goal_selector n
+      end
+    }
diff --git a/proofs/goal_select.mli b/proofs/goal_select.mli
new file mode 100644
index 00000000..b1c57238
--- /dev/null
+++ b/proofs/goal_select.mli
@@ -0,0 +1,26 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Names
+
+(* spiwack: I'm choosing, for now, to have [goal_selector] be a
+   different type than [goal_reference] mostly because if it makes sense
+   to print a goal that is out of focus (or already solved) it doesn't
+   make sense to apply a tactic to it. Hence it the types may look very
+   similar, they do not seem to mean the same thing. *)
+type t =
+  | SelectAlreadyFocused
+  | SelectNth of int
+  | SelectList of (int * int) list
+  | SelectId of Id.t
+  | SelectAll
+
+val pr_goal_selector : t -> Pp.t
+val get_default_goal_selector : unit -> t
diff --git a/proofs/logic.ml b/proofs/logic.ml
index e5294715..613581ad 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -23,7 +23,6 @@ open Typing
 open Proof_type
 open Type_errors
 open Retyping
-open Misctypes
 
 module NamedDecl = Context.Named.Declaration
 
@@ -63,6 +62,7 @@ let is_unification_error = function
 
 let catchable_exception = function
   | CErrors.UserError _ | TypeError _
+  | Notation.NumeralNotationError _
   | RefinerError _ | Indrec.RecursionSchemeError _
   | Nametab.GlobalizationError _
   (* reduction errors *)
@@ -185,6 +185,22 @@ let check_decl_position env sigma sign d =
  * on the right side [right] if [toleft=false].
  * If [with_dep] then dependent hypotheses are moved accordingly. *)
 
+(** Move destination for hypothesis *)
+
+type 'id move_location =
+  | MoveAfter of 'id
+  | MoveBefore of 'id
+  | MoveFirst
+  | MoveLast (** can be seen as "no move" when doing intro *)
+
+(** Printing of [move_location] *)
+
+let pr_move_location pr_id = function
+  | MoveAfter id -> brk(1,1) ++ str "after " ++ pr_id id
+  | MoveBefore id -> brk(1,1) ++ str "before " ++ pr_id id
+  | MoveFirst -> str " at top"
+  | MoveLast -> str " at bottom"
+
 let move_location_eq m1 m2 = match m1, m2 with
 | MoveAfter id1, MoveAfter id2 -> Id.equal id1 id2
 | MoveBefore id1, MoveBefore id2 -> Id.equal id1 id2
@@ -236,7 +252,7 @@ let move_hyp sigma toleft (left,declfrom,right) hto =
 	      (first, d::middle)
             else
 	      user_err ~hdr:"move_hyp" (str "Cannot move " ++ Id.print (NamedDecl.get_id declfrom) ++
-	        Miscprint.pr_move_location Id.print hto ++
+                pr_move_location Id.print hto ++
 	        str (if toleft then ": it occurs in the type of " else ": it depends on ")
 	        ++ Id.print hyp ++ str ".")
           else
@@ -289,7 +305,15 @@ let collect_meta_variables c =
   let rec collrec deep acc c = match kind c with
     | Meta mv -> if deep then error_unsupported_deep_meta () else mv::acc
     | Cast(c,_,_) -> collrec deep acc c
-    | (App _| Case _) -> Constr.fold (collrec deep) acc c
+    | Case(ci,p,c,br) ->
+        (* Hack assuming only two situations: the legacy one that branches,
+           if with Metas, are Meta, and the new one with eta-let-expanded
+           branches *)
+        let br = Array.map2 (fun n b -> try snd (Term.decompose_lam_n_decls n b) with UserError _ -> b) ci.ci_cstr_ndecls br in
+        Array.fold_left (collrec deep)
+          (Constr.fold (collrec deep) (Constr.fold (collrec deep) acc p) c)
+          br
+    | App _ -> Constr.fold (collrec deep) acc c
     | Proj (_, c) -> collrec deep acc c
     | _ -> Constr.fold (collrec true) acc c
   in
@@ -301,9 +325,10 @@ let check_meta_variables env sigma c =
 
 let check_conv_leq_goal env sigma arg ty conclty =
   if !check then
-    let evm, b = Reductionops.infer_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr conclty) in
-      if b then evm 
-      else raise (RefinerError (env, sigma, BadType (arg,ty,conclty)))
+    let ans = Reductionops.infer_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr conclty) in
+    match ans with
+    | Some evm -> evm
+    | None -> raise (RefinerError (env, sigma, BadType (arg,ty,conclty)))
   else sigma
 
 exception Stop of EConstr.t list
@@ -387,12 +412,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
       | Case (ci,p,c,lf) ->
 	let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals sigma goal goalacc p c in
 	let sigma = check_conv_leq_goal env sigma trm conclty' conclty in
-	let (acc'',sigma, rbranches) =
-	  Array.fold_left2
-            (fun (lacc,sigma,bacc) ty fi ->
-	       let (r,_,s,b') = mk_refgoals sigma goal lacc ty fi in r,s,(b'::bacc))
-            (acc',sigma,[]) lbrty lf
-	in
+        let (acc'',sigma,rbranches) = treat_case sigma goal ci lbrty lf acc' in
         let lf' = Array.rev_of_list rbranches in
         let ans =
           if p' == p && c' == c && Array.equal (==) lf' lf then trm
@@ -440,12 +460,7 @@ and mk_hdgoals sigma goal goalacc trm =
 
     | Case (ci,p,c,lf) ->
 	let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals sigma goal goalacc p c in
-	let (acc'',sigma,rbranches) =
-	  Array.fold_left2
-            (fun (lacc,sigma,bacc) ty fi ->
-	       let (r,_,s,b') = mk_refgoals sigma goal lacc ty fi in r,s,(b'::bacc))
-            (acc',sigma,[]) lbrty lf
-	in
+        let (acc'',sigma,rbranches) = treat_case sigma goal ci lbrty lf acc' in
 	let lf' = Array.rev_of_list rbranches in
 	let ans =
           if p' == p && c' == c && Array.equal (==) lf' lf then trm
@@ -483,7 +498,7 @@ and mk_arggoals sigma goal goalacc funty allargs =
       let env = Goal.V82.env sigma goal in
       raise (RefinerError (env,sigma,CannotApply (t, harg)))
   in
-  Array.smartfoldmap foldmap (goalacc, funty, sigma) allargs
+  Array.Smart.fold_left_map foldmap (goalacc, funty, sigma) allargs
 
 and mk_casegoals sigma goal goalacc p c =
   let env = Goal.V82.env sigma goal in
@@ -497,6 +512,50 @@ and mk_casegoals sigma goal goalacc p c =
   let (lbrty,conclty) = type_case_branches_with_names env sigma indspec p c in
   (acc'',lbrty,conclty,sigma,p',c')
 
+and treat_case sigma goal ci lbrty lf acc' =
+  let rec strip_outer_cast c = match kind c with
+  | Cast (c,_,_) -> strip_outer_cast c
+  | _ -> c in
+  let decompose_app_vect c = match kind c with
+  | App (f,cl) -> (f, cl)
+  | _ -> (c,[||]) in
+  let env = Goal.V82.env sigma goal in
+  Array.fold_left3
+    (fun (lacc,sigma,bacc) ty fi l ->
+        if isMeta (strip_outer_cast fi) then
+          (* Support for non-eta-let-expanded Meta as found in *)
+          (* destruct/case with an non eta-let expanded elimination scheme *)
+          let (r,_,s,fi') = mk_refgoals sigma goal lacc ty fi in
+          r,s,(fi'::bacc)
+        else
+        (* Deal with a branch in expanded form of the form
+           Case(ci,p,c,[|eta-let-exp(Meta);...;eta-let-exp(Meta)|]) as
+           if it were not so, so as to preserve compatibility with when
+           destruct/case generated schemes of the form
+           Case(ci,p,c,[|Meta;...;Meta|];
+           CAUTION: it does not deal with the general case of eta-zeta
+           reduced branches having a form different from Meta, as it
+           would be theoretically the case with third-party code *)
+        let n = List.length l in
+        let ctx, body = Term.decompose_lam_n_decls n fi in
+        let head, args = decompose_app_vect body in
+        (* Strip cast because clenv_cast_meta adds a cast when the branch is
+           eta-expanded but when not when the branch has the single-meta
+           form [Meta] *)
+        let head = strip_outer_cast head in
+        if isMeta head then begin
+          assert (args = Context.Rel.to_extended_vect mkRel 0 ctx);
+          let head' = lift (-n) head in
+          let (r,_,s,head'') = mk_refgoals sigma goal lacc ty head' in
+          let fi' = it_mkLambda_or_LetIn (mkApp (head'',args)) ctx in
+          (r,s,fi'::bacc)
+        end
+        else
+          (* Supposed to be meta-free *)
+          let sigma, t'ty = goal_type_of env sigma fi in
+          let sigma = check_conv_leq_goal env sigma fi t'ty ty in
+          (lacc,sigma,fi::bacc))
+    (acc',sigma,[]) lbrty lf ci.ci_pp_info.cstr_tags
 
 let convert_hyp check sign sigma d =
   let id = NamedDecl.get_id d in
diff --git a/proofs/logic.mli b/proofs/logic.mli
index dc471bb5..9db54732 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -58,12 +58,23 @@ val error_no_such_hypothesis : Environ.env -> evar_map -> Id.t -> 'a
 
 val catchable_exception : exn -> bool
 
+(** Move destination for hypothesis *)
+
+type 'id move_location =
+  | MoveAfter of 'id
+  | MoveBefore of 'id
+  | MoveFirst
+  | MoveLast (** can be seen as "no move" when doing intro *)
+
+val pr_move_location :
+  ('a -> Pp.t) -> 'a move_location -> Pp.t
+
 val convert_hyp : bool -> Environ.named_context_val -> evar_map ->
   EConstr.named_declaration -> Environ.named_context_val
 
-val move_hyp_in_named_context : Environ.env -> Evd.evar_map -> Id.t -> Id.t Misctypes.move_location ->
+val move_hyp_in_named_context : Environ.env -> Evd.evar_map -> Id.t -> Id.t move_location ->
   Environ.named_context_val -> Environ.named_context_val
 
 val insert_decl_in_named_context : Evd.evar_map ->
-  EConstr.named_declaration -> Id.t Misctypes.move_location ->
+  EConstr.named_declaration -> Id.t move_location ->
   Environ.named_context_val -> Environ.named_context_val
diff --git a/proofs/miscprint.ml b/proofs/miscprint.ml
index 1a63ff67..ec17b807 100644
--- a/proofs/miscprint.ml
+++ b/proofs/miscprint.ml
@@ -10,7 +10,7 @@
 
 open Pp
 open Names
-open Misctypes
+open Tactypes
 
 (** Printing of [intro_pattern] *)
 
@@ -20,7 +20,7 @@ let rec pr_intro_pattern prc {CAst.v=pat} = match pat with
   | IntroNaming p -> pr_intro_pattern_naming p
   | IntroAction p -> pr_intro_pattern_action prc p
 
-and pr_intro_pattern_naming = function
+and pr_intro_pattern_naming = let open Namegen in function
   | IntroIdentifier id -> Id.print id
   | IntroFresh id -> str "?" ++ Id.print id
   | IntroAnonymous -> str "?"
@@ -43,14 +43,6 @@ and pr_or_and_intro_pattern prc = function
       hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc (pr_intro_pattern prc)) pll)
       ++ str "]"
 
-(** Printing of [move_location] *)
-
-let pr_move_location pr_id = function
-  | MoveAfter id -> brk(1,1) ++ str "after " ++ pr_id id
-  | MoveBefore id -> brk(1,1) ++ str "before " ++ pr_id id
-  | MoveFirst -> str " at top"
-  | MoveLast -> str " at bottom"
-
 (** Printing of bindings *)
 let pr_binding prc = let open CAst in function
   | {loc;v=(NamedHyp id, c)} -> hov 1 (Names.Id.print id ++ str " := " ++ cut () ++ prc c)
diff --git a/proofs/miscprint.mli b/proofs/miscprint.mli
index 79790a27..f4e2e683 100644
--- a/proofs/miscprint.mli
+++ b/proofs/miscprint.mli
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Misctypes
+open Tactypes
 
 (** Printing of [intro_pattern] *)
 
@@ -18,13 +18,10 @@ val pr_intro_pattern :
 val pr_or_and_intro_pattern :
   ('a -> Pp.t) -> 'a or_and_intro_pattern_expr -> Pp.t
 
-val pr_intro_pattern_naming : intro_pattern_naming_expr -> Pp.t
+val pr_intro_pattern_naming : Namegen.intro_pattern_naming_expr -> Pp.t
 
 (** Printing of [move_location] *)
 
-val pr_move_location :
-  ('a -> Pp.t) -> 'a move_location -> Pp.t
-
 val pr_bindings :
   ('a -> Pp.t) ->
   ('a -> Pp.t) -> 'a bindings -> Pp.t
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 5d137988..e6507332 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -51,23 +51,22 @@ let _ = CErrors.register_handler begin function
   | _ -> raise CErrors.Unhandled
 end
 
-let get_nth_V82_goal i =
-  let p = Proof_global.give_me_the_proof () in
+let get_nth_V82_goal p i =
   let goals,_,_,_,sigma = Proof.proof p in
   try { it = List.nth goals (i-1) ; sigma }
   with Failure _ -> raise NoSuchGoal
 
-let get_goal_context_gen i =
-  let { it=goal ; sigma=sigma; } =  get_nth_V82_goal i in
+let get_goal_context_gen p i =
+  let { it=goal ; sigma=sigma; } = get_nth_V82_goal p i in
   (sigma, Refiner.pf_env { it=goal ; sigma=sigma; })
 
 let get_goal_context i =
-  try get_goal_context_gen i
+  try get_goal_context_gen (Proof_global.give_me_the_proof ()) i
   with Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof.")
      | NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.")
 
 let get_current_goal_context () =
-  try get_goal_context_gen 1
+  try get_goal_context_gen (Proof_global.give_me_the_proof ()) 1
   with Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof.")
      | NoSuchGoal -> 
     (* spiwack: returning empty evar_map, since if there is no goal, under focus,
@@ -75,14 +74,18 @@ let get_current_goal_context () =
     let env = Global.env () in
     (Evd.from_env env, env)
 
-let get_current_context () =
-  try get_goal_context_gen 1
+let get_current_context ?p () =
+  let current_proof_by_default = function
+    | Some p -> p
+    | None -> Proof_global.give_me_the_proof ()
+  in
+  try get_goal_context_gen (current_proof_by_default p) 1
   with Proof_global.NoCurrentProof ->
     let env = Global.env () in
     (Evd.from_env env, env)
      | NoSuchGoal ->
         (* No more focused goals ? *)
-        let p = Proof_global.give_me_the_proof () in
+        let p = (current_proof_by_default p) in
         let evd = Proof.in_proof p (fun x -> x) in
         (evd, Global.env ())
 
@@ -100,11 +103,23 @@ let solve ?with_end_tac gi info_lvl tac pr =
       | None -> tac
       | Some _ -> Proofview.Trace.record_info_trace tac
     in
-    let tac = match gi with
-      | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i tac
-      | Vernacexpr.SelectList l -> Proofview.tclFOCUSLIST l tac
-      | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id tac
-      | Vernacexpr.SelectAll -> tac
+    let tac = let open Goal_select in match gi with
+      | SelectAlreadyFocused ->
+        let open Proofview.Notations in
+        Proofview.numgoals >>= fun n ->
+        if n == 1 then tac
+        else
+          let e = CErrors.UserError
+              (None,
+               Pp.(str "Expected a single focused goal but " ++
+                   int n ++ str " goals are focused."))
+          in
+          Proofview.tclZERO e
+
+      | SelectNth i -> Proofview.tclFOCUS i i tac
+      | SelectList l -> Proofview.tclFOCUSLIST l tac
+      | SelectId id -> Proofview.tclFOCUSID id tac
+      | SelectAll -> tac
     in
     let tac =
       if use_unification_heuristics () then
@@ -121,7 +136,7 @@ let solve ?with_end_tac gi info_lvl tac pr =
   with
     Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof")
 
-let by tac = Proof_global.with_current_proof (fun _ -> solve (Vernacexpr.SelectNth 1) None tac)
+let by tac = Proof_global.with_current_proof (fun _ -> solve (Goal_select.SelectNth 1) None tac)
 
 let instantiate_nth_evar_com n com = 
   Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.instantiate_evar n com p)
@@ -161,7 +176,7 @@ let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac =
       const_entry_body = Future.chain ce.const_entry_body
         (fun (pt, _) -> pt, ()) } in
   let (cb, ctx), () = Future.force ce.const_entry_body in
-  let univs = UState.merge side_eff Evd.univ_rigid univs ctx in
+  let univs = UState.merge ~sideff:side_eff ~extend:true Evd.univ_rigid univs ctx in
   cb, status, univs
 
 let refine_by_tactic env sigma ty tac =
@@ -188,8 +203,7 @@ let refine_by_tactic env sigma ty tac =
   | [c, _] -> c
   | _ -> assert false
   in
-  let ans = Reductionops.nf_evar sigma ans in
-  let ans = EConstr.Unsafe.to_constr ans in
+  let ans = EConstr.to_constr ~abort_on_undefined_evars:false sigma ans in
   (** [neff] contains the freshly generated side-effects *)
   let neff = Evd.eval_side_effects sigma in
   (** Reset the old side-effects *)
@@ -233,7 +247,7 @@ let apply_implicit_tactic tac = (); fun env sigma evk ->
 	(Environ.named_context env) ->
       let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (CErrors.UserError (None,Pp.str"Proof is not complete."))) []) in
       (try
-        let c = Evarutil.nf_evars_universes sigma evi.evar_concl in
+        let c = Evarutil.nf_evars_universes sigma (EConstr.Unsafe.to_constr evi.evar_concl) in
         let c = EConstr.of_constr c in
         if Evarutil.has_undefined_evars sigma c then raise Exit;
         let (ans, _, ctx) =
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 65cde3a3..5feb5bd6 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -24,7 +24,7 @@ open Decl_kinds
     proof of mutually dependent theorems) *)
 
 val start_proof :
-  Id.t -> ?pl:Univdecls.universe_decl -> goal_kind -> Evd.evar_map -> named_context_val -> EConstr.constr ->
+  Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map -> named_context_val -> EConstr.constr ->
   ?init_tac:unit Proofview.tactic ->
   Proof_global.proof_terminator -> unit
 
@@ -60,7 +60,7 @@ val get_current_goal_context : unit -> Evd.evar_map * env
   If there is no pending proof then it returns the current global
   environment and empty evar_map. *)
 
-val get_current_context : unit -> Evd.evar_map * env
+val get_current_context : ?p:Proof.t -> unit -> Evd.evar_map * env
 
 (** [current_proof_statement] *)
 
@@ -75,7 +75,7 @@ val current_proof_statement :
     tac] applies [tac] to all subgoals. *)
 
 val solve : ?with_end_tac:unit Proofview.tactic ->
-      Vernacexpr.goal_selector -> int option -> unit Proofview.tactic ->
+      Goal_select.t -> int option -> unit Proofview.tactic ->
       Proof.t -> Proof.t * bool
 
 (** [by tac] applies tactic [tac] to the 1st subgoal of the current
@@ -85,6 +85,9 @@ val solve : ?with_end_tac:unit Proofview.tactic ->
 
 val by : unit Proofview.tactic -> bool
 
+(** Option telling if unification heuristics should be used. *)
+val use_unification_heuristics : unit -> bool
+
 (** [instantiate_nth_evar_com n c] instantiate the [n]th undefined
    existential variable of the current focused proof by [c] or raises a
    UserError if no proof is focused or if there is no such [n]th
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 51e0a1d6..8bbd82bb 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -63,6 +63,7 @@ exception CannotUnfocusThisWay
 (* Cannot focus on non-existing subgoals *)
 exception NoSuchGoals of int * int
 
+exception NoSuchGoal of Names.Id.t
 
 exception FullyUnfocused
 
@@ -75,6 +76,10 @@ let _ = CErrors.register_handler begin function
       CErrors.user_err ~hdr:"Focus" Pp.(
         str"Not every goal in range ["++ int i ++ str","++int j++str"] exist."
       )
+  | NoSuchGoal id ->
+      CErrors.user_err
+        ~hdr:"Focus"
+        Pp.(str "No such goal: " ++ str (Names.Id.to_string id) ++ str ".")
   | FullyUnfocused -> CErrors.user_err Pp.(str "The proof is not focused")
   | _ -> raise CErrors.Unhandled
 end
@@ -230,6 +235,37 @@ let focus cond inf i pr =
   try _focus cond (Obj.repr inf) i i pr
   with CList.IndexOutOfRange -> raise (NoSuchGoals (i,i))
 
+(* Focus on the goal named id *)
+let focus_id cond inf id pr =
+  let (focused_goals, evar_map) = Proofview.proofview pr.proofview in
+  begin match try Some (Evd.evar_key id evar_map) with Not_found -> None with
+  | Some ev ->
+     begin match CList.safe_index Evar.equal ev focused_goals with
+     | Some i ->
+        (* goal is already under focus *)
+        _focus cond (Obj.repr inf) i i pr
+     | None ->
+        if CList.mem_f Evar.equal ev pr.shelf then
+          (* goal is on the shelf, put it in focus *)
+          let proofview = Proofview.unshelve [ev] pr.proofview in
+          let shelf =
+            CList.filter (fun ev' -> Evar.equal ev ev' |> not) pr.shelf
+          in
+          let pr = { pr with proofview; shelf } in
+          let (focused_goals, _) = Proofview.proofview pr.proofview in
+          let i =
+            (* Now we know that this will succeed *)
+            try CList.index Evar.equal ev focused_goals
+            with Not_found -> assert false
+          in
+          _focus cond (Obj.repr inf) i i pr
+        else
+          raise CannotUnfocusThisWay
+     end
+  | None ->
+     raise (NoSuchGoal id)
+  end
+
 let rec unfocus kind pr () =
   let cond = cond_of_focus pr in
   match test_cond cond kind pr.proofview with
@@ -452,3 +488,12 @@ module V82 = struct
     { pr with proofview ; shelf }
 
 end
+
+let all_goals p =
+  let add gs set =
+    List.fold_left (fun s g -> Goal.Set.add g s) set gs in
+  let (goals,stack,shelf,given_up,_) = proof p in
+    let set = add goals Goal.Set.empty in
+    let set = List.fold_left (fun s gs -> let (g1, g2) = gs in add g1 (add g2 set)) set stack in
+    let set = add shelf set in
+    add given_up set
diff --git a/proofs/proof.mli b/proofs/proof.mli
index c0e832fb..511dcc2e 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -137,6 +137,9 @@ val done_cond : ?loose_end:bool -> 'a focus_kind -> 'a focus_condition
    a need for it? *)
 val focus : 'a focus_condition -> 'a -> int -> t -> t
 
+(* focus on goal named id *)
+val focus_id : 'aa focus_condition -> 'a -> Names.Id.t -> t -> t
+
 exception FullyUnfocused
 exception CannotUnfocusThisWay
 
@@ -207,3 +210,6 @@ module V82 : sig
   (* Implements the Existential command *)
   val instantiate_evar : int -> Constrexpr.constr_expr -> t -> t
 end
+
+(* returns the set of all goals in the proof *)
+val all_goals : t -> Goal.Set.t
diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml
index e22d382f..cc3e79f8 100644
--- a/proofs/proof_bullet.ml
+++ b/proofs/proof_bullet.ml
@@ -10,19 +10,22 @@
 
 open Proof
 
-type t = Vernacexpr.bullet
+type t =
+    | Dash of int
+    | Star of int
+    | Plus of int
 
 let bullet_eq b1 b2 = match b1, b2 with
-| Vernacexpr.Dash n1, Vernacexpr.Dash n2 -> n1 = n2
-| Vernacexpr.Star n1, Vernacexpr.Star n2 -> n1 = n2
-| Vernacexpr.Plus n1, Vernacexpr.Plus n2 -> n1 = n2
+| Dash n1, Dash n2 -> n1 = n2
+| Star n1, Star n2 -> n1 = n2
+| Plus n1, Plus n2 -> n1 = n2
 | _ -> false
 
 let pr_bullet b =
   match b with
-  | Vernacexpr.Dash n -> Pp.(str (String.make n '-'))
-  | Vernacexpr.Star n -> Pp.(str (String.make n '*'))
-  | Vernacexpr.Plus n -> Pp.(str (String.make n '+'))
+  | Dash n -> Pp.(str (String.make n '-'))
+  | Star n -> Pp.(str (String.make n '*'))
+  | Plus n -> Pp.(str (String.make n '+'))
 
 
 type behavior = {
@@ -195,52 +198,5 @@ let put p b =
 let suggest p =
   (!current_behavior).suggest p
 
-(**********************************************************)
-(*                                                        *)
-(*                     Default goal selector              *)
-(*                                                        *)
-(**********************************************************)
-
-
-(* Default goal selector: selector chosen when a tactic is applied
-   without an explicit selector. *)
-let default_goal_selector = ref (Vernacexpr.SelectNth 1)
-let get_default_goal_selector () = !default_goal_selector
-
-let pr_range_selector (i, j) =
-  if i = j then Pp.int i
-  else Pp.(int i ++ str "-" ++ int j)
-
-let pr_goal_selector = function
-  | Vernacexpr.SelectAll -> Pp.str "all"
-  | Vernacexpr.SelectNth i -> Pp.int i
-  | Vernacexpr.SelectList l ->
-    Pp.(str "["
-     ++ prlist_with_sep pr_comma pr_range_selector l
-     ++ str "]")
-  | Vernacexpr.SelectId id -> Names.Id.print id
-
-let parse_goal_selector = function
-  | "all" -> Vernacexpr.SelectAll
-  | i ->
-      let err_msg = "The default selector must be \"all\" or a natural number." in
-      begin try
-              let i = int_of_string i in
-              if i < 0 then CErrors.user_err Pp.(str err_msg);
-              Vernacexpr.SelectNth i
-        with Failure _ -> CErrors.user_err Pp.(str err_msg)
-      end
-
-let _ =
-  Goptions.(declare_string_option{optdepr = false;
-                                  optname = "default goal selector" ;
-                                  optkey = ["Default";"Goal";"Selector"] ;
-                                  optread = begin fun () ->
-                                            Pp.string_of_ppcmds
-                                              (pr_goal_selector !default_goal_selector)
-                                            end;
-                                  optwrite = begin fun n ->
-                                    default_goal_selector := parse_goal_selector n
-                                  end
-                                 })
-
+let pr_goal_selector = Goal_select.pr_goal_selector
+let get_default_goal_selector = Goal_select.get_default_goal_selector
diff --git a/proofs/proof_bullet.mli b/proofs/proof_bullet.mli
index ffbaa0fa..a09a7ec1 100644
--- a/proofs/proof_bullet.mli
+++ b/proofs/proof_bullet.mli
@@ -14,7 +14,10 @@
 (*                                                        *)
 (**********************************************************)
 
-type t = Vernacexpr.bullet
+type t =
+    | Dash of int
+    | Star of int
+    | Plus of int
 
 (** A [behavior] is the data of a put function which
     is called when a bullet prefixes a tactic, a suggest function
@@ -42,12 +45,8 @@ val register_behavior : behavior -> unit
 val put : Proof.t -> t -> Proof.t
 val suggest : Proof.t -> Pp.t
 
-(**********************************************************)
-(*                                                        *)
-(*                     Default goal selector              *)
-(*                                                        *)
-(**********************************************************)
-
-val pr_goal_selector : Vernacexpr.goal_selector -> Pp.t
-val get_default_goal_selector : unit -> Vernacexpr.goal_selector
-
+(** Deprecated  *)
+val pr_goal_selector : Goal_select.t -> Pp.t
+[@@ocaml.deprecated "Please use [Goal_select.pr_goal_selector]"]
+val get_default_goal_selector : unit -> Goal_select.t
+[@@ocaml.deprecated "Please use [Goal_select.get_default_goal_selector]"]
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index d6c0e334..7e250faa 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -78,11 +78,14 @@ type proof_object = {
   universes: UState.t;
 }
 
+type opacity_flag = Opaque | Transparent
+
 type proof_ending =
   | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t
-  | Proved of Vernacexpr.opacity_flag *
-              Misctypes.lident option *
+  | Proved of opacity_flag *
+              lident option *
               proof_object
+
 type proof_terminator = proof_ending -> unit
 type closed_proof = proof_object * proof_terminator
 
@@ -90,11 +93,11 @@ type pstate = {
   pid : Id.t;  (* the name of the theorem whose proof is being constructed *)
   terminator : proof_terminator CEphemeron.key;
   endline_tactic : Genarg.glob_generic_argument option;
-  section_vars : Context.Named.t option;
+  section_vars : Constr.named_context option;
   proof : Proof.t;
   strength : Decl_kinds.goal_kind;
   mode : proof_mode CEphemeron.key;
-  universe_decl: Univdecls.universe_decl;
+  universe_decl: UState.universe_decl;
 }
 
 type t = pstate list
@@ -235,13 +238,6 @@ let activate_proof_mode mode =
 let disactivate_current_proof_mode () =
   CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ())
 
-let default_universe_decl =
-  let open Misctypes in
-  { univdecl_instance = [];
-    univdecl_extensible_instance = true;
-    univdecl_constraints = Univ.Constraint.empty;
-    univdecl_extensible_constraints = true }
-
 (** [start_proof sigma id pl str goals terminator] starts a proof of name
     [id] with goals [goals] (a list of pairs of environment and
     conclusion); [str] describes what kind of theorem/definition this
@@ -250,7 +246,7 @@ let default_universe_decl =
     end of the proof to close the proof. The proof is started in the
     evar map [sigma] (which can typically contain universe
     constraints), and with universe bindings pl. *)
-let start_proof sigma id ?(pl=default_universe_decl) str goals terminator =
+let start_proof sigma id ?(pl=UState.default_univ_decl) str goals terminator =
   let initial_state = {
     pid = id;
     terminator = CEphemeron.create terminator;
@@ -262,7 +258,7 @@ let start_proof sigma id ?(pl=default_universe_decl) str goals terminator =
     universe_decl = pl } in
   push initial_state pstates
 
-let start_dependent_proof id ?(pl=default_universe_decl) str goals terminator =
+let start_dependent_proof id ?(pl=UState.default_univ_decl) str goals terminator =
   let initial_state = {
     pid = id;
     terminator = CEphemeron.create terminator;
@@ -340,8 +336,8 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
      have existential variables in the initial types of goals, we need to
      normalise them for the kernel. *)
   let subst_evar k =
-    Proof.in_proof proof (fun m -> Evd.existential_opt_value m k) in
-  let nf = Universes.nf_evars_and_universes_opt_subst subst_evar
+    Proof.in_proof proof (fun m -> Evd.existential_opt_value0 m k) in
+  let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar
     (UState.subst universes) in
   let make_body =
     if poly || now then
@@ -352,9 +348,8 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
           not (Safe_typing.empty_private_constants = eff))
         in
         let typ = if allow_deferred then t else nf t in
-        let env = Global.env () in
-        let used_univs_body = Univops.universes_of_constr env body in
-        let used_univs_typ = Univops.universes_of_constr env typ in
+        let used_univs_body = Univops.universes_of_constr body in
+        let used_univs_typ = Univops.universes_of_constr typ in
         if allow_deferred then
           let initunivs = UState.const_univ_entry ~poly initial_euctx in
           let ctx = constrain_variables universes in
@@ -441,8 +436,8 @@ let return_proof ?(allow_partial=false) () =
   (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
       side-effects... This may explain why one need to uniquize side-effects
       thereafter... *)
-  let proofs = 
-    List.map (fun (c, _) -> (Evarutil.nf_evars_universes evd (EConstr.Unsafe.to_constr c), eff)) initial_goals in
+  let proofs =
+    List.map (fun (c, _) -> (EConstr.to_constr evd c, eff)) initial_goals in
     proofs, Evd.evar_universe_context evd
 
 let close_future_proof ~feedback_id proof =
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index bf35fd65..854ceaa4 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -22,7 +22,7 @@ val check_no_pending_proof : unit -> unit
 val get_current_proof_name : unit -> Names.Id.t
 val get_all_proof_names : unit -> Names.Id.t list
 
-val discard : Misctypes.lident -> unit
+val discard : Names.lident -> unit
 val discard_current : unit -> unit
 val discard_all : unit -> unit
 
@@ -48,11 +48,13 @@ type proof_object = {
   universes: UState.t;
 }
 
+type opacity_flag = Opaque | Transparent
+
 type proof_ending =
   | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry *
                 UState.t
-  | Proved of Vernacexpr.opacity_flag *
-              Misctypes.lident option *
+  | Proved of opacity_flag *
+              Names.lident option *
               proof_object
 type proof_terminator
 type closed_proof = proof_object * proof_terminator
@@ -69,14 +71,14 @@ val apply_terminator : proof_terminator -> proof_ending -> unit
     evar map [sigma] (which can typically contain universe
     constraints), and with universe bindings pl. *)
 val start_proof :
-  Evd.evar_map -> Names.Id.t -> ?pl:Univdecls.universe_decl ->
+  Evd.evar_map -> Names.Id.t -> ?pl:UState.universe_decl ->
   Decl_kinds.goal_kind -> (Environ.env * EConstr.types) list  ->
     proof_terminator -> unit
 
 (** Like [start_proof] except that there may be dependencies between
     initial goals. *)
 val start_dependent_proof :
-  Names.Id.t -> ?pl:Univdecls.universe_decl -> Decl_kinds.goal_kind ->
+  Names.Id.t -> ?pl:UState.universe_decl -> Decl_kinds.goal_kind ->
   Proofview.telescope -> proof_terminator -> unit
 
 (** Update the proofs global environment after a side-effecting command
@@ -124,11 +126,11 @@ val set_endline_tactic : Genarg.glob_generic_argument -> unit
  * (w.r.t. type dependencies and let-ins covered by it) + a list of
  * ids to be cleared *)
 val set_used_variables :
-  Names.Id.t list -> Context.Named.t * Misctypes.lident list
-val get_used_variables : unit -> Context.Named.t option
+  Names.Id.t list -> Constr.named_context * Names.lident list
+val get_used_variables : unit -> Constr.named_context option
 
 (** Get the universe declaration associated to the current proof. *)
-val get_universe_decl : unit -> Univdecls.universe_decl
+val get_universe_decl : unit -> UState.universe_decl
 
 module V82 : sig
   val get_current_initial_conclusions : unit -> Names.Id.t *(EConstr.types list *
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index 058e839b..197f71ca 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -5,6 +5,7 @@ Proof_type
 Logic
 Refine
 Proof
+Goal_select
 Proof_bullet
 Proof_global
 Redexpr
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 6fb41193..44685d2b 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -12,7 +12,7 @@ open Pp
 open CErrors
 open Util
 open Names
-open Term
+open Constr
 open EConstr
 open Declarations
 open Globnames
@@ -23,7 +23,6 @@ open Tacred
 open CClosure
 open RedFlags
 open Libobject
-open Misctypes
 
 (* call by value normalisation function using the virtual machine *)
 let cbv_vm env sigma c =
@@ -53,7 +52,7 @@ let whd_cbn flags env sigma t =
   Reductionops.Stack.zip ~refold:true sigma state
 
 let strong_cbn flags =
-  strong (whd_cbn flags)
+  strong_with_flags whd_cbn flags
 
 let simplIsCbn = ref (false)
 let _ = Goptions.declare_bool_option {
@@ -92,9 +91,9 @@ let cache_strategy (_,str) =
 
 let subst_strategy (subs,(local,obj)) =
   local,
-  List.smartmap
+  List.Smart.map
     (fun (k,ql as entry) ->
-      let ql' = List.smartmap (Mod_subst.subst_evaluable_reference subs) ql in
+      let ql' = List.Smart.map (Mod_subst.subst_evaluable_reference subs) ql in
       if ql==ql' then entry else (k,ql'))
     obj
 
@@ -200,8 +199,8 @@ let decl_red_expr s e =
   end
 
 let out_arg = function
-  | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable.")
-  | ArgArg x -> x
+  | Locus.ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable.")
+  | Locus.ArgArg x -> x
 
 let out_with_occurrences (occs,c) =
   (Locusops.occurrences_map (List.map out_arg) occs, c)
@@ -263,7 +262,7 @@ let subst_mps subst c =
   EConstr.of_constr (Mod_subst.subst_mps subst (EConstr.Unsafe.to_constr c))
 
 let subst_red_expr subs =
-  Miscops.map_red_expr_gen
+  Redops.map_red_expr_gen
     (subst_mps subs)
     (Mod_subst.subst_evaluable_reference subs)
     (Patternops.subst_pattern subs)
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 909556b1..198e057e 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -15,7 +15,7 @@ open Context.Named.Declaration
 module NamedDecl = Context.Named.Declaration
 
 let extract_prefix env info =
-  let ctx1 = List.rev (Environ.named_context env) in
+  let ctx1 = List.rev (EConstr.named_context env) in
   let ctx2 = List.rev (Evd.evar_context info) in
   let rec share l1 l2 accu = match l1, l2 with
   | d1 :: l1, d2 :: l2 ->
@@ -29,47 +29,34 @@ let typecheck_evar ev env sigma =
   let info = Evd.find sigma ev in
   (** Typecheck the hypotheses. *)
   let type_hyp (sigma, env) decl =
-    let t = EConstr.of_constr (NamedDecl.get_type decl) in
-    let evdref = ref sigma in
-    let _ = Typing.e_sort_of env evdref t in
-    let () = match decl with
-    | LocalAssum _ -> ()
-    | LocalDef (_,body,_) -> Typing.e_check env evdref (EConstr.of_constr body) t
+    let t = NamedDecl.get_type decl in
+    let sigma, _ = Typing.sort_of env sigma t in
+    let sigma = match decl with
+    | LocalAssum _ -> sigma
+    | LocalDef (_,body,_) -> Typing.check env sigma body t
     in
-    (!evdref, Environ.push_named decl env)
+    (sigma, EConstr.push_named decl env)
   in
   let (common, changed) = extract_prefix env info in
-  let env = Environ.reset_with_named_context (Environ.val_of_named_context common) env in
+  let env = Environ.reset_with_named_context (EConstr.val_of_named_context common) env in
   let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in
   (** Typecheck the conclusion *)
-  let evdref = ref sigma in
-  let _ = Typing.e_sort_of env evdref (EConstr.of_constr (Evd.evar_concl info)) in
-  !evdref
-
-let typecheck_proof c concl env sigma =
-  let evdref = ref sigma in
-  let () = Typing.e_check env evdref c concl in
-  !evdref
+  let sigma, _ = Typing.sort_of env sigma (Evd.evar_concl info) in
+  sigma
 
 let (pr_constrv,pr_constr) =
   Hook.make ~default:(fun _env _sigma _c -> Pp.str"<constr>") ()
 
 (* Get the side-effect's constant declarations to update the monad's
   * environmnent *)
-let add_if_undefined kn cb env =
-  try ignore(Environ.lookup_constant kn env); env
-  with Not_found -> Environ.add_constant kn cb env
+let add_if_undefined env eff =
+  let open Entries in
+  try ignore(Environ.lookup_constant eff.seff_constant env); env
+  with Not_found -> Environ.add_constant eff.seff_constant eff.seff_body env
 
 (* Add the side effects to the monad's environment, if not already done. *)
-let add_side_effect env = function
-  | { Entries.eff = Entries.SEsubproof (kn, cb, eff_env) } ->
-    add_if_undefined kn cb env
-  | { Entries.eff = Entries.SEscheme (l,_) } ->
-    List.fold_left (fun env (_,kn,cb,eff_env) ->
-        add_if_undefined kn cb env) env l
-
-let add_side_effects env effects =
-  List.fold_left (fun env eff -> add_side_effect env eff) env effects
+let add_side_effects env eff =
+  List.fold_left add_if_undefined env eff
 
 let generic_refine ~typecheck f gl =
   let sigma = Proofview.Goal.sigma gl in
@@ -93,7 +80,7 @@ let generic_refine ~typecheck f gl =
   let fold accu ev = typecheck_evar ev env accu in
   let sigma = if typecheck then Evd.fold_future_goals fold sigma evs else sigma in
   (** Check that the refined term is typesafe *)
-  let sigma = if typecheck then typecheck_proof c concl env sigma else sigma in
+  let sigma = if typecheck then Typing.check env sigma c concl else sigma in
   (** Check that the goal itself does not appear in the refined term *)
   let self = Proofview.Goal.goal gl in
   let _ =
@@ -106,7 +93,6 @@ let generic_refine ~typecheck f gl =
   let evs = Evd.map_filter_future_goals (Proofview.Unsafe.advance sigma) evs in
   let comb,shelf,given_up,evkmain = Evd.dispatch_future_goals evs in
   (** Proceed to the refinement *)
-  let c = EConstr.Unsafe.to_constr c in
   let sigma = match Proofview.Unsafe.advance sigma self with
   | None ->
     (** Nothing to do, the goal has been solved by side-effect *)
@@ -124,7 +110,8 @@ let generic_refine ~typecheck f gl =
   (** Mark goals *)
   let sigma = CList.fold_left Proofview.Unsafe.mark_as_goal sigma comb in
   let comb = CList.map (fun x -> Proofview.goal_with_state x state) comb in
-  let trace () = Pp.(hov 2 (str"simple refine"++spc()++ Hook.get pr_constrv env sigma c)) in
+  let trace () = Pp.(hov 2 (str"simple refine"++spc()++
+                            Hook.get pr_constrv env sigma (EConstr.Unsafe.to_constr c))) in
   Proofview.Trace.name_tactic trace (Proofview.tclUNIT v) >>= fun v ->
   Proofview.Unsafe.tclSETENV (Environ.reset_context env) <*>
   Proofview.Unsafe.tclEVARS sigma <*>
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 5cd703a2..0f83e16e 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -23,9 +23,12 @@ val pf_env  : goal sigma -> Environ.env
 val pf_hyps : goal sigma -> named_context
 
 val unpackage : 'a sigma -> evar_map ref * 'a
+[@@ocaml.deprecated "Do not use [evar_map ref]"]
 val repackage : evar_map ref -> 'a -> 'a sigma
+[@@ocaml.deprecated "Do not use [evar_map ref]"]
 val apply_sig_tac :
   evar_map ref -> (goal sigma -> goal list sigma) -> goal -> goal list
+[@@ocaml.deprecated "Do not use [evar_map ref]"]
 
 val refiner : rule -> tactic
 
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 1889054f..182b38d3 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -33,9 +33,11 @@ let re_sig it  gc = { it = it; sigma = gc; }
 type 'a sigma   = 'a Evd.sigma;;
 type tactic     = Proof_type.tactic;;
 
+[@@@ocaml.warning "-3"]
 let unpackage = Refiner.unpackage
 let repackage = Refiner.repackage
 let apply_sig_tac = Refiner.apply_sig_tac
+[@@@ocaml.warning "+3"]
 
 let sig_it   = Refiner.sig_it
 let project  = Refiner.project
@@ -73,7 +75,7 @@ let pf_ids_set_of_hyps gls =
 let pf_get_new_id id gls =
   next_ident_away id (pf_ids_set_of_hyps gls)
 
-let pf_global gls id = EConstr.of_constr (Universes.constr_of_global (Constrintern.construct_reference (pf_hyps gls) id))
+let pf_global gls id = EConstr.of_constr (UnivGen.constr_of_global (Constrintern.construct_reference (pf_hyps gls) id))
 
 let pf_reduction_of_red_expr gls re c =
   let (redfun, _) = reduction_of_red_expr (pf_env gls) re in
@@ -125,8 +127,8 @@ open Pp
 
 let db_pr_goal sigma g =
   let env = Goal.V82.env sigma g in
-  let penv = print_named_context env in
-  let pc = print_constr_env env sigma (Goal.V82.concl sigma g) in
+  let penv = Termops.Internal.print_named_context env in
+  let pc = Termops.Internal.print_constr_env env sigma (Goal.V82.concl sigma g) in
   str"  " ++ hv 0 (penv ++ fnl () ++
                    str "============================" ++ fnl ()  ++
                    str" "  ++ pc) ++ fnl ()
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 770d0940..31496fb3 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -30,9 +30,12 @@ val project : goal sigma -> evar_map
 val re_sig : 'a -> evar_map -> 'a sigma
 
 val unpackage : 'a sigma -> evar_map ref * 'a
+[@@ocaml.deprecated "Do not use [evar_map ref]"]
 val repackage : evar_map ref -> 'a -> 'a sigma
+[@@ocaml.deprecated "Do not use [evar_map ref]"]
 val apply_sig_tac :
   evar_map ref -> (goal sigma -> (goal list) sigma) -> goal -> (goal list)
+[@@ocaml.deprecated "Do not use [evar_map ref]"]
 
 val pf_concl              : goal sigma -> types
 val pf_env                : goal sigma -> env
@@ -95,7 +98,7 @@ val pr_glls   : goal list sigma -> Pp.t
 (* Variants of [Tacmach] functions built with the new proof engine *)
 module New : sig
   val pf_apply : (env -> evar_map -> 'a) -> Proofview.Goal.t -> 'a
-  val pf_global : Id.t -> Proofview.Goal.t -> Globnames.global_reference
+  val pf_global : Id.t -> Proofview.Goal.t -> GlobRef.t
   (** FIXME: encapsulate the level in an existential type. *)
   val of_old : (Proof_type.goal Evd.sigma -> 'a) -> Proofview.Goal.t -> 'a
 
diff --git a/proofs/tactypes.ml b/proofs/tactypes.ml
new file mode 100644
index 00000000..86a7e9c5
--- /dev/null
+++ b/proofs/tactypes.ml
@@ -0,0 +1,54 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** Tactic-related types that are not totally Ltac specific and still used in
+    lower API. It's not clear whether this is a temporary API or if this is
+    meant to stay. *)
+
+open Names
+
+(** Introduction patterns *)
+
+type 'constr intro_pattern_expr =
+  | IntroForthcoming of bool
+  | IntroNaming of Namegen.intro_pattern_naming_expr
+  | IntroAction of 'constr intro_pattern_action_expr
+and 'constr intro_pattern_action_expr =
+  | IntroWildcard
+  | IntroOrAndPattern of 'constr or_and_intro_pattern_expr
+  | IntroInjection of ('constr intro_pattern_expr) CAst.t list
+  | IntroApplyOn of 'constr CAst.t * 'constr intro_pattern_expr CAst.t
+  | IntroRewrite of bool
+and 'constr or_and_intro_pattern_expr =
+  | IntroOrPattern of ('constr intro_pattern_expr) CAst.t list list
+  | IntroAndPattern of ('constr intro_pattern_expr) CAst.t list
+
+(** Bindings *)
+
+type quantified_hypothesis = AnonHyp of int | NamedHyp of Id.t
+
+type 'a explicit_bindings = (quantified_hypothesis * 'a) CAst.t list
+
+type 'a bindings =
+  | ImplicitBindings of 'a list
+  | ExplicitBindings of 'a explicit_bindings
+  | NoBindings
+
+type 'a with_bindings = 'a * 'a bindings
+
+type 'a delayed_open = Environ.env -> Evd.evar_map -> Evd.evar_map * 'a
+
+type delayed_open_constr = EConstr.constr delayed_open
+type delayed_open_constr_with_bindings = EConstr.constr with_bindings delayed_open
+
+type intro_pattern = delayed_open_constr intro_pattern_expr CAst.t
+type intro_patterns = delayed_open_constr intro_pattern_expr CAst.t list
+type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr CAst.t
+type intro_pattern_naming = Namegen.intro_pattern_naming_expr CAst.t