Imported Upstream version 8.8.2upstream/8.8.2

33 files changed, 1413 insertions, 1493 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 0a90e0db..03ff580a 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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 Pp
@@ -12,11 +14,12 @@ open Util
 open Names
 open Nameops
 open Term
-open Vars
 open Termops
 open Namegen
 open Environ
 open Evd
+open EConstr
+open Vars
 open Reduction
 open Reductionops
 open Tacred
@@ -24,12 +27,6 @@ open Pretype_errors
 open Evarutil
 open Unification
 open Misctypes
-open Sigma.Notations
-
-(* Abbreviations *)
-
-let pf_env = Refiner.pf_env
-let pf_type_of gls c  = Typing.unsafe_type_of (pf_env gls) gls.sigma c
 
 (******************************************************************)
 (* Clausal environments *)
@@ -43,12 +40,6 @@ type clausenv = {
 let cl_env ce = ce.env
 let cl_sigma ce =  ce.evd
 
-let map_clenv sub clenv =
-  { templval = map_fl sub clenv.templval;
-    templtyp = map_fl sub clenv.templtyp;
-    evd = cmap sub clenv.evd;
-    env = clenv.env }
-
 let clenv_nf_meta clenv c = nf_meta clenv.evd c
 let clenv_term clenv c = meta_instance clenv.evd c
 let clenv_meta_type clenv mv = Typing.meta_type clenv.evd mv
@@ -56,9 +47,9 @@ let clenv_value clenv = meta_instance clenv.evd clenv.templval
 let clenv_type clenv = meta_instance clenv.evd clenv.templtyp
 
 let refresh_undefined_univs clenv =
-  match kind_of_term clenv.templval.rebus with
+  match EConstr.kind clenv.evd clenv.templval.rebus with
   | Var _ -> clenv, Univ.empty_level_subst
-  | App (f, args) when isVar f -> clenv, Univ.empty_level_subst
+  | App (f, args) when isVar clenv.evd f -> clenv, Univ.empty_level_subst
   | _ ->  
     let evd', subst = Evd.refresh_undefined_universes clenv.evd in
     let map_freelisted f = { f with rebus = subst_univs_level_constr subst f.rebus } in
@@ -71,15 +62,18 @@ 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 kind_of_term typ with
+  let rec clrec typ = match EConstr.kind cl.evd typ with
     | Cast (t,_,_) -> clrec t
     | Prod (na,t,u) ->
 	let mv = new_meta () in
-	let dep = dependent (mkRel 1) u 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 t ~name:na' cl.evd in
+	let e' = meta_declare mv (EConstr.Unsafe.to_constr 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;
@@ -103,14 +97,17 @@ let clenv_push_prod cl =
    and [ccl] is [forall y, Meta n1=y -> y=Meta n1] *)
 
 let clenv_environments evd bound t =
+  let open EConstr in
+  let open Vars in
   let rec clrec (e,metas) n t =
-    match n, kind_of_term t with
+    match n, EConstr.kind evd t with
       | (Some 0, _) -> (e, List.rev metas, t)
       | (n, Cast (t,_,_)) -> clrec (e,metas) n t
       | (n, Prod (na,t1,t2)) ->
 	  let mv = new_meta () in
-	  let dep = not (noccurn 1 t2) 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
 	  clrec (e', (mkMeta mv)::metas) (Option.map ((+) (-1)) n)
 	    (if dep then (subst1 (mkMeta mv) t2) else t2)
@@ -128,11 +125,13 @@ let mk_clenv_from_env env sigma n (c,cty) =
     env = env }
 
 let mk_clenv_from_n gls n (c,cty) =
-  mk_clenv_from_env (pf_env gls) gls.sigma n (c, cty)
+  let env = Proofview.Goal.env gls in
+  let sigma = Tacmach.New.project gls in
+  mk_clenv_from_env env sigma n (c, cty)
 
 let mk_clenv_from gls = mk_clenv_from_n gls None
 
-let mk_clenv_type_of gls t = mk_clenv_from gls (t,pf_type_of gls t)
+let mk_clenv_type_of gls t = mk_clenv_from gls (t,Tacmach.New.pf_unsafe_type_of gls t)
 
 (******************************************************************)
 
@@ -155,28 +154,28 @@ let error_incompatible_inst clenv mv  =
   let na = meta_name clenv.evd mv in
   match na with
       Name id ->
-        errorlabstrm "clenv_assign"
+        user_err ~hdr:"clenv_assign"
           (str "An incompatible instantiation has already been found for " ++
-           pr_id id)
+           Id.print id)
     | _ ->
-        anomaly ~label:"clenv_assign" (Pp.str "non dependent metavar already assigned")
+        anomaly ~label:"clenv_assign" (Pp.str "non dependent metavar already assigned.")
 
 (* TODO: replace by clenv_unify (mkMeta mv) rhs ? *)
 let clenv_assign mv rhs clenv =
   let rhs_fls = mk_freelisted rhs in
   if Metaset.exists (mentions clenv mv) rhs_fls.freemetas then
-    error "clenv_assign: circularity in unification";
+    user_err Pp.(str "clenv_assign: circularity in unification");
   try
     if meta_defined clenv.evd mv then
-      if not (Term.eq_constr (fst (meta_fvalue clenv.evd mv)).rebus rhs) then
+      if not (EConstr.eq_constr clenv.evd (EConstr.of_constr (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 (rhs_fls.rebus,st) clenv.evd}
+      {clenv with evd = meta_assign mv (EConstr.Unsafe.to_constr rhs_fls.rebus,st) clenv.evd}
   with Not_found ->
-    error "clenv_assign: undefined meta"
+    user_err Pp.(str "clenv_assign: undefined meta")
 
 
 
@@ -219,7 +218,7 @@ let clenv_assign mv rhs clenv =
 *)
 
 let clenv_metas_in_type_of_meta evd mv =
-  (mk_freelisted (meta_instance evd (meta_ftype evd mv))).freemetas
+  (mk_freelisted (meta_instance evd (map_fl EConstr.of_constr (meta_ftype evd mv)))).freemetas
 
 let dependent_in_type_of_metas clenv mvs =
   List.fold_right
@@ -262,35 +261,38 @@ let clenv_unify ?(flags=default_unify_flags ()) cv_pb t1 t2 clenv =
 let clenv_unify_meta_types ?(flags=default_unify_flags ()) clenv =
   { clenv with evd = w_unify_meta_types ~flags:flags clenv.env clenv.evd }
 
-let clenv_unique_resolver ?(flags=default_unify_flags ()) clenv gl =
-  let concl = Goal.V82.concl clenv.evd (sig_it gl) in
-  if isMeta (fst (decompose_appvect (whd_nored clenv.evd clenv.templtyp.rebus))) then
+let clenv_unique_resolver_gen ?(flags=default_unify_flags ()) clenv concl =
+  if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (whd_nored clenv.evd clenv.templtyp.rebus))) then
     clenv_unify CUMUL ~flags (clenv_type clenv) concl
       (clenv_unify_meta_types ~flags clenv)
   else
     clenv_unify CUMUL ~flags
       (meta_reducible_instance clenv.evd clenv.templtyp) concl clenv
 
+let old_clenv_unique_resolver ?flags clenv gl =
+  let concl = Goal.V82.concl clenv.evd (sig_it gl) in
+  clenv_unique_resolver_gen ?flags clenv concl
+
+let clenv_unique_resolver ?flags clenv gl =
+  let concl = Proofview.Goal.concl gl in
+  clenv_unique_resolver_gen ?flags clenv concl
+
 let adjust_meta_source evd mv = function
   | loc,Evar_kinds.VarInstance id ->
     let rec match_name c l =
-      match kind_of_term c, l with
-      | Lambda (Name id,_,c), a::l when Constr.equal a (mkMeta mv) -> Some id
+      match EConstr.kind evd c, l with
+      | Lambda (Name id,_,c), a::l when EConstr.eq_constr evd a (mkMeta mv) -> Some id
       | Lambda (_,_,c), a::l -> match_name c l
       | _ -> None in
     (* This is very ad hoc code so that an evar inherits the name of the binder
        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 t.rebus in
-        match kind_of_term f with
+        let f,l = decompose_app evd (EConstr.of_constr t.rebus) in
+        match EConstr.kind evd f with
         | Meta mv'' ->
           (match meta_opt_fvalue evd mv'' with
-          | Some (c,_) -> match_name c.rebus l
-          | None -> None)
-        | Evar ev ->
-          (match existential_opt_value evd ev with
-          | Some c -> match_name c l
+          | Some (c,_) -> match_name (EConstr.of_constr c.rebus) l
           | None -> None)
         | _ -> None
       else None in
@@ -332,13 +334,12 @@ let clenv_pose_metas_as_evars clenv dep_mvs =
       let ty = clenv_meta_type clenv mv in
       (* Postpone the evar-ization if dependent on another meta *)
       (* This assumes no cycle in the dependencies - is it correct ? *)
-      if occur_meta ty then fold clenv (mvs@[mv])
+      if occur_meta clenv.evd ty then fold clenv (mvs@[mv])
       else
         let src = evar_source_of_meta mv clenv.evd in
         let src = adjust_meta_source clenv.evd mv src in
-        let evd = Sigma.Unsafe.of_evar_map clenv.evd in
-	let Sigma (evar, evd, _) = new_evar (cl_env clenv) evd ~src ty in
-	let evd = Sigma.to_evar_map evd in
+        let evd = clenv.evd in
+	let (evd, evar) = new_evar (cl_env clenv) evd ~src ty in
 	let clenv = clenv_assign mv evar {clenv with evd=evd} in
 	fold clenv mvs in
   fold clenv dep_mvs
@@ -404,7 +405,7 @@ type arg_bindings = constr explicit_bindings
  * of cval, ctyp. *)
 
 let clenv_independent clenv =
-  let mvs = collect_metas (clenv_value clenv) in
+  let mvs = collect_metas clenv.evd (clenv_value clenv) in
   let ctyp_mvs = (mk_freelisted (clenv_type clenv)).freemetas in
   let deps = Metaset.union (dependent_in_type_of_metas clenv mvs) ctyp_mvs in
   List.filter (fun mv -> not (Metaset.mem mv deps)) mvs
@@ -415,13 +416,13 @@ let qhyp_eq h1 h2 = match h1, h2 with
 | _ -> false
 
 let check_bindings bl =
-  match List.duplicates qhyp_eq (List.map pi2 bl) with
+  match List.duplicates qhyp_eq (List.map (fun {CAst.v=x} -> fst x) bl) with
     | NamedHyp s :: _ ->
-	errorlabstrm ""
-	  (str "The variable " ++ pr_id s ++
+	user_err 
+	  (str "The variable " ++ Id.print s ++
 	   str " occurs more than once in binding list.");
     | AnonHyp n :: _ ->
-	errorlabstrm ""
+	user_err 
 	  (str "The position " ++ int n ++
 	   str " occurs more than once in binding list.")
     | [] -> ()
@@ -432,16 +433,16 @@ let explain_no_such_bound_variable evd id =
     | Cltyp (na, _) -> na
     | Clval (na, _, _) -> na
     in
-    if na != Anonymous then out_name na :: l else l
+    if na != Anonymous then Name.get_id na :: l else l
   in
   let mvl = List.fold_left fold [] (Evd.meta_list evd) in
-  errorlabstrm "Evd.meta_with_name"
-    (str"No such bound variable " ++ pr_id id ++
+  user_err ~hdr:"Evd.meta_with_name"
+    (str"No such bound variable " ++ Id.print id ++
      (if mvl == [] then str " (no bound variables at all in the expression)."
       else
         (str" (possible name" ++
          str (if List.length mvl == 1 then " is: " else "s are: ") ++
-         pr_enum pr_id mvl ++ str").")))
+         pr_enum Id.print mvl ++ str").")))
 
 let meta_with_name evd id =
   let na = Name id in
@@ -460,8 +461,8 @@ let meta_with_name evd id =
     | ([n],_|_,[n]) ->
         n
     | _  ->
-        errorlabstrm "Evd.meta_with_name"
-          (str "Binder name \"" ++ pr_id id ++
+        user_err ~hdr:"Evd.meta_with_name"
+          (str "Binder name \"" ++ Id.print id ++
            strbrk "\" occurs more than once in clause.")
 
 let meta_of_binder clause loc mvs = function
@@ -469,20 +470,20 @@ let meta_of_binder clause loc mvs = function
   | AnonHyp n ->
       try List.nth mvs (n-1)
       with (Failure _|Invalid_argument _) ->
-        errorlabstrm "" (str "No such binder.")
+        user_err  (str "No such binder.")
 
 let error_already_defined b =
   match b with
     | NamedHyp id ->
-        errorlabstrm ""
-          (str "Binder name \"" ++ pr_id id ++
+        user_err 
+          (str "Binder name \"" ++ Id.print id ++
            str"\" already defined with incompatible value.")
     | AnonHyp n ->
         anomaly
           (str "Position " ++ int n ++ str" already defined.")
 
 let clenv_unify_binding_type clenv c t u =
-  if isMeta (fst (decompose_appvect (whd_nored clenv.evd u))) then
+  if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (whd_nored clenv.evd u))) then
     (* Not enough information to know if some subtyping is needed *)
     CoerceToType, clenv, c
   else
@@ -499,8 +500,9 @@ let clenv_unify_binding_type clenv c t u =
 
 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.evd (clenv_get_type_of clenv c) 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 =
@@ -510,10 +512,10 @@ let clenv_match_args bl clenv =
     let mvs = clenv_independent clenv in
     check_bindings bl;
     List.fold_left
-      (fun clenv (loc,b,c) ->
+      (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 Term.eq_constr (fst (meta_fvalue clenv.evd k)).rebus c then clenv
+          if EConstr.eq_constr clenv.evd (EConstr.of_constr (fst (meta_fvalue clenv.evd k)).rebus) c then clenv
           else error_already_defined b
         else
 	  clenv_assign_binding clenv k c)
@@ -522,12 +524,12 @@ let clenv_match_args bl clenv =
 exception NoSuchBinding
 
 let clenv_constrain_last_binding c clenv =
-  let all_mvs = collect_metas clenv.templval.rebus in
+  let all_mvs = collect_metas clenv.evd clenv.templval.rebus in
   let k = try List.last all_mvs with Failure _ -> raise NoSuchBinding in
   clenv_assign_binding clenv k c
 
 let error_not_right_number_missing_arguments n =
-  errorlabstrm ""
+  user_err 
     (strbrk "Not the right number of missing arguments (expected " ++
       int n ++ str ").")
 
@@ -557,8 +559,9 @@ let make_clenv_binding_gen hyps_only n env sigma (c,t) = function
       let clause = mk_clenv_from_env env sigma n (c,t) in
       clenv_constrain_dep_args hyps_only largs clause
   | ExplicitBindings lbind ->
+      let t = rename_bound_vars_as_displayed sigma Id.Set.empty [] t in
       let clause = mk_clenv_from_env env sigma n
-	(c,rename_bound_vars_as_displayed [] [] t)
+	(c, t)
       in clenv_match_args lbind clause
   | NoBindings ->
       mk_clenv_from_env env sigma n (c,t)
@@ -585,34 +588,34 @@ let pr_clenv clenv =
 (** Evar version of mk_clenv *)
 
 type hole = {
-  hole_evar : constr;
-  hole_type : types;
+  hole_evar : EConstr.constr;
+  hole_type : EConstr.types;
   hole_deps  : bool;
   hole_name : Name.t;
 }
 
 type clause = {
   cl_holes : hole list;
-  cl_concl : types;
+  cl_concl : EConstr.types;
 }
 
 let make_evar_clause env sigma ?len t =
+  let open EConstr in
+  let open Vars in
   let bound = match len with
   | None -> -1
   | Some n -> assert (0 <= n); n
   in
   (** FIXME: do the renaming online *)
-  let t = rename_bound_vars_as_displayed [] [] t in
+  let t = rename_bound_vars_as_displayed sigma Id.Set.empty [] t in
   let rec clrec (sigma, holes) n t =
     if n = 0 then (sigma, holes, t)
-    else match kind_of_term t with
+    else match EConstr.kind sigma t with
     | Cast (t, _, _) -> clrec (sigma, holes) n t
     | Prod (na, t1, t2) ->
       let store = Typeclasses.set_resolvable Evd.Store.empty false in
-      let sigma = Sigma.Unsafe.of_evar_map sigma in
-      let Sigma (ev, sigma, _) = new_evar ~store env sigma t1 in
-      let sigma = Sigma.to_evar_map sigma in
-      let dep = dependent (mkRel 1) t2 in
+      let (sigma, ev) = new_evar ~store env sigma t1 in
+      let dep = not (noccurn sigma 1 t2) in
       let hole = {
         hole_evar = ev;
         hole_type = t1;
@@ -638,10 +641,10 @@ let explain_no_such_bound_variable holes id =
   let mvl = List.fold_right fold holes [] in
   let expl = match mvl with
   | [] -> str " (no bound variables at all in the expression)."
-  | [id] -> str "(possible name is: " ++ pr_id id ++ str ")."
-  | _ -> str "(possible names are: " ++ pr_enum pr_id mvl ++ str ")."
+  | [id] -> str "(possible name is: " ++ Id.print id ++ str ")."
+  | _ -> str "(possible names are: " ++ pr_enum Id.print mvl ++ str ")."
   in
-  errorlabstrm "" (str "No such bound variable " ++ pr_id id ++ expl)
+  user_err  (str "No such bound variable " ++ Id.print id ++ expl)
 
 let evar_with_name holes id =
   let map h = match h.hole_name with
@@ -653,38 +656,41 @@ let evar_with_name holes id =
   | [] -> explain_no_such_bound_variable holes id
   | [h] -> h.hole_evar
   | _ ->
-    errorlabstrm ""
-      (str "Binder name \"" ++ pr_id id ++
+    user_err 
+      (str "Binder name \"" ++ Id.print id ++
         str "\" occurs more than once in clause.")
 
 let evar_of_binder holes = function
 | NamedHyp s -> evar_with_name holes s
 | AnonHyp n ->
   try
-    let h = List.nth holes (pred n) in
+    let nondeps = List.filter (fun hole -> not hole.hole_deps) holes in
+    let h = List.nth nondeps (pred n) in
     h.hole_evar
   with e when CErrors.noncritical e ->
-    errorlabstrm "" (str "No such binder.")
+    user_err  (str "No such binder.")
 
 let define_with_type sigma env ev c =
+  let open EConstr in
   let t = Retyping.get_type_of env sigma ev in
   let ty = Retyping.get_type_of env sigma c in
   let j = Environ.make_judge c ty in
-  let (sigma, j) = Coercion.inh_conv_coerce_to true (Loc.ghost) env sigma j t in
-  let (ev, _) = destEvar ev in
-  let sigma = Evd.define ev j.Environ.uj_val sigma 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
   sigma
 
 let solve_evar_clause env sigma hyp_only clause = function
 | NoBindings -> sigma
 | ImplicitBindings largs ->
+  let open EConstr in
   let fold holes h =
     if h.hole_deps then
       (** Some subsequent term uses the hole *)
-      let (ev, _) = destEvar h.hole_evar in
-      let is_dep hole = occur_evar ev hole.hole_type in
+      let (ev, _) = destEvar sigma h.hole_evar in
+      let is_dep hole = occur_evar sigma ev hole.hole_type in
       let in_hyp = List.exists is_dep holes in
-      let in_ccl = occur_evar ev clause.cl_concl in
+      let in_ccl = occur_evar sigma ev clause.cl_concl in
       let dep = if hyp_only then in_hyp && not in_ccl else in_hyp || in_ccl in
       let h = { h with hole_deps = dep } in
       h :: holes
@@ -704,7 +710,7 @@ let solve_evar_clause env sigma hyp_only clause = function
     error_not_right_number_missing_arguments len
 | ExplicitBindings lbind ->
   let () = check_bindings lbind in
-  let fold sigma (_, binder, c) =
+  let fold sigma {CAst.v=(binder, c)} =
     let ev = evar_of_binder clause.cl_holes binder in
     define_with_type sigma env ev c
   in
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index e9236b1d..b85c4fc5 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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)         *)
 (************************************************************************)
 
 (** This file defines clausenv, which is a deprecated way to handle open terms
@@ -11,9 +13,10 @@
     evar-based clauses. *)
 
 open Names
-open Term
+open Constr
 open Environ
 open Evd
+open EConstr
 open Unification
 open Misctypes
 
@@ -28,8 +31,6 @@ type clausenv = {
   templtyp : constr freelisted (** its type *)}
 
 
-val map_clenv : (constr -> constr) -> clausenv -> clausenv
-
 (** subject of clenv (instantiated) *)
 val clenv_value     : clausenv -> constr
 
@@ -37,16 +38,16 @@ val clenv_value     : clausenv -> constr
 val clenv_type      : clausenv -> types
 
 (** substitute resolved metas *)
-val clenv_nf_meta   : clausenv -> constr -> constr
+val clenv_nf_meta   : clausenv -> EConstr.constr -> EConstr.constr
 
 (** type of a meta in clenv context *)
 val clenv_meta_type : clausenv -> metavariable -> types
 
-val mk_clenv_from : Goal.goal sigma -> constr * types -> clausenv
+val mk_clenv_from : Proofview.Goal.t -> EConstr.constr * EConstr.types -> clausenv
 val mk_clenv_from_n :
-  Goal.goal sigma -> int option -> constr * types -> clausenv
-val mk_clenv_type_of : Goal.goal sigma -> constr -> clausenv
-val mk_clenv_from_env : env -> evar_map -> int option -> constr * types -> clausenv
+  Proofview.Goal.t -> int option -> EConstr.constr * EConstr.types -> clausenv
+val mk_clenv_type_of : Proofview.Goal.t -> EConstr.constr -> clausenv
+val mk_clenv_from_env : env -> evar_map -> int option -> EConstr.constr * EConstr.types -> clausenv
 
 (** Refresh the universes in a clenv *)
 val refresh_undefined_univs : clausenv -> clausenv * Univ.universe_level_subst
@@ -63,9 +64,12 @@ val clenv_unify :
   ?flags:unify_flags -> conv_pb -> constr -> constr -> clausenv -> clausenv
 
 (** unifies the concl of the goal with the type of the clenv *)
-val clenv_unique_resolver :
+val old_clenv_unique_resolver :
   ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv
 
+val clenv_unique_resolver :
+  ?flags:unify_flags -> clausenv -> Proofview.Goal.t -> clausenv
+
 val clenv_dependent : clausenv -> metavariable list
 
 val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv
@@ -92,25 +96,25 @@ val clenv_unify_meta_types : ?flags:unify_flags -> clausenv -> clausenv
    the optional int tells how many prods of the lemma have to be used 
    use all of them if None *)
 val make_clenv_binding_env_apply :
-  env -> evar_map -> int option -> constr * constr -> constr bindings ->
+  env -> evar_map -> int option -> EConstr.constr * EConstr.constr -> constr bindings ->
    clausenv
 
 val make_clenv_binding_apply :
-  env -> evar_map -> int option -> constr * constr -> constr bindings ->
+  env -> evar_map -> int option -> EConstr.constr * EConstr.constr -> constr bindings ->
    clausenv
 
 val make_clenv_binding_env :
-  env -> evar_map -> constr * constr -> constr bindings -> clausenv
+  env -> evar_map -> EConstr.constr * EConstr.constr -> constr bindings -> clausenv
 
 val make_clenv_binding :
-  env -> evar_map -> constr * constr -> constr bindings -> clausenv
+  env -> evar_map -> EConstr.constr * EConstr.constr -> constr bindings -> clausenv
 
 (** if the clause is a product, add an extra meta for this product *)
 exception NotExtensibleClause
 val clenv_push_prod : clausenv -> clausenv
 
 (** {6 Pretty-print (debug only) } *)
-val pr_clenv : clausenv -> Pp.std_ppcmds
+val pr_clenv : clausenv -> Pp.t
 
 (** {6 Evar-based clauses} *)
 
@@ -134,9 +138,9 @@ val pr_clenv : clausenv -> Pp.std_ppcmds
 *)
 
 type hole = {
-  hole_evar : constr;
+  hole_evar : EConstr.constr;
   (** The hole itself. Guaranteed to be an evar. *)
-  hole_type : types;
+  hole_type : EConstr.types;
   (** Type of the hole in the current environment. *)
   hole_deps  : bool;
   (** Whether the remainder of the clause was dependent in the hole. Note that
@@ -148,10 +152,10 @@ type hole = {
 
 type clause = {
   cl_holes : hole list;
-  cl_concl : types;
+  cl_concl : EConstr.types;
 }
 
-val make_evar_clause : env -> evar_map -> ?len:int -> types ->
+val make_evar_clause : env -> evar_map -> ?len:int -> EConstr.types ->
   (evar_map * clause)
 (** An evar version of {!make_clenv_binding}. Given a type [t],
     [evar_environments env sigma ~len t bl] tries to eliminate at most [len]
@@ -159,7 +163,7 @@ val make_evar_clause : env -> evar_map -> ?len:int -> types ->
     type together with the list of holes generated. Assumes that [t] is
     well-typed in the environment. *)
 
-val solve_evar_clause : env -> evar_map -> bool -> clause -> constr bindings ->
+val solve_evar_clause : env -> evar_map -> bool -> clause -> EConstr.constr bindings ->
   evar_map
 (** [solve_evar_clause env sigma hyps cl bl] tries to solve the holes contained
     in [cl] according to the [bl] argument. Assumes that [bl] are well-typed in
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 98b5bc8b..209104ac 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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 Util
@@ -11,12 +13,12 @@ open Names
 open Term
 open Termops
 open Evd
+open EConstr
 open Refiner
 open Logic
 open Reduction
 open Tacmach
 open Clenv
-open Proofview.Notations
 
 (* This function put casts around metavariables whose type could not be
  * infered by the refiner, that is head of applications, predicates and
@@ -26,19 +28,19 @@ open Proofview.Notations
 
 let clenv_cast_meta clenv =
   let rec crec u =
-    match kind_of_term u with
+    match EConstr.kind clenv.evd u with
       | App _ | Case _ -> crec_hd u
-      | Cast (c,_,_) when isMeta c -> u
+      | Cast (c,_,_) when isMeta clenv.evd c -> u
       | Proj (p, c) -> mkProj (p, crec_hd c)
-      | _  -> map_constr crec u
+      | _  -> EConstr.map clenv.evd crec u
 
   and crec_hd u =
-    match kind_of_term (strip_outer_cast u) with
+    match EConstr.kind clenv.evd (strip_outer_cast clenv.evd u) with
       | Meta mv ->
 	  (try
             let b = Typing.meta_type clenv.evd mv in
-	    assert (not (occur_meta b));
-	    if occur_meta b then u
+	    assert (not (occur_meta clenv.evd b));
+	    if occur_meta clenv.evd b then u
             else mkCast (mkMeta mv, DEFAULTcast, b)
 	  with Not_found -> u)
       | App(f,args) -> mkApp (crec_hd f, Array.map crec args)
@@ -54,9 +56,10 @@ let clenv_value_cast_meta clenv =
 
 let clenv_pose_dependent_evars with_evars 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
     raise
-      (RefinerError (UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs)));
+      (RefinerError (env, sigma, UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs)));
   clenv_pose_metas_as_evars clenv dep_mvs
 
 (** Use our own fast path, more informative than from Typeclasses *)
@@ -103,10 +106,10 @@ open Unification
 let dft = default_unify_flags
 
 let res_pf ?(with_evars=false) ?(with_classes=true) ?(flags=dft ()) clenv =
-  Proofview.Goal.enter { enter = begin fun gl ->
-    let clenv gl = clenv_unique_resolver ~flags clenv gl in
-    clenv_refine with_evars ~with_classes (Tacmach.New.of_old clenv (Proofview.Goal.assume gl))
-  end }
+  Proofview.Goal.enter begin fun gl ->
+    let clenv = clenv_unique_resolver ~flags clenv gl in
+    clenv_refine with_evars ~with_classes clenv
+  end
 
 (* [unifyTerms] et [unify] ne semble pas gérer les Meta, en
    particulier ne semblent pas vérifier que des instances différentes
@@ -138,12 +141,12 @@ let fail_quick_unif_flags = {
 
 (* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *)
 let unify ?(flags=fail_quick_unif_flags) m =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let env = Tacmach.New.pf_env gl in
-    let n = Tacmach.New.pf_concl (Proofview.Goal.assume gl) in
+    let n = Tacmach.New.pf_concl gl in
     let evd = clear_metas (Tacmach.New.project gl) in
     try
       let evd' = w_unify env evd CONV ~flags m n in
 	Proofview.Unsafe.tclEVARSADVANCE evd'
     with e when CErrors.noncritical e -> Proofview.tclZERO e
-  end }
+  end
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index aa091aec..7c1e300b 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -1,17 +1,19 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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)         *)
 (************************************************************************)
 
 (** Legacy components of the previous proof engine. *)
 
-open Term
 open Clenv
-open Tacexpr
+open EConstr
 open Unification
+open Misctypes
 
 (** Tactics *)
 val unify : ?flags:unify_flags -> constr -> unit Proofview.tactic
diff --git a/proofs/doc.tex b/proofs/doc.tex
deleted file mode 100644
index 431027ef..00000000
--- a/proofs/doc.tex
+++ /dev/null
@@ -1,14 +0,0 @@
-
-\newpage
-\section*{The Proof Engine}
-
-\ocwsection \label{proofs}
-This chapter describes the \Coq\ proof engine, which is also called
-the ``refiner'', since it provides a way to build terms by successive
-refining steps. Those steps are either primitive rules or higher-level
-tactics.
-The modules of the proof engine are organized as follows.
-
-\bigskip
-\begin{center}\epsfig{file=proofs.dep.ps,width=\linewidth}\end{center}
-
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 29cad063..0d197c92 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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 CErrors
@@ -13,35 +15,41 @@ open Evd
 open Evarutil
 open Evarsolve
 open Pp
+open Glob_term
+open Ltac_pretype
 
 (******************************************)
 (* Instantiation of existential variables *)
 (******************************************)
 
-let depends_on_evar evk _ (pbty,_,t1,t2) =
-  try Evar.equal (head_evar t1) evk
+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 t2) evk
+  try Evar.equal (head_evar sigma t2) evk
   with NoHeadEvar -> false
 
 let define_and_solve_constraints evk c env evd =
-  if Termops.occur_evar evk c then
+  if Termops.occur_evar evd evk c then
     Pretype_errors.error_occur_check env evd evk c;
-  let evd = define evk c evd in
-  let (evd,pbs) = extract_changed_conv_pbs evd (depends_on_evar evk) in
+  let evd = define evk (EConstr.Unsafe.to_constr 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 t1 t2
+	| Success evd -> Evarconv.evar_conv_x full_transparent_state env evd pbty (EConstr.of_constr t1) (EConstr.of_constr t2)
 	| UnifFailure _ as x -> x) (Success evd)
       pbs
   with
     | Success evd -> evd
-    | UnifFailure _ -> error "Instance does not satisfy the constraints."
+    | UnifFailure _ -> user_err Pp.(str "Instance does not satisfy the constraints.")
 
 let w_refine (evk,evi) (ltac_var,rawc) sigma =
   if Evd.is_defined sigma evk then
-    error "Instantiate called on already-defined evar";
+    user_err Pp.(str "Instantiate called on already-defined evar");
   let env = Evd.evar_filtered_env evi in
   let sigma',typed_c =
     let flags = {
@@ -51,11 +59,11 @@ 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 evi.evar_concl) rawc
+      env sigma ltac_var (Pretyping.OfType (EConstr.of_constr evi.evar_concl)) rawc
     with e when CErrors.noncritical e ->
       let loc = Glob_ops.loc_of_glob_constr rawc in
-      user_err_loc
-        (loc,"", str "Instance is not well-typed in the environment of " ++
-                 pr_existential_key sigma evk ++ str ".")
+      user_err ?loc 
+                (str "Instance is not well-typed in the environment of " ++
+                 Termops.pr_existential_key sigma evk ++ str ".")
   in
   define_and_solve_constraints evk typed_c env (evars_reset_evd sigma' sigma)
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index e3778e94..e8f3c4d1 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -1,15 +1,20 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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 Evd
-open Pretyping
+open Glob_term
+open Ltac_pretype
 
 (** Refinement of existential variables. *)
 
-val w_refine : evar * evar_info ->
+type glob_constr_ltac_closure = ltac_var_map * glob_constr
+
+val w_refine : Evar.t * evar_info ->
   glob_constr_ltac_closure -> evar_map -> evar_map
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 111a947a..ba7e458f 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -1,28 +1,28 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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 Util
 open Pp
-open Term
-open Sigma.Notations
-open Context.Named.Declaration
+
+module NamedDecl = Context.Named.Declaration
 
 (* This module implements the abstract interface to goals *)
 (* A general invariant of the module, is that a goal whose associated
    evar is defined in the current evar_map, should not be accessed. *)
 
 (* type of the goals *)
-type goal = Evd.evar
+type goal = Evar.t
 
 let pr_goal e = str "GOAL:" ++ Pp.int (Evar.repr e)
 
 let uid e = string_of_int (Evar.repr e)
-let get_by_uid u = Evar.unsafe_of_int (int_of_string u)
 
 (* Layer to implement v8.2 tactic engine ontop of the new architecture.
    Types are different from what they used to be due to a change of the
@@ -48,7 +48,7 @@ module V82 = struct
   (* Access to ".evar_concl" *)
   let concl evars gl =
     let evi = Evd.find evars gl in
-    evi.Evd.evar_concl
+    EConstr.of_constr evi.Evd.evar_concl
 
   (* Access to ".evar_extra" *)
   let extra evars gl =
@@ -61,24 +61,22 @@ 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 prev_future_goals = Evd.future_goals evars in
-    let prev_principal_goal = Evd.principal_future_goal evars in
+    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;
 		Evd.evar_filter = Evd.Filter.identity;
 		Evd.evar_body = Evd.Evar_empty;
-		Evd.evar_source = (Loc.ghost,Evar_kinds.GoalEvar);
+		Evd.evar_source = (Loc.tag Evar_kinds.GoalEvar);
 		Evd.evar_candidates = None;
 		Evd.evar_extra = extra }
     in
     let evi = Typeclasses.mark_unresolvable evi in
-    let evars = Sigma.Unsafe.of_evar_map evars in
-    let Sigma (evk, evars, _) = Evarutil.new_pure_evar_full evars evi in
-    let evars = Sigma.to_evar_map evars in
-    let evars = Evd.restore_future_goals evars prev_future_goals prev_principal_goal in
+    let (evars, evk) = Evarutil.new_pure_evar_full evars evi in
+    let evars = Evd.restore_future_goals evars prev_future_goals in
     let ctxt = Environ.named_context_of_val hyps in
-    let inst = Array.map_of_list (mkVar % get_id) ctxt in
-    let ev = Term.mkEvar (evk,inst) in
+    let inst = Array.map_of_list (NamedDecl.get_id %> EConstr.mkVar) ctxt in
+    let ev = EConstr.mkEvar (evk,inst) in
     (evk, ev, evars)
 
   (* Instantiates a goal with an open term *)
@@ -88,7 +86,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 c sigma
+    Evd.define evk (EConstr.Unsafe.to_constr c) sigma
 
   (* Instantiates a goal with an open term, using name of goal for evk' *)
   let partial_solution_to sigma evk evk' c =
@@ -102,7 +100,7 @@ module V82 = struct
   let same_goal evars1 gl1 evars2 gl2 =
     let evi1 = Evd.find evars1 gl1 in
     let evi2 = Evd.find evars2 gl2 in
-    Term.eq_constr evi1.Evd.evar_concl evi2.Evd.evar_concl &&
+    Constr.equal evi1.Evd.evar_concl evi2.Evd.evar_concl &&
     Environ.eq_named_context_val evi1.Evd.evar_hyps evi2.Evd.evar_hyps
 
   let weak_progress glss gls =
@@ -130,9 +128,7 @@ module V82 = struct
     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 = Sigma.Unsafe.of_evar_map Evd.empty in
-    let Sigma (evk, sigma, _) = Evarutil.new_pure_evar_full sigma new_evi in
-    let sigma = Sigma.to_evar_map sigma 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 *)
@@ -144,14 +140,16 @@ module V82 = struct
 
   (* Goal represented as a type, doesn't take into account section variables *)
   let abstract_type sigma gl =
+    let open EConstr in
     let (gl,sigma) = nf_evar sigma gl in
     let env = env sigma gl in
     let genv = Global.env () in
     let is_proof_var decl =
-      try ignore (Environ.lookup_named (get_id decl) genv); false
+      try ignore (Environ.lookup_named (NamedDecl.get_id decl) genv); false
       with Not_found -> true in
     Environ.fold_named_context_reverse (fun t decl ->
 					  if is_proof_var decl then
+                                            let decl = Termops.map_named_decl EConstr.of_constr decl in
 					    mkNamedProd_or_LetIn decl t
 					  else
 					    t
diff --git a/proofs/goal.mli b/proofs/goal.mli
index 6a79c1f4..dc986315 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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)         *)
 (************************************************************************)
 
 (** This module implements the abstract interface to goals. Most of the code
@@ -15,12 +17,9 @@ type goal = Evar.t
 (* Gives a unique identifier to each goal. The identifier is
    guaranteed to contain no space. *)
 val uid : goal -> string
-(* Returns the goal (even if it has been partially solved)
-   corresponding to a unique identifier obtained by {!uid}. *)
-val get_by_uid : string -> goal
 
 (* Debugging help *)
-val pr_goal : goal -> Pp.std_ppcmds
+val pr_goal : goal -> Pp.t
 
 (* Layer to implement v8.2 tactic engine ontop of the new architecture. 
    Types are different from what they used to be due to a change of the
@@ -38,7 +37,7 @@ module V82 : sig
   val nf_hyps : Evd.evar_map -> goal -> Environ.named_context_val
 
   (* Access to ".evar_concl" *)
-  val concl : Evd.evar_map -> goal -> Term.constr
+  val concl : Evd.evar_map -> goal -> EConstr.constr
 
   (* Access to ".evar_extra" *)
   val extra : Evd.evar_map -> goal -> Evd.Store.t
@@ -48,23 +47,20 @@ module V82 : sig
        the evar corresponding to the goal, and an updated evar_map. *)
   val mk_goal : Evd.evar_map -> 
                          Environ.named_context_val ->
-                         Term.constr ->
+                         EConstr.constr ->
                          Evd.Store.t ->
-                         goal * Term.constr * Evd.evar_map
+                         goal * EConstr.constr * Evd.evar_map
 
   (* Instantiates a goal with an open term *)
-  val partial_solution : Evd.evar_map -> goal -> Term.constr -> Evd.evar_map
+  val partial_solution : Evd.evar_map -> goal -> EConstr.constr -> Evd.evar_map
 
   (* Instantiates a goal with an open term, reusing name of goal for
      second goal *)
-  val partial_solution_to : Evd.evar_map -> goal -> goal -> Term.constr -> Evd.evar_map
+  val partial_solution_to : Evd.evar_map -> goal -> goal -> EConstr.constr -> Evd.evar_map
 
-  (* Principal part of the weak-progress tactical *)
-  val weak_progress : goal list Evd.sigma -> goal Evd.sigma -> bool
-   
   (* Principal part of the progress tactical *)
   val progress : goal list Evd.sigma -> goal Evd.sigma -> bool
-    
+
  (* Principal part of tclNOTSAMEGOAL *)
   val same_goal : Evd.evar_map -> goal -> Evd.evar_map -> goal -> bool
 
@@ -75,6 +71,6 @@ module V82 : sig
   val nf_evar : Evd.evar_map -> goal -> goal * Evd.evar_map
 
   (* Goal represented as a type, doesn't take into account section variables *)
-  val abstract_type : Evd.evar_map -> goal -> Term.types 
+  val abstract_type : Evd.evar_map -> goal -> EConstr.types 
 
 end
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 65497c80..e5294715 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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 Pp
@@ -11,7 +13,7 @@ open CErrors
 open Util
 open Names
 open Nameops
-open Term
+open Constr
 open Vars
 open Termops
 open Environ
@@ -22,7 +24,8 @@ open Proof_type
 open Type_errors
 open Retyping
 open Misctypes
-open Context.Named.Declaration
+
+module NamedDecl = Context.Named.Declaration
 
 type refiner_error =
 
@@ -32,14 +35,14 @@ type refiner_error =
   | CannotApply of constr * constr
   | NotWellTyped of constr
   | NonLinearProof of constr
-  | MetaInType of constr
+  | MetaInType of EConstr.constr
 
   (* Errors raised by the tactics *)
   | IntroNeedsProduct
   | DoesNotOccurIn of constr * Id.t
   | NoSuchHyp of Id.t
 
-exception RefinerError of refiner_error
+exception RefinerError of Environ.env * Evd.evar_map * refiner_error
 
 open Pretype_errors
 
@@ -68,7 +71,7 @@ let catchable_exception = function
   | PretypeError(_,_, e) -> is_unification_error e || is_typing_error e 
   | _ -> false
 
-let error_no_such_hypothesis id = raise (RefinerError (NoSuchHyp id))
+let error_no_such_hypothesis env sigma id = raise (RefinerError (env, sigma, NoSuchHyp id))
 
 (* Tells if the refiner should check that the submitted rules do not
    produce invalid subgoals *)
@@ -77,34 +80,20 @@ let with_check = Flags.with_option check
 
 (* [apply_to_hyp sign id f] splits [sign] into [tail::[id,_,_]::head] and
    returns [tail::(f head (id,_,_) (rev tail))] *)
-let apply_to_hyp check sign id f =
+let apply_to_hyp env sigma check sign id f =
   try apply_to_hyp sign id f
   with Hyp_not_found ->
-    if check then error_no_such_hypothesis id
+    if check then error_no_such_hypothesis env sigma id
     else sign
 
 let check_typability env sigma c =
-  if !check then let _ = unsafe_type_of env sigma c in ()
+  if !check then let _ = unsafe_type_of env sigma (EConstr.of_constr c) in ()
 
 (************************************************************************)
 (************************************************************************)
 (* Implementation of the structural rules (moving and deleting
    hypotheses around) *)
 
-(* The Clear tactic: it scans the context for hypotheses to be removed
-   (instead of iterating on the list of identifier to be removed, which
-   forces the user to give them in order). *)
-
-let clear_hyps env sigma ids sign cl =
-  let evdref = ref (Evd.clear_metas sigma) in
-  let (hyps,cl) = Evarutil.clear_hyps_in_evi env evdref sign cl ids in
-  (hyps, cl, !evdref)
-
-let clear_hyps2 env sigma ids sign t cl =
-  let evdref = ref (Evd.clear_metas sigma) in
-  let (hyps,t,cl) = Evarutil.clear_hyps2_in_evi env evdref sign t cl ids in
-  (hyps, t, cl, !evdref)
-
 (* The ClearBody tactic *)
 
 (* Reordering of the context *)
@@ -136,33 +125,33 @@ let find_q x (m,q) =
         else find (Id.Set.union l accs) (i::acc) itl in
   find Id.Set.empty [] q
 
-let occur_vars_in_decl env hyps d =
+let occur_vars_in_decl env sigma hyps d =
   if Id.Set.is_empty hyps then false else
-    let ohyps = global_vars_set_of_decl env d in
+    let ohyps = global_vars_set_of_decl env sigma d in
     Id.Set.exists (fun h -> Id.Set.mem h ohyps) hyps
 
-let reorder_context env sign ord =
+let reorder_context env sigma sign ord =
   let ords = List.fold_right Id.Set.add ord Id.Set.empty in
   if not (Int.equal (List.length ord) (Id.Set.cardinal ords)) then
-    error "Order list has duplicates";
+    user_err Pp.(str "Order list has duplicates");
   let rec step ord expected ctxt_head moved_hyps ctxt_tail =
     match ord with
       | [] -> List.rev ctxt_tail @ ctxt_head
       | top::ord' when mem_q top moved_hyps ->
           let ((d,h),mh) = find_q top moved_hyps in
-          if occur_vars_in_decl env h d then
-            errorlabstrm "reorder_context"
-              (str "Cannot move declaration " ++ pr_id top ++ spc() ++
+          if occur_vars_in_decl env sigma h d then
+            user_err ~hdr:"reorder_context"
+              (str "Cannot move declaration " ++ Id.print top ++ spc() ++
               str "before " ++
-              pr_sequence pr_id
+              pr_sequence Id.print
                 (Id.Set.elements (Id.Set.inter h
-                  (global_vars_set_of_decl env d))));
+                  (global_vars_set_of_decl env sigma d))));
           step ord' expected ctxt_head mh (d::ctxt_tail)
       | _ ->
           (match ctxt_head with
-            | [] -> error_no_such_hypothesis (List.hd ord)
+            | [] -> error_no_such_hypothesis env sigma (List.hd ord)
             | d :: ctxt ->
-                let x = get_id d in
+                let x = NamedDecl.get_id d in
                 if Id.Set.mem x expected then
                   step ord (Id.Set.remove x expected)
                     ctxt (push_item x d moved_hyps) ctxt_tail
@@ -171,19 +160,21 @@ let reorder_context env sign ord =
                     ctxt (push_val x moved_hyps) (d::ctxt_tail)) in
   step ord ords sign mt_q []
 
-let reorder_val_context env sign ord =
-  val_of_named_context (reorder_context env (named_context_of_val sign) ord)
+let reorder_val_context env sigma sign ord =
+  let open EConstr in
+  val_of_named_context (reorder_context env sigma (named_context_of_val sign) ord)
 
 
 
 
-let check_decl_position env sign d =
-  let x = get_id d in
-  let needed = global_vars_set_of_decl env d in
-  let deps = dependency_closure env (named_context_of_val sign) needed in
+let check_decl_position env sigma sign d =
+  let open EConstr in
+  let x = NamedDecl.get_id d in
+  let needed = global_vars_set_of_decl env sigma d in
+  let deps = dependency_closure env sigma (named_context_of_val sign) needed in
   if Id.List.mem x deps then
-    errorlabstrm "Logic.check_decl_position"
-      (str "Cannot create self-referring hypothesis " ++ pr_id x);
+    user_err ~hdr:"Logic.check_decl_position"
+      (str "Cannot create self-referring hypothesis " ++ Id.print x);
   x::deps
 
 (* Auxiliary functions for primitive MOVE tactic
@@ -201,19 +192,11 @@ let move_location_eq m1 m2 = match m1, m2 with
 | MoveFirst, MoveFirst -> true
 | _ -> false
 
-let rec get_hyp_after h = function
-  | [] -> error_no_such_hypothesis h
-  | d :: right ->
-      if Id.equal (get_id d) h then
-	match right with d' ::_ -> MoveBefore (get_id d') | [] -> MoveFirst
-      else
-       get_hyp_after h right
-
-let split_sign hfrom hto l =
+let split_sign env sigma hfrom hto l =
   let rec splitrec left toleft = function
-    | [] -> error_no_such_hypothesis hfrom
+    | [] -> error_no_such_hypothesis env sigma hfrom
     | d :: right ->
-        let hyp,_,typ = to_tuple d in
+        let hyp = NamedDecl.get_id d in
       	if Id.equal hyp hfrom then
 	  (left,right,d, toleft || move_location_eq hto MoveLast)
       	else
@@ -231,31 +214,31 @@ let hyp_of_move_location = function
   | MoveBefore id -> id
   | _ -> assert false
 
-let move_hyp toleft (left,declfrom,right) hto =
+let move_hyp sigma toleft (left,declfrom,right) hto =
   let env = Global.env() in
   let test_dep d d2 =
     if toleft
-    then occur_var_in_decl env (get_id d2) d
-    else occur_var_in_decl env (get_id d) d2
+    then occur_var_in_decl env sigma (NamedDecl.get_id d2) d
+    else occur_var_in_decl env sigma (NamedDecl.get_id d) d2
   in
   let rec moverec first middle = function
     | [] ->
 	if match hto with MoveFirst | MoveLast -> false | _ -> true then
-	  error_no_such_hypothesis (hyp_of_move_location hto);
+          error_no_such_hypothesis env sigma (hyp_of_move_location hto);
 	List.rev first @ List.rev middle
-    | d :: _ as right when move_location_eq hto (MoveBefore (get_id d)) ->
+    | d :: _ as right when move_location_eq hto (MoveBefore (NamedDecl.get_id d)) ->
 	List.rev first @ List.rev middle @ right
     | d :: right ->
-        let hyp = get_id d in
+        let hyp = NamedDecl.get_id d in
 	let (first',middle') =
       	  if List.exists (test_dep d) middle then
 	    if not (move_location_eq hto (MoveAfter hyp)) then
 	      (first, d::middle)
             else
-	      errorlabstrm "move_hyp" (str "Cannot move " ++ pr_id (get_id declfrom) ++
-	        Miscprint.pr_move_location pr_id hto ++
-	        str (if toleft then ": it occurs in " else ": it depends on ")
-	        ++ pr_id hyp ++ str ".")
+	      user_err ~hdr:"move_hyp" (str "Cannot move " ++ Id.print (NamedDecl.get_id declfrom) ++
+	        Miscprint.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
 	    (d::first, middle)
 	in
@@ -264,6 +247,7 @@ let move_hyp toleft (left,declfrom,right) hto =
       	else
 	  moverec first' middle' right
   in
+  let open EConstr in
   if toleft then
     let right =
       List.fold_right push_named_context_val right empty_named_context_val in
@@ -276,10 +260,15 @@ let move_hyp toleft (left,declfrom,right) hto =
     List.fold_left (fun sign d -> push_named_context_val d sign)
       right left
 
-let move_hyp_in_named_context hfrom hto sign =
+let move_hyp_in_named_context env sigma hfrom hto sign =
+  let open EConstr in
   let (left,right,declfrom,toleft) =
-    split_sign hfrom hto (named_context_of_val sign) in
-  move_hyp toleft (left,declfrom,right) hto
+    split_sign env sigma hfrom hto (named_context_of_val sign) in
+  move_hyp sigma toleft (left,declfrom,right) hto
+
+let insert_decl_in_named_context sigma decl hto sign =
+  let open EConstr in
+  move_hyp sigma false ([],decl,named_context_of_val sign) hto
 
 (**********************************************************************)
 
@@ -292,43 +281,46 @@ let move_hyp_in_named_context hfrom hto sign =
 variables only in Application and Case *)
 
 let error_unsupported_deep_meta c =
-  errorlabstrm "" (strbrk "Application of lemmas whose beta-iota normal " ++
+  user_err  (strbrk "Application of lemmas whose beta-iota normal " ++
     strbrk "form contains metavariables deep inside the term is not " ++
     strbrk "supported; try \"refine\" instead.")
 
 let collect_meta_variables c =
-  let rec collrec deep acc c = match kind_of_term c with
+  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 _) -> fold_constr (collrec deep) acc c
+    | (App _| Case _) -> Constr.fold (collrec deep) acc c
     | Proj (_, c) -> collrec deep acc c
-    | _ -> fold_constr (collrec true) acc c
+    | _ -> Constr.fold (collrec true) acc c
   in
   List.rev (collrec false [] c)
 
-let check_meta_variables c =
+let check_meta_variables env sigma c =
   if not (List.distinct_f Int.compare (collect_meta_variables c)) then
-    raise (RefinerError (NonLinearProof c))
+    raise (RefinerError (env, sigma, NonLinearProof c))
 
 let check_conv_leq_goal env sigma arg ty conclty =
   if !check then
-    let evm, b = Reductionops.infer_conv env sigma ty conclty in
+    let evm, b = Reductionops.infer_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr conclty) in
       if b then evm 
-      else raise (RefinerError (BadType (arg,ty,conclty)))
+      else raise (RefinerError (env, sigma, BadType (arg,ty,conclty)))
   else sigma
 
-exception Stop of constr list
-let meta_free_prefix a =
+exception Stop of EConstr.t list
+let meta_free_prefix sigma a =
   try
+    let a = Array.map EConstr.of_constr a in
     let _ = Array.fold_left (fun acc a -> 
-      if occur_meta a then raise (Stop acc)
+      if occur_meta sigma a then raise (Stop acc)
       else a :: acc) [] a
     in a
   with Stop acc -> Array.rev_of_list acc
 
 let goal_type_of env sigma c =
-  if !check then unsafe_type_of env sigma c
-  else Retyping.get_type_of env sigma c
+  if !check then
+    let (sigma,t) = type_of env sigma (EConstr.of_constr c) in
+    (sigma, EConstr.Unsafe.to_constr t)
+  else (sigma, EConstr.Unsafe.to_constr (Retyping.get_type_of env sigma (EConstr.of_constr c)))
 
 let rec mk_refgoals sigma goal goalacc conclty trm =
   let env = Goal.V82.env sigma goal in
@@ -336,17 +328,20 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
   let mk_goal hyps concl =
     Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal)
   in
-    if (not !check) && not (occur_meta trm) then
-      let t'ty = Retyping.get_type_of env sigma trm in
+    if (not !check) && not (occur_meta sigma (EConstr.of_constr trm)) then
+      let t'ty = Retyping.get_type_of env sigma (EConstr.of_constr trm) in
+      let t'ty = EConstr.Unsafe.to_constr t'ty in
       let sigma = check_conv_leq_goal env sigma trm t'ty conclty in
         (goalacc,t'ty,sigma,trm)
     else
-      match kind_of_term trm with
+      match kind trm with
       | Meta _ ->
-	let conclty = nf_betaiota sigma conclty in
-	  if !check && occur_meta conclty then
-	    raise (RefinerError (MetaInType conclty));
+        let conclty = nf_betaiota env sigma (EConstr.of_constr conclty) in
+	  if !check && occur_meta sigma conclty then
+            raise (RefinerError (env, sigma, MetaInType conclty));
 	  let (gl,ev,sigma) = mk_goal hyps conclty in
+	  let ev = EConstr.Unsafe.to_constr ev in
+	  let conclty = EConstr.Unsafe.to_constr conclty in
 	  gl::goalacc, conclty, sigma, ev
 
       | Cast (t,k, ty) ->
@@ -365,26 +360,28 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 
       | App (f,l) ->
 	let (acc',hdty,sigma,applicand) =
-	  if is_template_polymorphic env f then
+	  if is_template_polymorphic env sigma (EConstr.of_constr f) then
 	    let ty = 
-	      (* Template sort-polymorphism of definition and inductive types *)
-	      let firstmeta = Array.findi (fun i x -> occur_meta x) l in
+	      (* Template polymorphism of definitions and inductive types *)
+	      let firstmeta = Array.findi (fun i x -> occur_meta sigma (EConstr.of_constr x)) l in
 	      let args, _ = Option.cata (fun i -> CArray.chop i l) (l, [||]) firstmeta in
-	        type_of_global_reference_knowing_parameters env sigma f args
+	        type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) (Array.map EConstr.of_constr args)
 	    in
+	    let ty = EConstr.Unsafe.to_constr ty in
 	      goalacc, ty, sigma, f
 	  else
 	    mk_hdgoals sigma goal goalacc f
 	in
 	let ((acc'',conclty',sigma), args) = mk_arggoals sigma goal acc' hdty l in
         let sigma = check_conv_leq_goal env sigma trm conclty' conclty in
-        let ans = if applicand == f && args == l then trm else Term.mkApp (applicand, args) in
+        let ans = if applicand == f && args == l then trm else mkApp (applicand, args) in
         (acc'',conclty',sigma, ans)
 
       | Proj (p,c) ->
 	let (acc',cty,sigma,c') = mk_hdgoals sigma goal goalacc c in
 	let c = mkProj (p, c') in
-	let ty = get_type_of env sigma c in
+	let ty = get_type_of env sigma (EConstr.of_constr c) in
+	let ty = EConstr.Unsafe.to_constr ty in
 	  (acc',ty,sigma,c)
 
       | Case (ci,p,c,lf) ->
@@ -399,14 +396,14 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
         let lf' = Array.rev_of_list rbranches in
         let ans =
           if p' == p && c' == c && Array.equal (==) lf' lf then trm
-          else Term.mkCase (ci,p',c',lf')
+          else mkCase (ci,p',c',lf')
         in
 	(acc'',conclty',sigma, ans)
 
       | _ ->
-	if occur_meta trm then
-	  anomaly (Pp.str "refiner called with a meta in non app/case subterm");
-	let t'ty = goal_type_of env sigma trm in
+	if occur_meta sigma (EConstr.of_constr trm) then
+	  anomaly (Pp.str "refiner called with a meta in non app/case subterm.");
+	let (sigma, t'ty) = goal_type_of env sigma trm in
 	let sigma = check_conv_leq_goal env sigma trm t'ty conclty in
           (goalacc,t'ty,sigma, trm)
 
@@ -418,10 +415,11 @@ and mk_hdgoals sigma goal goalacc trm =
   let hyps = Goal.V82.hyps sigma goal in
   let mk_goal hyps concl = 
     Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in
-  match kind_of_term trm with
+  match kind trm with
     | Cast (c,_, ty) when isMeta c ->
 	check_typability env sigma ty;
-	let (gl,ev,sigma) = mk_goal hyps (nf_betaiota sigma ty) in
+        let (gl,ev,sigma) = mk_goal hyps (nf_betaiota env sigma (EConstr.of_constr ty)) in
+	let ev = EConstr.Unsafe.to_constr ev in
 	gl::goalacc,ty,sigma,ev
 
     | Cast (t,_, ty) ->
@@ -430,14 +428,14 @@ and mk_hdgoals sigma goal goalacc trm =
 
     | App (f,l) ->
 	let (acc',hdty,sigma,applicand) =
-	  if is_template_polymorphic env f
+	  if is_template_polymorphic env sigma (EConstr.of_constr f)
 	  then
-	    let l' = meta_free_prefix l in	      
-	   (goalacc,type_of_global_reference_knowing_parameters env sigma f l',sigma,f)
+	    let l' = meta_free_prefix sigma l in
+	   (goalacc,EConstr.Unsafe.to_constr (type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) l'),sigma,f)
 	  else mk_hdgoals sigma goal goalacc f
 	in
 	let ((acc'',conclty',sigma), args) = mk_arggoals sigma goal acc' hdty l in
-        let ans = if applicand == f && args == l then trm else Term.mkApp (applicand, args) in
+        let ans = if applicand == f && args == l then trm else mkApp (applicand, args) in
 	(acc'',conclty',sigma, ans)
 
     | Case (ci,p,c,lf) ->
@@ -451,68 +449,74 @@ and mk_hdgoals sigma goal goalacc trm =
 	let lf' = Array.rev_of_list rbranches in
 	let ans =
           if p' == p && c' == c && Array.equal (==) lf' lf then trm
-          else Term.mkCase (ci,p',c',lf')
+          else mkCase (ci,p',c',lf')
 	in
 	(acc'',conclty',sigma, ans)
 
     | Proj (p,c) ->
          let (acc',cty,sigma,c') = mk_hdgoals sigma goal goalacc c in
 	 let c = mkProj (p, c') in
-         let ty = get_type_of env sigma c in
+         let ty = get_type_of env sigma (EConstr.of_constr c) in
+         let ty = EConstr.Unsafe.to_constr ty in
 	   (acc',ty,sigma,c)
 
     | _ ->
-	if !check && occur_meta trm then
-	  anomaly (Pp.str "refine called with a dependent meta");
-	goalacc, goal_type_of env sigma trm, sigma, trm
+	if !check && occur_meta sigma (EConstr.of_constr trm) then
+	  anomaly (Pp.str "refine called with a dependent meta.");
+        let (sigma, ty) = goal_type_of env sigma trm in
+	goalacc, ty, sigma, trm
 
 and mk_arggoals sigma goal goalacc funty allargs =
   let foldmap (goalacc, funty, sigma) harg =
-    let t = whd_all (Goal.V82.env sigma goal) sigma funty in
-    let rec collapse t = match kind_of_term t with
+    let t = whd_all (Goal.V82.env sigma goal) sigma (EConstr.of_constr funty) in
+    let t = EConstr.Unsafe.to_constr t in
+    let rec collapse t = match kind t with
     | LetIn (_, c1, _, b) -> collapse (subst1 c1 b)
     | _ -> t
     in
     let t = collapse t in
-    match kind_of_term t with
+    match kind t with
     | Prod (_, c1, b) ->
       let (acc, hargty, sigma, arg) = mk_refgoals sigma goal goalacc c1 harg in
       (acc, subst1 harg b, sigma), arg
-    | _ -> raise (RefinerError (CannotApply (t, harg)))
+    | _ ->
+      let env = Goal.V82.env sigma goal in
+      raise (RefinerError (env,sigma,CannotApply (t, harg)))
   in
   Array.smartfoldmap foldmap (goalacc, funty, sigma) allargs
 
 and mk_casegoals sigma goal goalacc p c =
   let env = Goal.V82.env sigma goal in
   let (acc',ct,sigma,c') = mk_hdgoals sigma goal goalacc c in
+  let ct = EConstr.of_constr ct in
   let (acc'',pt,sigma,p') = mk_hdgoals sigma goal acc' p in
-  let indspec =
+  let ((ind, u), spec) =
     try Tacred.find_hnf_rectype env sigma ct
-    with Not_found -> anomaly (Pp.str "mk_casegoals") in
-  let (lbrty,conclty) = type_case_branches_with_names env indspec p c in
+    with Not_found -> anomaly (Pp.str "mk_casegoals.") in
+  let indspec = ((ind, EConstr.EInstance.kind sigma u), spec) in
+  let (lbrty,conclty) = type_case_branches_with_names env sigma indspec p c in
   (acc'',lbrty,conclty,sigma,p',c')
 
 
 let convert_hyp check sign sigma d =
-  let id,b,bt = to_tuple d in
-  let env = Global.env() in
+  let id = NamedDecl.get_id d in
+  let b = NamedDecl.get_value d in
+  let env = Global.env () in
   let reorder = ref [] in
   let sign' =
-    apply_to_hyp check sign id
+    apply_to_hyp env sigma check sign id
       (fun _ d' _ ->
-        let _,c,ct = to_tuple d' in
+        let c = Option.map EConstr.of_constr (NamedDecl.get_value d') in
         let env = Global.env_of_context sign in
-        if check && not (is_conv env sigma bt ct) then
-	  errorlabstrm "Logic.convert_hyp"
-            (str "Incorrect change of the type of " ++ pr_id id ++ str ".");
+        if check && not (is_conv env sigma (NamedDecl.get_type d) (EConstr.of_constr (NamedDecl.get_type d'))) then
+	  user_err ~hdr:"Logic.convert_hyp"
+            (str "Incorrect change of the type of " ++ Id.print id ++ str ".");
         if check && not (Option.equal (is_conv env sigma) b c) then
-	  errorlabstrm "Logic.convert_hyp"
-            (str "Incorrect change of the body of "++ pr_id id ++ str ".");
-       if check then reorder := check_decl_position env sign d;
-       d) in
-  reorder_val_context env sign' !reorder
-
-
+	  user_err ~hdr:"Logic.convert_hyp"
+            (str "Incorrect change of the body of "++ Id.print id ++ str ".");
+       if check then reorder := check_decl_position env sigma sign d;
+       map_named_decl EConstr.Unsafe.to_constr d) in
+  reorder_val_context env sigma sign' !reorder
 
 (************************************************************************)
 (************************************************************************)
@@ -520,37 +524,13 @@ let convert_hyp check sign sigma d =
 
 let prim_refiner r sigma goal =
   let env = Goal.V82.env sigma goal in
-  let sign = Goal.V82.hyps sigma goal in
   let cl = Goal.V82.concl sigma goal in
-  let mk_goal hyps concl = 
-    Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) 
-  in
   match r with
     (* Logical rules *)
-    | Cut (b,replace,id,t) ->
-(*        if !check && not (Retyping.get_sort_of env sigma t) then*)
-        let (sg1,ev1,sigma) = mk_goal sign (nf_betaiota sigma t) in
-	let sign,t,cl,sigma =
-	  if replace then
-	    let nexthyp = get_hyp_after id (named_context_of_val sign) in
-	    let sign,t,cl,sigma = clear_hyps2 env sigma (Id.Set.singleton id) sign t cl in
-	    move_hyp false ([], LocalAssum (id,t),named_context_of_val sign)
-	      nexthyp,
-	      t,cl,sigma
-	  else
-            (if !check && mem_named_context_val id sign then
-	      errorlabstrm "Logic.prim_refiner"
-                (str "Variable " ++ pr_id id ++ str " is already declared.");
-	     push_named_context_val (LocalAssum (id,t)) sign,t,cl,sigma) in
-        let (sg2,ev2,sigma) = 
-	  Goal.V82.mk_goal sigma sign cl (Goal.V82.extra sigma goal) in
-	let oterm = Term.mkNamedLetIn id ev1 t ev2 in
-	let sigma = Goal.V82.partial_solution_to sigma goal sg2 oterm in
-        if b then ([sg1;sg2],sigma) else ([sg2;sg1],sigma)
-
     | Refine c ->
-	check_meta_variables c;
+        let cl = EConstr.Unsafe.to_constr cl in
+        check_meta_variables env sigma c;
 	let (sgl,cl',sigma,oterm) = mk_refgoals sigma goal [] cl c in
 	let sgl = List.rev sgl in
-	let sigma = Goal.V82.partial_solution sigma goal oterm in
+	let sigma = Goal.V82.partial_solution sigma goal (EConstr.of_constr oterm) in
 	  (sgl, sigma)
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 0dba9ef1..dc471bb5 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -1,15 +1,17 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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)         *)
 (************************************************************************)
 
 (** Legacy proof engine. Do not use in newly written code. *)
 
 open Names
-open Term
+open Constr
 open Evd
 open Proof_type
 
@@ -43,19 +45,25 @@ type refiner_error =
   | CannotApply of constr * constr
   | NotWellTyped of constr
   | NonLinearProof of constr
-  | MetaInType of constr
+  | MetaInType of EConstr.constr
 
   (*i Errors raised by the tactics i*)
   | IntroNeedsProduct
   | DoesNotOccurIn of constr * Id.t
   | NoSuchHyp of Id.t
 
-exception RefinerError of refiner_error
+exception RefinerError of Environ.env * evar_map * refiner_error
+
+val error_no_such_hypothesis : Environ.env -> evar_map -> Id.t -> 'a
 
 val catchable_exception : exn -> bool
 
 val convert_hyp : bool -> Environ.named_context_val -> evar_map ->
-  Context.Named.Declaration.t -> Environ.named_context_val
+  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 ->
+  Environ.named_context_val -> Environ.named_context_val
 
-val move_hyp_in_named_context : Id.t -> Id.t Misctypes.move_location ->
+val insert_decl_in_named_context : Evd.evar_map ->
+  EConstr.named_declaration -> Id.t Misctypes.move_location ->
   Environ.named_context_val -> Environ.named_context_val
diff --git a/proofs/miscprint.ml b/proofs/miscprint.ml
new file mode 100644
index 00000000..1a63ff67
--- /dev/null
+++ b/proofs/miscprint.ml
@@ -0,0 +1,77 @@
+(************************************************************************)
+(*         *   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 Pp
+open Names
+open Misctypes
+
+(** Printing of [intro_pattern] *)
+
+let rec pr_intro_pattern prc {CAst.v=pat} = match pat with
+  | IntroForthcoming true -> str "*"
+  | IntroForthcoming false -> str "**"
+  | IntroNaming p -> pr_intro_pattern_naming p
+  | IntroAction p -> pr_intro_pattern_action prc p
+
+and pr_intro_pattern_naming = function
+  | IntroIdentifier id -> Id.print id
+  | IntroFresh id -> str "?" ++ Id.print id
+  | IntroAnonymous -> str "?"
+
+and pr_intro_pattern_action prc = function
+  | IntroWildcard -> str "_"
+  | IntroOrAndPattern pll -> pr_or_and_intro_pattern prc pll
+  | IntroInjection pl ->
+      str "[=" ++ hv 0 (prlist_with_sep spc (pr_intro_pattern prc) pl) ++
+      str "]"
+  | IntroApplyOn ({CAst.v=c},pat) -> pr_intro_pattern prc pat ++ str "%" ++ prc c
+  | IntroRewrite true -> str "->"
+  | IntroRewrite false -> str "<-"
+
+and pr_or_and_intro_pattern prc = function
+  | IntroAndPattern pl ->
+      str "(" ++ hv 0 (prlist_with_sep pr_comma (pr_intro_pattern prc) pl) ++ str ")"
+  | IntroOrPattern pll ->
+      str "[" ++
+      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)
+  | {loc;v=(AnonHyp n, c)} -> hov 1 (int n ++ str " := " ++ cut () ++ prc c)
+
+let pr_bindings prc prlc = function
+  | ImplicitBindings l ->
+    brk (1,1) ++ str "with" ++ brk (1,1) ++
+    pr_sequence prc l
+  | ExplicitBindings l ->
+    brk (1,1) ++ str "with" ++ brk (1,1) ++
+    pr_sequence (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
+  | NoBindings -> mt ()
+
+let pr_bindings_no_with prc prlc = function
+  | ImplicitBindings l ->
+    brk (0,1) ++ prlist_with_sep spc prc l
+  | ExplicitBindings l ->
+    brk (0,1) ++ prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
+  | NoBindings -> mt ()
+
+let pr_with_bindings prc prlc (c,bl) =
+  hov 1 (prc c ++ pr_bindings prc prlc bl)
+
diff --git a/proofs/miscprint.mli b/proofs/miscprint.mli
new file mode 100644
index 00000000..79790a27
--- /dev/null
+++ b/proofs/miscprint.mli
@@ -0,0 +1,39 @@
+(************************************************************************)
+(*         *   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 Misctypes
+
+(** Printing of [intro_pattern] *)
+
+val pr_intro_pattern :
+  ('a -> Pp.t) -> 'a intro_pattern_expr CAst.t -> Pp.t
+
+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
+
+(** 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
+
+val pr_bindings_no_with :
+  ('a -> Pp.t) ->
+  ('a -> Pp.t) -> 'a bindings -> Pp.t
+
+val pr_with_bindings :
+  ('a -> Pp.t) ->
+  ('a -> Pp.t) -> 'a * 'a bindings -> Pp.t
+
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index eddbf72a..5d137988 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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 Pp
@@ -15,7 +17,7 @@ open Evd
 
 let use_unification_heuristics_ref = ref true
 let _ = Goptions.declare_bool_option {
-  Goptions.optsync = true; Goptions.optdepr = false;
+  Goptions.optdepr = false;
   Goptions.optname = "Solve unification constraints at every \".\"";
   Goptions.optkey = ["Solve";"Unification";"Constraints"];
   Goptions.optread = (fun () -> !use_unification_heuristics_ref);
@@ -24,19 +26,6 @@ let _ = Goptions.declare_bool_option {
 
 let use_unification_heuristics () = !use_unification_heuristics_ref
 
-let refining = Proof_global.there_are_pending_proofs
-let check_no_pending_proofs = Proof_global.check_no_pending_proof
-
-let get_current_proof_name = Proof_global.get_current_proof_name
-let get_all_proof_names = Proof_global.get_all_proof_names
-
-type lemma_possible_guards = Proof_global.lemma_possible_guards
-type universe_binders = Proof_global.universe_binders
-
-let delete_proof = Proof_global.discard
-let delete_current_proof = Proof_global.discard_current
-let delete_all_proofs = Proof_global.discard_all
-
 let start_proof (id : Id.t) ?pl str sigma hyps c ?init_tac terminator =
   let goals = [ (Global.env_of_context hyps , c) ] in
   Proof_global.start_proof sigma id ?pl str goals terminator;
@@ -55,44 +44,31 @@ let cook_this_proof p =
 let cook_proof () =
   cook_this_proof (fst
     (Proof_global.close_proof ~keep_body_ucst_separate:false (fun x -> x)))
-let get_pftreestate () =
-  Proof_global.give_me_the_proof ()
-
-let set_end_tac tac =
-  Proof_global.set_endline_tactic tac
-
-let set_used_variables l =
-  Proof_global.set_used_variables l
-let get_used_variables () =
-  Proof_global.get_used_variables ()
-
-let get_universe_binders () =
-  Proof_global.get_universe_binders ()
 
 exception NoSuchGoal
 let _ = CErrors.register_handler begin function
-  | NoSuchGoal -> CErrors.error "No such goal."
+  | NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.")
   | _ -> raise CErrors.Unhandled
 end
+
 let get_nth_V82_goal i =
   let p = Proof_global.give_me_the_proof () in
-  let { it=goals ; sigma = sigma; } = Proof.V82.subgoals p in
-  try
-          { it=(List.nth goals (i-1)) ; sigma=sigma; }
+  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
   (sigma, Refiner.pf_env { it=goal ; sigma=sigma; })
 
 let get_goal_context i =
   try get_goal_context_gen i
-  with Proof_global.NoCurrentProof -> CErrors.error "No focused proof."
-     | NoSuchGoal -> CErrors.error "No such goal."
+  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
-  with Proof_global.NoCurrentProof -> CErrors.error "No focused proof."
+  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,
         there is no accessible evar either *)
@@ -106,14 +82,14 @@ let get_current_context () =
     (Evd.from_env env, env)
      | NoSuchGoal ->
         (* No more focused goals ? *)
-        let p = get_pftreestate () in
+        let p = Proof_global.give_me_the_proof () in
         let evd = Proof.in_proof p (fun x -> x) in
         (evd, Global.env ())
 
 let current_proof_statement () =
   match Proof_global.V82.get_current_initial_conclusions () with
     | (id,([concl],strength)) -> id,strength,concl
-    | _ -> CErrors.anomaly ~label:"Pfedit.current_proof_statement" (Pp.str "more than one statement")
+    | _ -> CErrors.anomaly ~label:"Pfedit.current_proof_statement" (Pp.str "more than one statement.")
 
 let solve ?with_end_tac gi info_lvl tac pr =
   try 
@@ -143,12 +119,7 @@ let solve ?with_end_tac gi info_lvl tac pr =
     in
     (p,status)
   with
-    | Proof_global.NoCurrentProof  -> CErrors.error "No focused proof"
-    | CList.IndexOutOfRange ->
-        match gi with
-	| Vernacexpr.SelectNth i -> let msg = str "No such goal: " ++ int i ++ str "." in
-	                            CErrors.errorlabstrm "" msg
-        | _ -> assert false
+    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)
 
@@ -170,11 +141,12 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo
   try
     let status = by tac in
     let _,(const,univs,_) = cook_proof () in
-    delete_current_proof ();
-    const, status, fst univs
+    Proof_global.discard_current ();
+    let univs = UState.demote_seff_univs const univs in
+    const, status, univs
   with reraise ->
     let reraise = CErrors.push reraise in
-    delete_current_proof ();
+    Proof_global.discard_current ();
     iraise reraise
 
 let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac =
@@ -186,12 +158,11 @@ let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac =
   let ce =
     if side_eff then Safe_typing.inline_private_constants_in_definition_entry env ce
     else { ce with
-      const_entry_body = Future.chain ~pure:true ce.const_entry_body
-        (fun (pt, _) -> pt, Safe_typing.empty_private_constants) } in
-  let (cb, ctx), se = Future.force ce.const_entry_body in
-  let univs' = Evd.merge_context_set Evd.univ_rigid (Evd.from_ctx univs) ctx in
-  assert(Safe_typing.empty_private_constants = se);
-  cb, status, Evd.evar_universe_context univs'
+      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
+  cb, status, univs
 
 let refine_by_tactic env sigma ty tac =
   (** Save the initial side-effects to restore them afterwards. We set the
@@ -199,6 +170,8 @@ let refine_by_tactic env sigma ty tac =
       ones created during the tactic invocation easily. *)
   let eff = Evd.eval_side_effects sigma in
   let sigma = Evd.drop_side_effects sigma in
+  (** Save the existing goals *)
+  let prev_future_goals = save_future_goals sigma in
   (** Start a proof *)
   let prf = Proof.start sigma [env, ty] in
   let (prf, _) =
@@ -209,17 +182,30 @@ let refine_by_tactic env sigma ty tac =
       iraise (e, info)
   in
   (** Plug back the retrieved sigma *)
-  let sigma = Proof.in_proof prf (fun sigma -> sigma) in
+  let (goals,stack,shelf,given_up,sigma) = Proof.proof prf in
+  assert (stack = []);
   let ans = match Proof.initial_goals prf with
   | [c, _] -> c
   | _ -> assert false
   in
   let ans = Reductionops.nf_evar sigma ans in
+  let ans = EConstr.Unsafe.to_constr ans in
   (** [neff] contains the freshly generated side-effects *)
   let neff = Evd.eval_side_effects sigma in
   (** Reset the old side-effects *)
   let sigma = Evd.drop_side_effects sigma in
   let sigma = Evd.emit_side_effects eff sigma in
+  (** Restore former goals *)
+  let sigma = restore_future_goals sigma prev_future_goals in
+  (** Push remaining goals as future_goals which is the only way we
+      have to inform the caller that there are goals to collect while
+      not being encapsulated in the monad *)
+  (** Goals produced by tactic "shelve" *)
+  let sigma = List.fold_right (Evd.declare_future_goal ~tag:Evd.ToShelve) shelf sigma in
+  (** Goals produced by tactic "give_up" *)
+  let sigma = List.fold_right (Evd.declare_future_goal ~tag:Evd.ToGiveUp) given_up sigma in
+  (** Other goals *)
+  let sigma = List.fold_right Evd.declare_future_goal goals sigma in
   (** Get rid of the fresh side-effects by internalizing them in the term
       itself. Note that this is unsound, because the tactic may have solved
       other goals that were already present during its invocation, so that
@@ -238,20 +224,25 @@ let declare_implicit_tactic tac = implicit_tactic := Some tac
 
 let clear_implicit_tactic () = implicit_tactic := None
 
-let solve_by_implicit_tactic env sigma evk =
+let apply_implicit_tactic tac = (); fun env sigma evk ->
   let evi = Evd.find_undefined sigma evk in
-  match (!implicit_tactic, snd (evar_source evk sigma)) with
-  | Some tac, (Evar_kinds.ImplicitArg _ | Evar_kinds.QuestionMark _)
+  match snd (evar_source evk sigma) with
+  | (Evar_kinds.ImplicitArg _ | Evar_kinds.QuestionMark _)
       when
-	Context.Named.equal (Environ.named_context_of_val evi.evar_hyps)
+	Context.Named.equal Constr.equal (Environ.named_context_of_val evi.evar_hyps)
 	(Environ.named_context env) ->
-      let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (CErrors.UserError ("",Pp.str"Proof is not complete."))) []) in
+      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 = EConstr.of_constr c in
         if Evarutil.has_undefined_evars sigma c then raise Exit;
         let (ans, _, ctx) =
 	  build_by_tactic env (Evd.evar_universe_context sigma) c tac in
         let sigma = Evd.set_universe_context sigma ctx in
-        sigma, ans
+        sigma, EConstr.of_constr ans
        with e when Logic.catchable_exception e -> raise Exit)
   | _ -> raise Exit
+
+let solve_by_implicit_tactic () = match !implicit_tactic with
+| None -> None
+| Some tac -> Some (apply_implicit_tactic tac)
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index ea604e08..65cde3a3 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -1,52 +1,20 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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)         *)
 (************************************************************************)
 
 (** Global proof state. A quite redundant wrapper on {!Proof_global}. *)
 
-open Loc
 open Names
-open Term
+open Constr
 open Environ
 open Decl_kinds
 
-(** Several proofs can be opened simultaneously but at most one is
-   focused at some time. The following functions work by side-effect
-   on current set of open proofs. In this module, ``proofs'' means an
-   open proof (something started by vernacular command [Goal], [Lemma]
-   or [Theorem]), and ``goal'' means a subgoal of the current focused
-   proof *)
-
-(** {6 ... } *)
-(** [refining ()] tells if there is some proof in progress, even if a not
-   focused one *)
-
-val refining : unit -> bool
-
-(** [check_no_pending_proofs ()] fails if there is still some proof in
-   progress *)
-
-val check_no_pending_proofs : unit -> unit
-
-(** {6 ... } *)
-(** [delete_proof name] deletes proof of name [name] or fails if no proof
-    has this name *)
-
-val delete_proof : Id.t located -> unit
-
-(** [delete_current_proof ()] deletes current focused proof or fails if
-    no proof is focused *)
-
-val delete_current_proof : unit -> unit
-
-(** [delete_all_proofs ()] deletes all open proofs if any *)
-
-val delete_all_proofs : unit -> unit
-
 (** {6 ... } *)
 (** [start_proof s str env t hook tac] starts a proof of name [s] and
     conclusion [t]; [hook] is optionally a function to be applied at
@@ -55,12 +23,8 @@ val delete_all_proofs : unit -> unit
     systematically apply at initialization time (e.g. to start the
     proof of mutually dependent theorems) *)
 
-type lemma_possible_guards = Proof_global.lemma_possible_guards
-
-type universe_binders = Id.t Loc.located list
-
 val start_proof :
-  Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map -> named_context_val -> constr ->
+  Id.t -> ?pl:Univdecls.universe_decl -> goal_kind -> Evd.evar_map -> named_context_val -> EConstr.constr ->
   ?init_tac:unit Proofview.tactic ->
   Proof_global.proof_terminator -> unit
 
@@ -73,18 +37,13 @@ val start_proof :
 val cook_this_proof :
     Proof_global.proof_object ->
   (Id.t *
-    (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * goal_kind))
+    (Safe_typing.private_constants Entries.definition_entry * UState.t * goal_kind))
 
 val cook_proof : unit ->
   (Id.t *
-    (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * goal_kind))
+    (Safe_typing.private_constants Entries.definition_entry * UState.t * goal_kind))
 
 (** {6 ... } *)
-(** [get_pftreestate ()] returns the current focused pending proof.
-   @raise NoCurrentProof if there is no pending proof. *)
-
-val get_pftreestate : unit -> Proof.proof
-
 (** [get_goal_context n] returns the context of the [n]th subgoal of
    the current focused proof or raises a [UserError] if there is no
    focused proof or if there is no more subgoals *)
@@ -106,37 +65,10 @@ val get_current_context : unit -> Evd.evar_map * env
 (** [current_proof_statement] *)
 
 val current_proof_statement :
-  unit -> Id.t * goal_kind * types
+  unit -> Id.t * goal_kind * EConstr.types
 
 (** {6 ... } *)
-(** [get_current_proof_name ()] return the name of the current focused
-    proof or failed if no proof is focused *)
-
-val get_current_proof_name : unit -> Id.t
 
-(** [get_all_proof_names ()] returns the list of all pending proof names.
-    The first name is the current proof, the other names may come in
-    any order. *)
-
-val get_all_proof_names : unit -> Id.t list
-
-(** {6 ... } *)
-(** [set_end_tac tac] applies tactic [tac] to all subgoal generate
-    by [solve] *)
-
-val set_end_tac : Tacexpr.raw_tactic_expr -> unit
-
-(** {6 ... } *)
-(** [set_used_variables l] declares that section variables [l] will be
-    used in the proof *)
-val set_used_variables :
-  Id.t list -> Context.section_context * (Loc.t * Names.Id.t) list
-val get_used_variables : unit -> Context.section_context option
-
-(** {6 Universe binders } *)
-val get_universe_binders : unit -> universe_binders option
-
-(** {6 ... } *)
 (** [solve (SelectNth n) tac] applies tactic [tac] to the [n]th
     subgoal of the current focused proof or raises a [UserError] if no
     proof is focused or if there is no [n]th subgoal. [solve SelectAll
@@ -144,7 +76,7 @@ val get_universe_binders : unit -> universe_binders option
 
 val solve : ?with_end_tac:unit Proofview.tactic ->
       Vernacexpr.goal_selector -> int option -> unit Proofview.tactic ->
-      Proof.proof -> Proof.proof*bool
+      Proof.t -> Proof.t * bool
 
 (** [by tac] applies tactic [tac] to the 1st subgoal of the current
     focused proof or raises a UserError if there is no focused proof or
@@ -165,16 +97,16 @@ val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> unit
     tactic. *)
 
 val build_constant_by_tactic :
-  Id.t -> Evd.evar_universe_context -> named_context_val -> ?goal_kind:goal_kind ->
-  types -> unit Proofview.tactic -> 
+  Id.t -> UState.t -> named_context_val -> ?goal_kind:goal_kind ->
+  EConstr.types -> unit Proofview.tactic -> 
   Safe_typing.private_constants Entries.definition_entry * bool *
-    Evd.evar_universe_context
+    UState.t
 
-val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?poly:polymorphic ->
-  types -> unit Proofview.tactic -> 
-  constr * bool * Evd.evar_universe_context
+val build_by_tactic : ?side_eff:bool -> env -> UState.t -> ?poly:polymorphic ->
+  EConstr.types -> unit Proofview.tactic -> 
+  constr * bool * UState.t
 
-val refine_by_tactic : env -> Evd.evar_map -> types -> unit Proofview.tactic ->
+val refine_by_tactic : env -> Evd.evar_map -> EConstr.types -> unit Proofview.tactic ->
   constr * Evd.evar_map
 (** A variant of the above function that handles open terms as well.
     Caveat: all effects are purged in the returned term at the end, but other
@@ -190,4 +122,4 @@ val declare_implicit_tactic : unit Proofview.tactic -> unit
 val clear_implicit_tactic : unit -> unit
 
 (* Raise Exit if cannot solve *)
-val solve_by_implicit_tactic : env -> Evd.evar_map -> Evd.evar -> Evd.evar_map * constr
+val solve_by_implicit_tactic : unit -> Pretyping.inference_hook option
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 5c963d53..51e0a1d6 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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)         *)
 (************************************************************************)
 
 (* Module defining the last essential tiles of interactive proofs.
@@ -66,14 +68,14 @@ exception FullyUnfocused
 
 let _ = CErrors.register_handler begin function
   | CannotUnfocusThisWay ->
-    CErrors.error "This proof is focused, but cannot be unfocused this way"
+    CErrors.user_err Pp.(str "This proof is focused, but cannot be unfocused this way")
   | NoSuchGoals (i,j) when Int.equal i j ->
-      CErrors.errorlabstrm "Focus" Pp.(str"No such goal (" ++ int i ++ str").")
+      CErrors.user_err ~hdr:"Focus" Pp.(str"No such goal (" ++ int i ++ str").")
   | NoSuchGoals (i,j) ->
-      CErrors.errorlabstrm "Focus" Pp.(
+      CErrors.user_err ~hdr:"Focus" Pp.(
         str"Not every goal in range ["++ int i ++ str","++int j++str"] exist."
       )
-  | FullyUnfocused -> CErrors.error "The proof is not focused"
+  | FullyUnfocused -> CErrors.user_err Pp.(str "The proof is not focused")
   | _ -> raise CErrors.Unhandled
 end
 
@@ -98,7 +100,7 @@ let done_cond ?(loose_end=false) k = CondDone (loose_end,k)
 
 (* Subpart of the type of proofs. It contains the parts of the proof which
    are under control of the undo mechanism *)
-type proof = {
+type t = {
   (* Current focused proofview *)
   proofview: Proofview.proofview;
   (* Entry for the proofview *)
@@ -112,9 +114,11 @@ type proof = {
   (* List of goals that have been given up *)
   given_up : Goal.goal list;
   (* The initial universe context (for the statement) *)
-  initial_euctx : Evd.evar_universe_context
+  initial_euctx : UState.t
 }
 
+type proof = t
+
 (*** General proof functions ***)
 
 let proof p =
@@ -163,6 +167,7 @@ let map_structured_proof pfts process_goal: 'a pre_goals =
 let rec unroll_focus pv = function
   | (_,_,ctx)::stk -> unroll_focus (Proofview.unfocus ctx pv) stk
   | [] -> pv
+
 (* spiwack: a proof is considered completed even if its still focused, if the focus
    doesn't hide any goal.
    Unfocusing is handled in {!return}. *)
@@ -301,10 +306,10 @@ exception HasShelvedGoals
 exception HasGivenUpGoals
 exception HasUnresolvedEvar
 let _ = CErrors.register_handler begin function
-  | UnfinishedProof -> CErrors.error "Some goals have not been solved."
-  | HasShelvedGoals -> CErrors.error "Some goals have been left on the shelf."
-  | HasGivenUpGoals -> CErrors.error "Some goals have been given up."
-  | HasUnresolvedEvar -> CErrors.error "Some existential variables are uninstantiated."
+  | UnfinishedProof -> CErrors.user_err Pp.(str "Some goals have not been solved.")
+  | HasShelvedGoals -> CErrors.user_err Pp.(str "Some goals have been left on the shelf.")
+  | HasGivenUpGoals -> CErrors.user_err Pp.(str "Some goals have been given up.")
+  | HasUnresolvedEvar -> CErrors.user_err Pp.(str "Some existential variables are uninstantiated.")
   | _ -> raise CErrors.Unhandled
 end
 
@@ -342,7 +347,11 @@ let run_tactic env tac pr =
     Proofview.tclEVARMAP >>= fun sigma ->
     (* Already solved goals are not to be counted as shelved. Nor are
       they to be marked as unresolvable. *)
-    let retrieved = undef sigma (List.rev (Evd.future_goals sigma)) in
+    let retrieved = Evd.filter_future_goals (Evd.is_undefined sigma) (Evd.save_future_goals sigma) in
+    let retrieved,retrieved_given_up = Evd.extract_given_up_future_goals retrieved in
+    (* Check that retrieved given up is empty *)
+    if not (List.is_empty retrieved_given_up) then
+      CErrors.anomaly Pp.(str "Evars generated outside of proof engine (e.g. V82, clear, ...) are not supposed to be explicitly given up.");
     let sigma = List.fold_left Proofview.Unsafe.mark_as_goal sigma retrieved in
     Proofview.Unsafe.tclEVARS sigma >>= fun () ->
     Proofview.tclUNIT retrieved
@@ -372,13 +381,31 @@ let in_proof p k = k (Proofview.return p.proofview)
 let unshelve p =
   { p with proofview = Proofview.unshelve (p.shelf) (p.proofview) ; shelf = [] }
 
+let pr_proof p =
+  let p = map_structured_proof p (fun _sigma g -> g) in
+  Pp.(
+    let pr_goal_list = prlist_with_sep spc Goal.pr_goal in
+    let rec aux acc = function
+      | [] -> acc
+      | (before,after)::stack ->
+         aux (pr_goal_list before ++ spc () ++ str "{" ++ acc ++ str "}" ++ spc () ++
+              pr_goal_list after) stack in
+    str "[" ++ str "focus structure: " ++
+               aux (pr_goal_list p.fg_goals) p.bg_goals ++ str ";" ++ spc () ++
+    str "shelved: " ++ pr_goal_list p.shelved_goals ++ str ";" ++ spc () ++
+    str "given up: " ++ pr_goal_list p.given_up_goals ++
+    str "]"
+  )
+
 (*** Compatibility layer with <=v8.2 ***)
 module V82 = struct
   let subgoals p =
-    Proofview.V82.goals p.proofview
+    let it, sigma = Proofview.proofview p.proofview in
+    Evd.{ it; sigma }
 
   let background_subgoals p =
-    Proofview.V82.goals (unroll_focus p.proofview p.focus_stack)
+    let it, sigma = Proofview.proofview (unroll_focus p.proofview p.focus_stack) in
+    Evd.{ it; sigma }
 
   let top_goal p =
     let { Evd.it=gls ; sigma=sigma; } =
@@ -404,15 +431,15 @@ module V82 = struct
         let evl = Evarutil.non_instantiated sigma in
         let evl = Evar.Map.bindings evl in
         if (n <= 0) then
-          CErrors.error "incorrect existential variable index"
+          CErrors.user_err Pp.(str "incorrect existential variable index")
         else if CList.length evl < n then
-          CErrors.error "not so many uninstantiated existential variables"
+          CErrors.user_err Pp.(str "not so many uninstantiated existential variables")
         else
           CList.nth evl (n-1)
       in
       let env = Evd.evar_filtered_env evi in
-      let rawc = Constrintern.intern_constr env com in
-      let ltac_vars = Pretyping.empty_lvar in
+      let rawc = Constrintern.intern_constr env sigma com in
+      let ltac_vars = Glob_ops.empty_lvar in
       let sigma = Evar_refiner.w_refine (evk, evi) (ltac_vars, rawc) sigma in
       Proofview.Unsafe.tclEVARS sigma
     end in
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 5053fc7f..c0e832fb 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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)         *)
 (************************************************************************)
 
 (* Module defining the last essential tiles of interactive proofs.
@@ -30,7 +32,9 @@
 *)
 
 (* Type of a proof. *)
-type proof
+type t
+type proof = t
+[@@ocaml.deprecated "please use [Proof.t]"]
 
 (* Returns a stylised view of a proof for use by, for instance,
    ide-s. *)
@@ -42,7 +46,7 @@ type proof
    shelf (the list of goals on the shelf), a representation of the
    given up goals (the list of the given up goals) and the underlying
    evar_map *)
-val proof : proof ->
+val proof : t ->
   Goal.goal list
   * (Goal.goal list * Goal.goal list) list
   * Goal.goal list
@@ -61,27 +65,26 @@ type 'a pre_goals = {
   (** List of the goals that have been given up *)
 }
 
-val map_structured_proof : proof -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre_goals)
+val map_structured_proof : t -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre_goals)
 
 
 (*** General proof functions ***)
-
-val start : Evd.evar_map -> (Environ.env * Term.types) list -> proof
-val dependent_start : Proofview.telescope -> proof
-val initial_goals : proof -> (Term.constr * Term.types) list
-val initial_euctx : proof -> Evd.evar_universe_context
+val start : Evd.evar_map -> (Environ.env * EConstr.types) list -> t
+val dependent_start : Proofview.telescope -> t
+val initial_goals : t -> (EConstr.constr * EConstr.types) list
+val initial_euctx : t -> UState.t
 
 (* Returns [true] if the considered proof is completed, that is if no goal remain
     to be considered (this does not require that all evars have been solved). *)
-val is_done : proof -> bool
+val is_done : t -> bool
 
 (* Like is_done, but this time it really means done (i.e. nothing left to do) *)
-val is_complete : proof -> bool
+val is_complete : t -> bool
 
 (* Returns the list of partial proofs to initial goals. *)
-val partial_proof : proof -> Term.constr list
+val partial_proof : t -> EConstr.constr list
 
-val compact : proof -> proof
+val compact : t -> t
 
 (* Returns the proofs (with their type) of the initial goals.
     Raises [UnfinishedProof] is some goals remain to be considered.
@@ -92,7 +95,7 @@ exception UnfinishedProof
 exception HasShelvedGoals
 exception HasGivenUpGoals
 exception HasUnresolvedEvar
-val return : proof -> Evd.evar_map
+val return : t -> Evd.evar_map
 
 (*** Focusing actions ***)
 
@@ -132,7 +135,7 @@ val done_cond : ?loose_end:bool -> 'a focus_kind -> 'a focus_condition
 (* focus command (focuses on the [i]th subgoal) *)
 (* spiwack: there could also, easily be a focus-on-a-range tactic, is there 
    a need for it? *)
-val focus : 'a focus_condition -> 'a -> int -> proof -> proof
+val focus : 'a focus_condition -> 'a -> int -> t -> t
 
 exception FullyUnfocused
 exception CannotUnfocusThisWay
@@ -148,56 +151,59 @@ exception NoSuchGoals of int * int
    Raises [FullyUnfocused] if the proof is not focused.
    Raises [CannotUnfocusThisWay] if the proof the unfocusing condition
      is not met. *)
-val unfocus : 'a focus_kind -> proof -> unit -> proof
+val unfocus : 'a focus_kind -> t -> unit -> t
 
 (* [unfocused p] returns [true] when [p] is fully unfocused. *)
-val unfocused : proof -> bool
+val unfocused : t -> bool
 
 (* [get_at_focus k] gets the information stored at the closest focus point
     of kind [k].
     Raises [NoSuchFocus] if there is no focus point of kind [k]. *)
 exception NoSuchFocus
-val get_at_focus : 'a focus_kind -> proof -> 'a
+val get_at_focus : 'a focus_kind -> t -> 'a
 
 (* [is_last_focus k] check if the most recent focus is of kind [k] *)
-val is_last_focus : 'a focus_kind -> proof -> bool
+val is_last_focus : 'a focus_kind -> t -> bool
 
 (* returns [true] if there is no goal under focus. *)
-val no_focused_goal : proof -> bool
+val no_focused_goal : t -> bool
 
 (*** Tactics ***)
 
 (* the returned boolean signal whether an unsafe tactic has been
    used. In which case it is [false]. *)
 val run_tactic : Environ.env ->
-  unit Proofview.tactic -> proof -> proof*(bool*Proofview_monad.Info.tree)
+  unit Proofview.tactic -> t -> t * (bool*Proofview_monad.Info.tree)
 
-val maximal_unfocus : 'a focus_kind -> proof -> proof
+val maximal_unfocus : 'a focus_kind -> t -> t
 
 (*** Commands ***)
 
-val in_proof : proof -> (Evd.evar_map -> 'a) -> 'a
+val in_proof : t -> (Evd.evar_map -> 'a) -> 'a
 
 (* Remove all the goals from the shelf and adds them at the end of the
    focused goals. *)
-val unshelve : proof -> proof
+val unshelve : t -> t
+
+val pr_proof : t -> Pp.t
 
 (*** Compatibility layer with <=v8.2 ***)
 module V82 : sig
-  val subgoals : proof -> Goal.goal list Evd.sigma
+  val subgoals : t -> Goal.goal list Evd.sigma
+  [@@ocaml.deprecated "Use the first and fifth argument of [Proof.proof]"]
 
   (* All the subgoals of the proof, including those which are not focused. *)
-  val background_subgoals : proof -> Goal.goal list Evd.sigma
+  val background_subgoals : t -> Goal.goal list Evd.sigma
 
-  val top_goal : proof -> Goal.goal Evd.sigma
+  val top_goal : t -> Goal.goal Evd.sigma
 
   (* returns the existential variable used to start the proof *)
-  val top_evars : proof -> Evd.evar list
+  val top_evars : t -> Evar.t list
 
   (* Turns the unresolved evars into goals.
      Raises [UnfinishedProof] if there are still unsolved goals. *)
-  val grab_evars : proof -> proof
+  val grab_evars : t -> t
 
   (* Implements the Existential command *)
-  val instantiate_evar : int -> Constrexpr.constr_expr -> proof -> proof
+  val instantiate_evar : int -> Constrexpr.constr_expr -> t -> t
 end
diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml
new file mode 100644
index 00000000..e22d382f
--- /dev/null
+++ b/proofs/proof_bullet.ml
@@ -0,0 +1,246 @@
+(************************************************************************)
+(*         *   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 Proof
+
+type t = Vernacexpr.bullet
+
+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
+| _ -> 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 '+'))
+
+
+type behavior = {
+  name : string;
+  put : Proof.t -> t -> Proof.t;
+  suggest: Proof.t -> Pp.t
+}
+
+let behaviors = Hashtbl.create 4
+let register_behavior b = Hashtbl.add behaviors b.name b
+
+(*** initial modes ***)
+let none = {
+  name = "None";
+  put = (fun x _ -> x);
+  suggest = (fun _ -> Pp.mt ())
+}
+let _ = register_behavior none
+
+module Strict = struct
+  type suggestion =
+  | Suggest of t (* this bullet is mandatory here *)
+  | Unfinished of t (* no mandatory bullet here, but this bullet is unfinished *)
+  | NoBulletInUse (* No mandatory bullet (or brace) here, no bullet pending,
+      	       some focused goals exists. *)
+  | NeedClosingBrace (* Some unfocussed goal exists "{" needed to focus them *)
+  | ProofFinished (* No more goal anywhere *)
+
+  (* give a message only if more informative than the standard coq message *)
+  let suggest_on_solved_goal sugg =
+    match sugg with
+    | NeedClosingBrace -> Pp.(str"Try unfocusing with \"}\".")
+    | NoBulletInUse -> Pp.mt ()
+    | ProofFinished -> Pp.mt ()
+    | Suggest b -> Pp.(str"Focus next goal with bullet " ++ pr_bullet b ++ str".")
+    | Unfinished b -> Pp.(str"The current bullet " ++ pr_bullet b ++ str" is unfinished.")
+
+  (* give always a message. *)
+  let suggest_on_error sugg =
+    match sugg with
+    | NeedClosingBrace -> Pp.(str"Try unfocusing with \"}\".")
+    | NoBulletInUse -> assert false (* This should never raise an error. *)
+    | ProofFinished -> Pp.(str"No more subgoals.")
+    | Suggest b -> Pp.(str"Expecting " ++ pr_bullet b ++ str".")
+    | Unfinished b -> Pp.(str"Current bullet " ++ pr_bullet b ++ str" is not finished.")
+
+  exception FailedBullet of t * suggestion
+
+  let _ =
+    CErrors.register_handler
+      (function
+      | FailedBullet (b,sugg) ->
+        let prefix = Pp.(str"Wrong bullet " ++ pr_bullet b ++ str": ") in
+        CErrors.user_err ~hdr:"Focus" Pp.(prefix ++ suggest_on_error sugg)
+      | _ -> raise CErrors.Unhandled)
+
+
+  (* spiwack: we need only one focus kind as we keep a stack of (distinct!) bullets *)
+  let bullet_kind = (new_focus_kind () : t list focus_kind)
+  let bullet_cond = done_cond ~loose_end:true bullet_kind
+
+  (* spiwack: as it is bullets are reset (locally) by *any* non-bullet focusing command
+     experience will tell if this is the right discipline of if we want to be finer and
+     reset them only for a choice of bullets. *)
+  let get_bullets pr =
+    if is_last_focus bullet_kind pr then
+      get_at_focus bullet_kind pr
+    else
+      []
+
+  let has_bullet bul pr =
+    let rec has_bullet = function
+      | b'::_ when bullet_eq bul b' -> true
+      | _::l -> has_bullet l
+      | [] -> false
+    in
+    has_bullet (get_bullets pr)
+
+  (* pop a bullet from proof [pr]. There should be at least one
+     bullet in use. If pop impossible (pending proofs on this level
+     of bullet or higher) then raise [Proof.CannotUnfocusThisWay]. *)
+  let pop pr =
+    match get_bullets pr with
+    | b::_ -> unfocus bullet_kind pr () , b
+    | _ -> assert false
+
+  let push (b:t) pr =
+    focus bullet_cond (b::get_bullets pr) 1 pr
+
+  let suggest_bullet (prf : Proof.t): suggestion =
+    if is_done prf then ProofFinished
+    else if not (no_focused_goal prf)
+    then (* No suggestion if a bullet is not mandatory, look for an unfinished bullet *)
+      match get_bullets prf with
+      | b::_ -> Unfinished b
+      | _ -> NoBulletInUse
+    else (* There is no goal under focus but some are unfocussed,
+            let us look at the bullet needed. *)
+      let rec loop prf =
+        match pop prf with
+        | prf, b ->
+          (* pop went well, this means that there are no more goals
+           *under this* bullet b, see if a new b can be pushed. *)
+          begin
+            try ignore (push b prf); Suggest b
+            with _ ->
+              (* b could not be pushed, so we must look for a outer bullet *)
+              loop prf
+          end
+        | exception _ ->
+          (* No pop was possible, but there are still
+             subgoals somewhere: there must be a "}" to use. *)
+          NeedClosingBrace
+      in
+      loop prf
+
+  let rec pop_until (prf : Proof.t) bul : Proof.t =
+    let prf', b = pop prf in
+    if bullet_eq bul b then prf'
+    else pop_until prf' bul
+
+  let put p bul =
+    try
+      if not (has_bullet bul p) then
+        (* bullet is not in use, so pushing it is always ok unless
+           no goal under focus. *)
+        push bul p
+      else
+        match suggest_bullet p with
+        | Suggest suggested_bullet when bullet_eq bul suggested_bullet
+            -> (* suggested_bullet is mandatory and you gave the right one *)
+          let p' = pop_until p bul in
+          push bul p'
+      (* the bullet you gave is in use but not the right one *)
+        | sugg -> raise (FailedBullet (bul,sugg))
+    with NoSuchGoals _ -> (* push went bad *)
+      raise (FailedBullet (bul,suggest_bullet p))
+
+  let strict = {
+    name = "Strict Subproofs";
+    put = put;
+    suggest = (fun prf -> suggest_on_solved_goal (suggest_bullet prf))
+
+  }
+  let _ = register_behavior strict
+end
+
+(* Current bullet behavior, controlled by the option *)
+let current_behavior = ref Strict.strict
+
+let _ =
+  Goptions.(declare_string_option {
+    optdepr = false;
+    optname = "bullet behavior";
+    optkey = ["Bullet";"Behavior"];
+    optread = begin fun () ->
+      (!current_behavior).name
+    end;
+    optwrite = begin fun n ->
+      current_behavior :=
+        try Hashtbl.find behaviors n
+        with Not_found ->
+          CErrors.user_err Pp.(str ("Unknown bullet behavior: \"" ^ n ^ "\"."))
+    end
+  })
+
+let put p b =
+  (!current_behavior).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
+                                 })
+
diff --git a/proofs/proof_bullet.mli b/proofs/proof_bullet.mli
new file mode 100644
index 00000000..ffbaa0fa
--- /dev/null
+++ b/proofs/proof_bullet.mli
@@ -0,0 +1,53 @@
+(************************************************************************)
+(*         *   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)         *)
+(************************************************************************)
+
+(**********************************************************)
+(*                                                        *)
+(*                                 Bullets                *)
+(*                                                        *)
+(**********************************************************)
+
+type t = Vernacexpr.bullet
+
+(** A [behavior] is the data of a put function which
+    is called when a bullet prefixes a tactic, a suggest function
+    suggesting the right bullet to use on a given proof, together
+    with a name to identify the behavior. *)
+type behavior = {
+  name : string;
+  put : Proof.t -> t -> Proof.t;
+  suggest: Proof.t -> Pp.t
+}
+
+(** A registered behavior can then be accessed in Coq
+    through the command [Set Bullet Behavior "name"].
+
+    Two modes are registered originally:
+    * "Strict Subproofs":
+      - If this bullet follows another one of its kind, defocuses then focuses
+        (which fails if the focused subproof is not complete).
+      - If it is the first bullet of its kind, then focuses a new subproof.
+    * "None": bullets don't do anything *)
+val register_behavior : behavior -> unit
+
+(** Handles focusing/defocusing with bullets:
+     *)
+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
+
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index e753e972..d6c0e334 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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)         *)
 (************************************************************************)
 
 (***********************************************************************)
@@ -18,6 +20,8 @@ open Util
 open Pp
 open Names
 
+module NamedDecl = Context.Named.Declaration
+
 (*** Proof Modes ***)
 
 (* Type of proof modes :
@@ -34,7 +38,7 @@ let proof_modes = Hashtbl.create 6
 let find_proof_mode n =
   try Hashtbl.find proof_modes n
   with Not_found ->
-    CErrors.error (Format.sprintf "No proof mode named \"%s\"." n)
+    CErrors.user_err Pp.(str (Format.sprintf "No proof mode named \"%s\"." n))
 
 let register_proof_mode ({name = n} as m) =
   Hashtbl.add proof_modes n (CEphemeron.create m)
@@ -50,8 +54,7 @@ let get_default_proof_mode_name () =
   (CEphemeron.default !default_proof_mode standard).name
 
 let _ =
-  Goptions.declare_string_option {Goptions.
-    optsync = true ;
+  Goptions.(declare_string_option {
     optdepr = false;
     optname = "default proof mode" ;
     optkey = ["Default";"Proof";"Mode"] ;
@@ -61,41 +64,42 @@ let _ =
     optwrite = begin fun n ->
       default_proof_mode := find_proof_mode n
     end
-  }
+  })
 
 (*** Proof Global Environment ***)
 
 (* Extra info on proofs. *)
 type lemma_possible_guards = int list list
-type proof_universes = Evd.evar_universe_context * Universes.universe_binders option
-type universe_binders = Id.t Loc.located list
 
 type proof_object = {
   id : Names.Id.t;
   entries : Safe_typing.private_constants Entries.definition_entry list;
   persistence : Decl_kinds.goal_kind;
-  universes: proof_universes;
+  universes: UState.t;
 }
 
 type proof_ending =
-  | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * proof_universes
+  | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t
   | Proved of Vernacexpr.opacity_flag *
-             (Vernacexpr.lident * Decl_kinds.theorem_kind option) option *
+              Misctypes.lident option *
               proof_object
 type proof_terminator = proof_ending -> unit
 type closed_proof = proof_object * proof_terminator
 
 type pstate = {
-  pid : Id.t;
+  pid : Id.t;  (* the name of the theorem whose proof is being constructed *)
   terminator : proof_terminator CEphemeron.key;
-  endline_tactic : Tacexpr.raw_tactic_expr option;
-  section_vars : Context.section_context option;
-  proof : Proof.proof;
+  endline_tactic : Genarg.glob_generic_argument option;
+  section_vars : Context.Named.t option;
+  proof : Proof.t;
   strength : Decl_kinds.goal_kind;
   mode : proof_mode CEphemeron.key;
-  universe_binders: universe_binders option;
+  universe_decl: Univdecls.universe_decl;
 }
 
+type t = pstate list
+type state = t
+
 let make_terminator f = f
 let apply_terminator f = f
 
@@ -123,13 +127,13 @@ let push a l = l := a::!l;
 
 exception NoSuchProof
 let _ = CErrors.register_handler begin function
-  | NoSuchProof -> CErrors.error "No such proof."
+  | NoSuchProof -> CErrors.user_err Pp.(str "No such proof.")
   | _ -> raise CErrors.Unhandled
 end
 
 exception NoCurrentProof
 let _ = CErrors.register_handler begin function
-  | NoCurrentProof -> CErrors.error "No focused proof (No proof-editing in progress)."
+  | NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof (No proof-editing in progress).")
   | _ -> raise CErrors.Unhandled
 end
 
@@ -144,11 +148,9 @@ let cur_pstate () =
   | [] -> raise NoCurrentProof
 
 let give_me_the_proof () = (cur_pstate ()).proof
+let give_me_the_proof_opt () = try Some (give_me_the_proof ()) with | NoCurrentProof -> None
 let get_current_proof_name () = (cur_pstate ()).pid
 
-let interp_tac = ref (fun _ -> assert false)
-let set_interp_tac f = interp_tac := f
-
 let with_current_proof f =
   match !pstates with
   | [] -> raise NoCurrentProof
@@ -156,11 +158,18 @@ let with_current_proof f =
       let et =
         match p.endline_tactic with
         | None -> Proofview.tclUNIT ()
-        | Some tac -> !interp_tac tac in
+        | Some tac ->
+          let open Geninterp in
+          let ist = { lfun = Id.Map.empty; extra = TacStore.empty } in
+          let Genarg.GenArg (Genarg.Glbwit tag, tac) = tac in
+          let tac = Geninterp.interp tag ist tac in
+          Ftactic.run tac (fun _ -> Proofview.tclUNIT ())
+      in
       let (newpr,ret) = f et p.proof in
       let p = { p with proof = newpr } in
       pstates := p :: rest;
       ret
+
 let simple_with_current_proof f = with_current_proof (fun t p -> f t p , ())
 
 let compact_the_proof () = simple_with_current_proof (fun _ -> Proof.compact)
@@ -182,7 +191,7 @@ let msg_proofs () =
   match get_all_proof_names () with
     | [] -> (spc () ++ str"(No proof-editing in progress).")
     | l ->  (str"." ++ fnl () ++ str"Proofs currently edited:" ++ spc () ++
-               (pr_sequence Nameops.pr_id l) ++ str".")
+               (pr_sequence Id.print l) ++ str".")
 
 let there_is_a_proof () = not (List.is_empty !pstates)
 let there_are_pending_proofs () = there_is_a_proof ()
@@ -190,20 +199,20 @@ let check_no_pending_proof () =
   if not (there_are_pending_proofs ()) then
     ()
   else begin
-    CErrors.error (Pp.string_of_ppcmds
+    CErrors.user_err
       (str"Proof editing in progress" ++ msg_proofs () ++ fnl() ++
-       str"Use \"Abort All\" first or complete proof(s)."))
+       str"Use \"Abort All\" first or complete proof(s).")
   end
 
 let discard_gen id =
   pstates := List.filter (fun { pid = id' } -> not (Id.equal id id')) !pstates
 
-let discard (loc,id) =
+let discard {CAst.loc;v=id} =
   let n = List.length !pstates in
   discard_gen id;
   if Int.equal (List.length !pstates) n then
-    CErrors.user_err_loc
-      (loc,"Pfedit.delete_proof",str"No such proof" ++ msg_proofs ())
+    CErrors.user_err ?loc
+      ~hdr:"Pfedit.delete_proof" (str"No such proof" ++ msg_proofs ())
 
 let discard_current () =
   if List.is_empty !pstates then raise NoCurrentProof else pstates := List.tl !pstates
@@ -226,15 +235,22 @@ let activate_proof_mode mode =
 let disactivate_current_proof_mode () =
   CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ())
 
-(** [start_proof sigma id str goals terminator] starts a proof of name
+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
     is (spiwack: for potential printing, I believe is used only by
     closing commands and the xml plugin); [terminator] is used at the
     end of the proof to close the proof. The proof is started in the
     evar map [sigma] (which can typically contain universe
-    constraints). *)
-let start_proof sigma id ?pl str goals terminator =
+    constraints), and with universe bindings pl. *)
+let start_proof sigma id ?(pl=default_universe_decl) str goals terminator =
   let initial_state = {
     pid = id;
     terminator = CEphemeron.create terminator;
@@ -243,10 +259,10 @@ let start_proof sigma id ?pl str goals terminator =
     section_vars = None;
     strength = str;
     mode = find_proof_mode "No";
-    universe_binders = pl } in
+    universe_decl = pl } in
   push initial_state pstates
 
-let start_dependent_proof id ?pl str goals terminator =
+let start_dependent_proof id ?(pl=default_universe_decl) str goals terminator =
   let initial_state = {
     pid = id;
     terminator = CEphemeron.create terminator;
@@ -255,16 +271,15 @@ let start_dependent_proof id ?pl str goals terminator =
     section_vars = None;
     strength = str;
     mode = find_proof_mode "No";
-    universe_binders = pl } in
+    universe_decl = pl } in
   push initial_state pstates
 
 let get_used_variables () = (cur_pstate ()).section_vars
-let get_universe_binders () = (cur_pstate ()).universe_binders
+let get_universe_decl () = (cur_pstate ()).universe_decl
 
 let proof_using_auto_clear = ref false
 let _ = Goptions.declare_bool_option
-    { Goptions.optsync  = true;
-      Goptions.optdepr  = false;
+    { Goptions.optdepr  = false;
       Goptions.optname  = "Proof using Clear Unused";
       Goptions.optkey   = ["Proof";"Using";"Clear";"Unused"];
       Goptions.optread  = (fun () -> !proof_using_auto_clear);
@@ -276,19 +291,19 @@ let set_used_variables l =
   let ids = List.fold_right Id.Set.add l Id.Set.empty in
   let ctx = Environ.keep_hyps env ids in
   let ctx_set =
-    List.fold_right Id.Set.add (List.map get_id ctx) Id.Set.empty in
+    List.fold_right Id.Set.add (List.map NamedDecl.get_id ctx) Id.Set.empty in
   let vars_of = Environ.global_vars_set in
   let aux env entry (ctx, all_safe, to_clear as orig) =
     match entry with
     | LocalAssum (x,_) ->
        if Id.Set.mem x all_safe then orig
-       else (ctx, all_safe, (Loc.ghost,x)::to_clear) 
+       else (ctx, all_safe, (CAst.make x)::to_clear)
     | LocalDef (x,bo, ty) as decl ->
        if Id.Set.mem x all_safe then orig else
        let vars = Id.Set.union (vars_of env bo) (vars_of env ty) in
        if Id.Set.subset vars all_safe
        then (decl :: ctx, Id.Set.add x all_safe, to_clear)
-       else (ctx, all_safe, (Loc.ghost,x) :: to_clear) in
+       else (ctx, all_safe, (CAst.make x) :: to_clear) in
   let ctx, _, to_clear =
     Environ.fold_named_context aux env ~init:(ctx,ctx_set,[]) in
   let to_clear = if !proof_using_auto_clear then to_clear else [] in
@@ -296,7 +311,7 @@ let set_used_variables l =
   | [] -> raise NoCurrentProof
   | p :: rest ->
       if not (Option.is_empty p.section_vars) then
-        CErrors.error "Used section variables can be declared only once";
+        CErrors.user_err Pp.(str "Used section variables can be declared only once");
       pstates := { p with section_vars = Some ctx} :: rest;
       ctx, to_clear
 
@@ -307,17 +322,18 @@ let get_open_goals () =
     (List.map (fun (l1,l2) -> List.length l1 + List.length l2) gll) +
     List.length shelf
 
-let constrain_variables init uctx =
-  let levels = Univ.Instance.levels (Univ.UContext.instance init) in
-  let cstrs = UState.constrain_variables levels uctx in
-  Univ.ContextSet.add_constraints cstrs (UState.context_set uctx)
+type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * UState.t
 
-let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
-  let { pid; section_vars; strength; proof; terminator; universe_binders } =
+let close_proof ~keep_body_ucst_separate ?feedback_id ~now
+                (fpl : closed_proof_output Future.computation) =
+  let { pid; section_vars; strength; proof; terminator; universe_decl } =
     cur_pstate () in
   let poly = pi2 strength (* Polymorphic *) in
   let initial_goals = Proof.initial_goals proof in
   let initial_euctx = Proof.initial_euctx proof in
+  let constrain_variables ctx =
+    UState.constrain_variables (fst (UState.context_set initial_euctx)) ctx
+  in
   let fpl, univs = Future.split2 fpl in
   let universes = if poly || now then Future.force univs else initial_euctx in
   (* Because of dependent subgoals at the beginning of proofs, we could
@@ -326,72 +342,73 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
   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
-    (Evd.evar_universe_context_subst universes) in
+    (UState.subst universes) in
   let make_body =
     if poly || now then
       let make_body t (c, eff) =
-        let open Universes in
         let body = c in
-	let typ =
-	  if not (keep_body_ucst_separate || not (Safe_typing.empty_private_constants = eff)) then
-	    nf t
-	  else t
-	in
-        let used_univs_body = Universes.universes_of_constr body in
-        let used_univs_typ = Universes.universes_of_constr typ in
-        if keep_body_ucst_separate ||
-           not (Safe_typing.empty_private_constants = eff) then
-          let initunivs = Evd.evar_context_universe_context initial_euctx in
-          let ctx = constrain_variables initunivs universes in
+        let allow_deferred =
+          not poly && (keep_body_ucst_separate ||
+          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
+        if allow_deferred then
+          let initunivs = UState.const_univ_entry ~poly initial_euctx in
+          let ctx = constrain_variables universes in
           (* For vi2vo compilation proofs are computed now but we need to
-           * complement the univ constraints of the typ with the ones of
-           * the body.  So we keep the two sets distinct. *)
-	  let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
-          let ctx_body = restrict_universe_context ctx used_univs in
-          (initunivs, typ), ((body, ctx_body), eff)
+             complement the univ constraints of the typ with the ones of
+             the body.  So we keep the two sets distinct. *)
+          let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
+          let ctx_body = UState.restrict ctx used_univs in
+          let univs = UState.check_mono_univ_decl ctx_body universe_decl in
+          (initunivs, typ), ((body, univs), eff)
         else
-          let initunivs = Univ.UContext.empty in
-          let ctx = constrain_variables initunivs universes in
           (* Since the proof is computed now, we can simply have 1 set of
-           * constraints in which we merge the ones for the body and the ones
-           * for the typ *)
+             constraints in which we merge the ones for the body and the ones
+             for the typ. We recheck the declaration after restricting with
+             the actually used universes.
+             TODO: check if restrict is really necessary now. *)
           let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
-          let ctx = restrict_universe_context ctx used_univs in
-          let univs = Univ.ContextSet.to_context ctx in
+          let ctx = UState.restrict universes used_univs in
+          let univs = UState.check_univ_decl ~poly ctx universe_decl in
           (univs, typ), ((body, Univ.ContextSet.empty), eff)
       in 
-       fun t p -> Future.split2 (Future.chain ~pure:true p (make_body t))
+       fun t p -> Future.split2 (Future.chain p (make_body t))
     else
       fun t p ->
-        let initunivs = Evd.evar_context_universe_context initial_euctx in
-        Future.from_val (initunivs, nf t),
-        Future.chain ~pure:true p (fun (pt,eff) ->
-          (pt,constrain_variables initunivs (Future.force univs)),eff)
+        (* Already checked the univ_decl for the type universes when starting the proof. *)
+        let univctx = Entries.Monomorphic_const_entry (UState.context_set universes) in
+        Future.from_val (univctx, nf t),
+        Future.chain p (fun (pt,eff) ->
+          (* Deferred proof, we already checked the universe declaration with
+             the initial universes, ensure that the final universes respect
+             the declaration as well. If the declaration is non-extensible,
+             this will prevent the body from adding universes and constraints. *)
+          let bodyunivs = constrain_variables (Future.force univs) in
+          let univs = UState.check_mono_univ_decl bodyunivs universe_decl in
+          (pt,univs),eff)
   in
-  let entries =
-    Future.map2 (fun p (_, t) ->
-      let univstyp, body = make_body t p in
-      let univs, typ = Future.force univstyp in
-	{ Entries.
-	  const_entry_body = body;
-	  const_entry_secctx = section_vars;
-	  const_entry_feedback = feedback_id;
-	  const_entry_type  = Some typ;
-	  const_entry_inline_code = false;
-	  const_entry_opaque = true;
-	  const_entry_universes = univs;
-	  const_entry_polymorphic = poly})
-		fpl initial_goals in
-  let binders =
-    Option.map (fun names -> fst (Evd.universe_context ~names (Evd.from_ctx universes)))
-	       universe_binders
+  let entry_fn p (_, t) =
+    let t = EConstr.Unsafe.to_constr t in
+    let univstyp, body = make_body t p in
+    let univs, typ = Future.force univstyp in
+    {Entries.
+      const_entry_body = body;
+      const_entry_secctx = section_vars;
+      const_entry_feedback = feedback_id;
+      const_entry_type  = Some typ;
+      const_entry_inline_code = false;
+      const_entry_opaque = true;
+      const_entry_universes = univs; }
   in
+  let entries = Future.map2 entry_fn fpl initial_goals in
   { id = pid; entries = entries; persistence = strength;
-    universes = (universes, binders) },
+    universes },
   fun pr_ending -> CEphemeron.get terminator pr_ending
 
-type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context
-
 let return_proof ?(allow_partial=false) () =
  let { pid; proof; strength = (_,poly,_) } = cur_pstate () in
  if allow_partial then begin
@@ -401,14 +418,14 @@ 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 -> c, eff) proofs in
+  let proofs = List.map (fun c -> EConstr.Unsafe.to_constr c, eff) proofs in
     proofs, Evd.evar_universe_context evd
  end else
   let initial_goals = Proof.initial_goals proof in
   let evd =
     let error s =
       let prf = str " (in proof " ++ Id.print pid ++ str ")" in
-      raise (CErrors.UserError("last tactic before Qed",s ++ prf))
+      raise (CErrors.UserError(Some "last tactic before Qed",s ++ prf))
     in
     try Proof.return proof with
     | Proof.UnfinishedProof ->
@@ -420,12 +437,12 @@ let return_proof ?(allow_partial=false) () =
     | Proof.HasUnresolvedEvar->
         error(strbrk"Attempt to save a proof with existential variables still non-instantiated") in
   let eff = Evd.eval_side_effects evd in
-  let evd = Evd.nf_constraints evd in
+  let evd = Evd.minimize_universes evd in
   (** 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 c, eff)) initial_goals in
+    List.map (fun (c, _) -> (Evarutil.nf_evars_universes evd (EConstr.Unsafe.to_constr c), eff)) initial_goals in
     proofs, Evd.evar_universe_context evd
 
 let close_future_proof ~feedback_id proof =
@@ -442,263 +459,6 @@ let set_terminator hook =
   | [] -> raise NoCurrentProof
   | p :: ps -> pstates := { p with terminator = CEphemeron.create hook } :: ps
 
-
-
-
-(**********************************************************)
-(*                                                        *)
-(*                                 Bullets                *)
-(*                                                        *)
-(**********************************************************)
-
-module Bullet = struct
-
-  type t = Vernacexpr.bullet
-
-  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
-  | _ -> false
-
-  let pr_bullet b =
-    match b with
-    | Vernacexpr.Dash n -> str (String.make n '-')
-    | Vernacexpr.Star n -> str (String.make n '*')
-    | Vernacexpr.Plus n -> str (String.make n '+')
-
-
-  type behavior = {
-    name : string;
-    put : Proof.proof -> t -> Proof.proof;
-    suggest: Proof.proof -> std_ppcmds
-  }
-
-  let behaviors = Hashtbl.create 4
-  let register_behavior b = Hashtbl.add behaviors b.name b
-
-  (*** initial modes ***)
-  let none = {
-    name = "None";
-    put = (fun x _ -> x);
-    suggest = (fun _ -> mt ())
-  }
-  let _ = register_behavior none
-
-  module Strict = struct
-    type suggestion =
-    | Suggest of t (* this bullet is mandatory here *)
-    | Unfinished of t (* no mandatory bullet here, but this bullet is unfinished *)
-    | NoBulletInUse (* No mandatory bullet (or brace) here, no bullet pending,
-		       some focused goals exists. *)
-    | NeedClosingBrace (* Some unfocussed goal exists "{" needed to focus them *)
-    | ProofFinished (* No more goal anywhere *)
-
-    (* give a message only if more informative than the standard coq message *)
-    let suggest_on_solved_goal sugg =
-      match sugg with
-      | NeedClosingBrace -> str"Try unfocusing with \"}\"."
-      | NoBulletInUse -> mt ()
-      | ProofFinished -> mt ()
-      | Suggest b -> str"Focus next goal with bullet " ++ pr_bullet b ++ str"."
-      | Unfinished b -> str"The current bullet " ++ pr_bullet b ++ str" is unfinished."
-
-    (* give always a message. *)
-    let suggest_on_error sugg =
-      match sugg with
-      | NeedClosingBrace -> str"Try unfocusing with \"}\"."
-      | NoBulletInUse -> assert false (* This should never raise an error. *)
-      | ProofFinished -> str"No more subgoals."
-      | Suggest b -> str"Bullet " ++ pr_bullet b ++ str" is mandatory here."
-      | Unfinished b -> str"Current bullet " ++ pr_bullet b ++ str" is not finished."
-
-    exception FailedBullet of t * suggestion
-
-    let _ =
-      CErrors.register_handler
-	(function
-	| FailedBullet (b,sugg) ->
-	  let prefix = str"Wrong bullet " ++ pr_bullet b ++ str" : " in
-	  CErrors.errorlabstrm "Focus" (prefix ++ suggest_on_error sugg)
-	| _ -> raise CErrors.Unhandled)
-
-
-    (* spiwack: we need only one focus kind as we keep a stack of (distinct!) bullets *)
-    let bullet_kind = (Proof.new_focus_kind () : t list Proof.focus_kind)
-    let bullet_cond = Proof.done_cond ~loose_end:true bullet_kind
-
-    (* spiwack: as it is bullets are reset (locally) by *any* non-bullet focusing command
-       experience will tell if this is the right discipline of if we want to be finer and
-       reset them only for a choice of bullets. *)
-    let get_bullets pr =
-      if Proof.is_last_focus bullet_kind pr then
-	Proof.get_at_focus bullet_kind pr
-      else
-	[]
-
-    let has_bullet bul pr =
-      let rec has_bullet = function
-	| b'::_ when bullet_eq bul b' -> true
-	| _::l -> has_bullet l
-	| [] -> false
-      in
-      has_bullet (get_bullets pr)
-
-    (* pop a bullet from proof [pr]. There should be at least one
-       bullet in use. If pop impossible (pending proofs on this level
-       of bullet or higher) then raise [Proof.CannotUnfocusThisWay]. *)
-    let pop pr =
-      match get_bullets pr with
-      | b::_ -> Proof.unfocus bullet_kind pr () , b
-      | _ -> assert false
-
-    let push (b:t) pr =
-      Proof.focus bullet_cond (b::get_bullets pr) 1 pr
-
-    (* Used only in the next function.
-       TODO: use a recursive function instead? *)
-    exception SuggestFound of t
-
-    let suggest_bullet (prf:Proof.proof): suggestion =
-      if Proof.is_done prf then ProofFinished
-      else if not (Proof.no_focused_goal prf)
-      then (* No suggestion if a bullet is not mandatory, look for an unfinished bullet *)
-	match get_bullets prf with
-	| b::_ -> Unfinished b
-	| _ -> NoBulletInUse
-      else (* There is no goal under focus but some are unfocussed,
-	      let us look at the bullet needed. If no  *)
-	let pcobaye = ref prf in
-	try
-	  while true do
-	    let pcobaye', b = pop !pcobaye in
-	   (* pop went well, this means that there are no more goals
-	    *under this* bullet b, see if a new b can be pushed. *)
-	    (try let _ = push b pcobaye' in (* push didn't fail so a new b can be pushed. *)
-		 raise (SuggestFound b)
-	     with SuggestFound _ as e -> raise e
-	     | _ -> ()); (* b could not be pushed, so we must look for a outer bullet *)
-	    pcobaye := pcobaye'
-	  done;
-	  assert false
-	with SuggestFound b -> Suggest b
-	| _ -> NeedClosingBrace (* No push was possible, but there are still
-				   subgoals somewhere: there must be a "}" to use. *)
-
-
-    let rec pop_until (prf:Proof.proof) bul: Proof.proof =
-      let prf', b = pop prf in
-      if bullet_eq bul b then prf'
-      else pop_until prf' bul
-
-    let put p bul =
-      try
-	if not (has_bullet bul p) then
-	  (* bullet is not in use, so pushing it is always ok unless
-	     no goal under focus. *)
-	  push bul p
-	else
-	  match suggest_bullet p with
-	  | Suggest suggested_bullet when bullet_eq bul suggested_bullet
-	      -> (* suggested_bullet is mandatory and you gave the right one *)
-	    let p' = pop_until p bul in
-	    push bul p'
-	(* the bullet you gave is in use but not the right one *)
-	  | sugg -> raise (FailedBullet (bul,sugg))
-      with Proof.NoSuchGoals _ -> (* push went bad *)
-	raise (FailedBullet (bul,suggest_bullet p))
-
-    let strict = {
-      name = "Strict Subproofs";
-      put = put;
-      suggest = (fun prf -> suggest_on_solved_goal (suggest_bullet prf))
-
-    }
-    let _ = register_behavior strict
-  end
-
-  (* Current bullet behavior, controlled by the option *)
-  let current_behavior = ref Strict.strict
-
-  let _ =
-    Goptions.declare_string_option {Goptions.
-      optsync = true;
-      optdepr = false;
-      optname = "bullet behavior";
-      optkey = ["Bullet";"Behavior"];
-      optread = begin fun () ->
-	(!current_behavior).name
-      end;
-      optwrite = begin fun n ->
-	current_behavior :=
-          try Hashtbl.find behaviors n
-          with Not_found ->
-            CErrors.error ("Unknown bullet behavior: \"" ^ n ^ "\".")
-      end
-    }
-
-  let put p b =
-    (!current_behavior).put p b
-
-  let suggest p =
-    (!current_behavior).suggest p
-end
-
-
-let _ =
-  let hook n =
-    let prf = give_me_the_proof () in
-    (Bullet.suggest prf) in
-  Proofview.set_nosuchgoals_hook hook
-
-
-(**********************************************************)
-(*                                                        *)
-(*                     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 print_range_selector (i, j) =
-  if i = j then string_of_int i
-  else string_of_int i ^ "-" ^ string_of_int j
-
-let print_goal_selector = function
-  | Vernacexpr.SelectAll -> "all"
-  | Vernacexpr.SelectNth i -> string_of_int i
-  | Vernacexpr.SelectList l -> "[" ^
-      String.concat ", " (List.map print_range_selector l) ^ "]"
-  | Vernacexpr.SelectId id -> Id.to_string 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.error err_msg;
-              Vernacexpr.SelectNth i
-        with Failure _ -> CErrors.error err_msg
-      end
-
-let _ =
-  Goptions.declare_string_option {Goptions.
-                                  optsync = true ;
-                                  optdepr = false;
-                                  optname = "default goal selector" ;
-                                  optkey = ["Default";"Goal";"Selector"] ;
-                                  optread = begin fun () -> print_goal_selector !default_goal_selector end;
-                                  optwrite = begin fun n ->
-                                    default_goal_selector := parse_goal_selector n
-                                  end
-                                 }
-
-
 module V82 = struct
   let get_current_initial_conclusions () =
   let { pid; strength; proof } = cur_pstate () in
@@ -707,12 +467,10 @@ module V82 = struct
     pid, (goals, strength)
 end
 
-type state = pstate list
-        
 let freeze ~marshallable =
   match marshallable with
   | `Yes ->
-      CErrors.anomaly (Pp.str"full marshalling of proof state not supported")
+      CErrors.anomaly (Pp.str"full marshalling of proof state not supported.")
   | `Shallow -> !pstates
   | `No -> !pstates
 let unfreeze s = pstates := s; update_proof_mode ()
@@ -727,3 +485,14 @@ let update_global_env () =
        let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in
        let (p,(status,info)) = Proof.run_tactic (Global.env ()) tac p in
          (p, ())))
+
+(* XXX: Bullet hook, should be really moved elsewhere *)
+let _ =
+  let hook n =
+    try
+      let prf = give_me_the_proof () in
+      (Proof_bullet.suggest prf)
+    with NoCurrentProof -> mt ()
+  in
+  Proofview.set_nosuchgoals_hook hook
+
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 59daa296..bf35fd65 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -1,34 +1,20 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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)         *)
 (************************************************************************)
 
 (** This module defines proof facilities relevant to the
      toplevel. In particular it defines the global proof
      environment. *)
 
-(** Type of proof modes :
-    - A name
-    - A function [set] to set it *from standard mode*
-    - A function [reset] to reset the *standard mode* from it 
-
-*)
-type proof_mode_name = string
-type proof_mode = {
-  name : proof_mode_name ;
-  set : unit -> unit ;
-  reset : unit -> unit
-}
-
-(** Registers a new proof mode which can then be adressed by name
-    in [set_default_proof_mode].
-    One mode is already registered - the standard mode - named "No",
-    It corresponds to Coq default setting are they are set when coqtop starts. *)
-val register_proof_mode : proof_mode -> unit
-val get_default_proof_mode_name : unit -> proof_mode_name
+type t
+type state = t
+[@@ocaml.deprecated "please use [Proof_global.t]"]
 
 val there_are_pending_proofs : unit -> bool
 val check_no_pending_proof : unit -> unit
@@ -36,16 +22,13 @@ 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 : Names.Id.t Loc.located -> unit
+val discard : Misctypes.lident -> unit
 val discard_current : unit -> unit
 val discard_all : unit -> unit
 
-(** [set_proof_mode] sets the proof mode to be used after it's called. It is
-    typically called by the Proof Mode command. *)
-val set_proof_mode : proof_mode_name -> unit
-
+val give_me_the_proof_opt : unit -> Proof.t option
 exception NoCurrentProof
-val give_me_the_proof : unit -> Proof.proof
+val give_me_the_proof : unit -> Proof.t
 (** @raise NoCurrentProof when outside proof mode. *)
 
 val compact_the_proof : unit -> unit
@@ -57,20 +40,19 @@ val compact_the_proof : unit -> unit
     (i.e. an proof ending command) and registers the appropriate
     values. *)
 type lemma_possible_guards = int list list
-type proof_universes = Evd.evar_universe_context * Universes.universe_binders option
-type universe_binders = Names.Id.t Loc.located list
+
 type proof_object = {
   id : Names.Id.t;
   entries : Safe_typing.private_constants Entries.definition_entry list;
   persistence : Decl_kinds.goal_kind;
-  universes: proof_universes;
+  universes: UState.t;
 }
 
 type proof_ending =
   | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry *
-		  proof_universes
+                UState.t
   | Proved of Vernacexpr.opacity_flag *
-             (Vernacexpr.lident * Decl_kinds.theorem_kind option) option *
+              Misctypes.lident option *
               proof_object
 type proof_terminator
 type closed_proof = proof_object * proof_terminator
@@ -78,21 +60,23 @@ type closed_proof = proof_object * proof_terminator
 val make_terminator : (proof_ending -> unit) -> proof_terminator
 val apply_terminator : proof_terminator -> proof_ending -> unit
 
-(** [start_proof id str goals terminator] starts a proof of name [id]
+(** [start_proof id str pl 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
     is (spiwack: for potential printing, I believe is used only by
     closing commands and the xml plugin); [terminator] is used at the
-    end of the proof to close the proof. *)
+    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. *)
 val start_proof :
-  Evd.evar_map -> Names.Id.t -> ?pl:universe_binders ->
-  Decl_kinds.goal_kind -> (Environ.env * Term.types) list  ->
+  Evd.evar_map -> Names.Id.t -> ?pl:Univdecls.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:universe_binders -> Decl_kinds.goal_kind ->
+  Names.Id.t -> ?pl:Univdecls.universe_decl -> Decl_kinds.goal_kind ->
   Proofview.telescope -> proof_terminator -> unit
 
 (** Update the proofs global environment after a side-effecting command
@@ -108,7 +92,7 @@ val close_proof : keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof
  * Both access the current proof state. The former is supposed to be
  * chained with a computation that completed the proof *)
 
-type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context
+type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * UState.t
 
 (* If allow_partial is set (default no) then an incomplete proof
  * is allowed (no error), and a warn is given if the proof is complete. *)
@@ -129,87 +113,72 @@ val get_open_goals : unit -> int
     no current proof.
     The return boolean is set to [false] if an unsafe tactic has been used. *)
 val with_current_proof :
-  (unit Proofview.tactic -> Proof.proof -> Proof.proof*'a) -> 'a
+  (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> 'a
 val simple_with_current_proof :
-  (unit Proofview.tactic -> Proof.proof -> Proof.proof) -> unit
+  (unit Proofview.tactic -> Proof.t -> Proof.t) -> unit
 
 (** Sets the tactic to be used when a tactic line is closed with [...] *)
-val set_endline_tactic : Tacexpr.raw_tactic_expr -> unit
-val set_interp_tac :
-  (Tacexpr.raw_tactic_expr -> unit Proofview.tactic)
-    -> unit
+val set_endline_tactic : Genarg.glob_generic_argument -> unit
 
 (** Sets the section variables assumed by the proof, returns its closure
  * (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.section_context * (Loc.t * Names.Id.t) list
-val get_used_variables : unit -> Context.section_context option
+  Names.Id.t list -> Context.Named.t * Misctypes.lident list
+val get_used_variables : unit -> Context.Named.t option
 
-val get_universe_binders : unit -> universe_binders option
+(** Get the universe declaration associated to the current proof. *)
+val get_universe_decl : unit -> Univdecls.universe_decl
 
-(**********************************************************)
-(*                                                        *)
-(*                            Proof modes                 *)
-(*                                                        *)
-(**********************************************************)
+module V82 : sig
+  val get_current_initial_conclusions : unit -> Names.Id.t *(EConstr.types list *
+  Decl_kinds.goal_kind)
+end
 
+val freeze : marshallable:[`Yes | `No | `Shallow] -> t
+val unfreeze : t -> unit
+val proof_of_state : t -> Proof.t
+val copy_terminators : src:t -> tgt:t -> t
 
-val activate_proof_mode : proof_mode_name -> unit
-val disactivate_current_proof_mode : unit -> unit
 
 (**********************************************************)
-(*                                                        *)
-(*                                 Bullets                *)
-(*                                                        *)
+(* Proof Mode API                                         *)
+(* The current Proof Mode API is deprecated and a new one *)
+(* will be (hopefully) defined in 8.8                     *)
 (**********************************************************)
 
-module Bullet : sig
-  type t = Vernacexpr.bullet
-
-  (** A [behavior] is the data of a put function which
-      is called when a bullet prefixes a tactic, a suggest function
-      suggesting the right bullet to use on a given proof, together
-      with a name to identify the behavior. *)
-  type behavior = {
-    name : string;
-    put : Proof.proof -> t -> Proof.proof;
-    suggest: Proof.proof -> Pp.std_ppcmds
-  }
-
-  (** A registered behavior can then be accessed in Coq
-      through the command [Set Bullet Behavior "name"].
-
-      Two modes are registered originally:
-      * "Strict Subproofs":
-        - If this bullet follows another one of its kind, defocuses then focuses
-          (which fails if the focused subproof is not complete).
-        - If it is the first bullet of its kind, then focuses a new subproof.
-      * "None": bullets don't do anything *)
-  val register_behavior : behavior -> unit
-
-  (** Handles focusing/defocusing with bullets:
-       *)
-  val put : Proof.proof -> t -> Proof.proof
-  val suggest : Proof.proof -> Pp.std_ppcmds
-end
+(** Type of proof modes :
+    - A name
+    - A function [set] to set it *from standard mode*
+    - A function [reset] to reset the *standard mode* from it 
 
+*)
+type proof_mode_name = string
+type proof_mode = {
+  name : proof_mode_name ;
+  set : unit -> unit ;
+  reset : unit -> unit
+}
 
-(**********************************************************)
-(*                                                        *)
-(*                     Default goal selector              *)
-(*                                                        *)
-(**********************************************************)
+(** Registers a new proof mode which can then be adressed by name
+    in [set_default_proof_mode].
+    One mode is already registered - the standard mode - named "No",
+    It corresponds to Coq default setting are they are set when coqtop starts. *)
+val register_proof_mode : proof_mode -> unit
+(* Can't make this deprecated due to limitations of camlp5 *)
+(* [@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "] *)
 
-val get_default_goal_selector : unit -> Vernacexpr.goal_selector
+val get_default_proof_mode_name : unit -> proof_mode_name
+[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "]
 
-module V82 : sig
-  val get_current_initial_conclusions : unit -> Names.Id.t *(Term.types list *
-  Decl_kinds.goal_kind)
-end
+(** [set_proof_mode] sets the proof mode to be used after it's called. It is
+    typically called by the Proof Mode command. *)
+val set_proof_mode : proof_mode_name -> unit
+[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "]
+
+val activate_proof_mode : proof_mode_name -> unit
+[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "]
+
+val disactivate_current_proof_mode : unit -> unit
+[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "]
 
-type state
-val freeze : marshallable:[`Yes | `No | `Shallow] -> state
-val unfreeze : state -> unit
-val proof_of_state : state -> Proof.proof
-val copy_terminators : src:state -> tgt:state -> state
diff --git a/proofs/proof_type.mli b/proofs/proof_type.ml
index c1207962..149f30c6 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.ml
@@ -1,26 +1,22 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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)         *)
 (************************************************************************)
 
 (** Legacy proof engine. Do not use in newly written code. *)
 
 open Evd
-open Names
-open Term
-open Tacexpr
-open Glob_term
-open Nametab
-open Misctypes
+open Constr
 
 (** This module defines the structure of proof tree and the tactic type. So, it
    is used by [Proof_tree] and [Refiner] *)
 
 type prim_rule =
-  | Cut of bool * bool * Id.t * types
   | Refine of constr
 
 (** Nowadays, the only rules we'll consider are the primitive rules *)
diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml
deleted file mode 100644
index caa9b328..00000000
--- a/proofs/proof_using.ml
+++ /dev/null
@@ -1,166 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Names
-open Environ
-open Util
-open Vernacexpr
-open Context.Named.Declaration
-
-let to_string e =
-  let rec aux = function
-    | SsEmpty -> "()"
-    | SsSingl (_,id) -> "("^Id.to_string id^")"
-    | SsCompl e -> "-" ^ aux e^""
-    | SsUnion(e1,e2) -> "("^aux e1 ^" + "^ aux e2^")"
-    | SsSubstr(e1,e2) -> "("^aux e1 ^" - "^ aux e2^")"
-    | SsFwdClose e -> "("^aux e^")*"
-  in aux e
-
-let known_names = Summary.ref [] ~name:"proofusing-nameset"
-
-let in_nameset =
-  let open Libobject in
-  declare_object { (default_object "proofusing-nameset") with
-    cache_function = (fun (_,x) -> known_names := x :: !known_names);
-    classify_function = (fun _ -> Dispose);
-    discharge_function = (fun _ -> None)
-  }
-
-let rec close_fwd e s =
-  let s' =
-    List.fold_left (fun s decl ->
-      let (id,b,ty) = Context.Named.Declaration.to_tuple decl in
-      let vb = Option.(default Id.Set.empty (map (global_vars_set e) b)) in
-      let vty = global_vars_set e ty in
-      let vbty = Id.Set.union vb vty in
-      if Id.Set.exists (fun v -> Id.Set.mem v s) vbty
-      then Id.Set.add id (Id.Set.union s vbty) else s)
-    s (named_context e)
-    in
-  if Id.Set.equal s s' then s else close_fwd e s'
-;;
-
-let rec process_expr env e ty =
-  let rec aux = function
-    | SsEmpty -> Id.Set.empty
-    | SsSingl (_,id) -> set_of_id env ty id
-    | SsUnion(e1,e2) -> Id.Set.union (aux e1) (aux e2)
-    | SsSubstr(e1,e2) -> Id.Set.diff (aux e1) (aux e2)
-    | SsCompl e -> Id.Set.diff (full_set env) (aux e)
-    | SsFwdClose e -> close_fwd env (aux e)
-  in
-    aux e
-
-and set_of_id env ty id =
-  if Id.to_string id = "Type" then
-    List.fold_left (fun acc ty ->
-        Id.Set.union (global_vars_set env ty) acc)
-      Id.Set.empty ty
-  else if Id.to_string id = "All" then
-    List.fold_right Id.Set.add (List.map get_id (named_context env)) Id.Set.empty
-  else if CList.mem_assoc_f Id.equal id !known_names then
-    process_expr env (CList.assoc_f Id.equal id !known_names) []
-  else Id.Set.singleton id
-
-and full_set env =
-  List.fold_right Id.Set.add (List.map get_id (named_context env)) Id.Set.empty
-
-let process_expr env e ty =
-  let ty_expr = SsSingl(Loc.ghost, Id.of_string "Type") in
-  let v_ty = process_expr env ty_expr ty in
-  let s = Id.Set.union v_ty (process_expr env e ty) in
-  Id.Set.elements s
-
-let name_set id expr = Lib.add_anonymous_leaf (in_nameset (id,expr))
-
-let minimize_hyps env ids =
-  let rec aux ids =
-    let ids' =
-      Id.Set.fold (fun id alive ->
-        let impl_by_id =
-          Id.Set.remove id (really_needed env (Id.Set.singleton id)) in
-        if Id.Set.is_empty impl_by_id then alive
-        else Id.Set.diff alive impl_by_id)
-      ids ids in
-    if Id.Set.equal ids ids' then ids else aux ids'
-  in
-    aux ids
-
-let remove_ids_and_lets env s ids =
-  let not_ids id = not (Id.Set.mem id ids) in
-  let no_body id = named_body id env = None in
-  let deps id = really_needed env (Id.Set.singleton id) in
-    (Id.Set.filter (fun id ->
-      not_ids id &&
-     (no_body id ||
-       Id.Set.exists not_ids (Id.Set.filter no_body (deps id)))) s)
-
-let suggest_Proof_using name env vars ids_typ context_ids =
-  let module S = Id.Set in
-  let open Pp in
-  let print x = prerr_endline (string_of_ppcmds x) in
-  let pr_set parens s =
-    let wrap ppcmds =
-      if parens && S.cardinal s > 1 then str "(" ++ ppcmds ++ str ")"
-      else ppcmds in
-    wrap (prlist_with_sep (fun _ -> str" ") Id.print (S.elements s)) in
-  let used = S.union vars ids_typ in
-  let needed = minimize_hyps env (remove_ids_and_lets env used ids_typ) in
-  let all_needed = really_needed env needed in
-  let all = List.fold_right S.add context_ids S.empty in
-  let fwd_typ = close_fwd env ids_typ in
-  if !Flags.debug then begin
-    print (str "All "        ++ pr_set false all);
-    print (str "Type "       ++ pr_set false ids_typ);
-    print (str "needed "     ++ pr_set false needed);
-    print (str "all_needed " ++ pr_set false all_needed);
-    print (str "Type* "      ++ pr_set false fwd_typ);
-  end;
-  let valid_exprs = ref [] in
-  let valid e = valid_exprs := e :: !valid_exprs in
-  if S.is_empty needed then valid (str "Type");
-  if S.equal all_needed fwd_typ then valid (str "Type*");
-  if S.equal all all_needed then valid(str "All");
-  valid (pr_set false needed);
-  Feedback.msg_info (
-    str"The proof of "++ str name ++ spc() ++
-    str "should start with one of the following commands:"++spc()++
-    v 0 (
-    prlist_with_sep cut (fun x->str"Proof using " ++x++ str". ") !valid_exprs));
-  string_of_ppcmds (prlist_with_sep (fun _ -> str";")  (fun x->x) !valid_exprs)
-;;
-
-let value = ref false
-
-let _ =
-  Goptions.declare_bool_option
-    { Goptions.optsync  = true;
-      Goptions.optdepr  = false;
-      Goptions.optname  = "suggest Proof using";
-      Goptions.optkey   = ["Suggest";"Proof";"Using"];
-      Goptions.optread  = (fun () -> !value);
-      Goptions.optwrite = (fun b ->
-        value := b;
-        if b then Term_typing.set_suggest_proof_using suggest_Proof_using
-        else Term_typing.set_suggest_proof_using (fun _ _ _ _ _ -> "")
-      ) }
-
-let value = ref None
-
-let _ =
-  Goptions.declare_stringopt_option
-    { Goptions.optsync  = true;
-      Goptions.optdepr  = false;
-      Goptions.optname  = "default value for Proof using";
-      Goptions.optkey   = ["Default";"Proof";"Using"];
-      Goptions.optread  = (fun () -> !value);
-      Goptions.optwrite = (fun b -> value := b;) }
-
-
-let get_default_proof_using () = !value
diff --git a/proofs/proof_using.mli b/proofs/proof_using.mli
deleted file mode 100644
index b2c65412..00000000
--- a/proofs/proof_using.mli
+++ /dev/null
@@ -1,19 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** Utility code for section variables handling in Proof using... *)
-
-val process_expr :
-  Environ.env -> Vernacexpr.section_subset_expr -> Constr.types list ->
-    Names.Id.t list
-
-val name_set : Names.Id.t -> Vernacexpr.section_subset_expr -> unit
-
-val to_string : Vernacexpr.section_subset_expr -> string
-
-val get_default_proof_using : unit -> string option
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index 804a5436..058e839b 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -1,10 +1,11 @@
 Miscprint
 Goal
 Evar_refiner
-Proof_using
+Proof_type
 Logic
 Refine
 Proof
+Proof_bullet
 Proof_global
 Redexpr
 Refiner
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 72cb05f1..6fb41193 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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 Pp
@@ -11,6 +13,7 @@ open CErrors
 open Util
 open Names
 open Term
+open EConstr
 open Declarations
 open Globnames
 open Genredexpr
@@ -24,10 +27,11 @@ open Misctypes
 
 (* call by value normalisation function using the virtual machine *)
 let cbv_vm env sigma c =
-  let ctyp = Retyping.get_type_of env sigma c in
-  if Termops.occur_meta_or_existential c then
-    error "vm_compute does not support existential variables.";
-  Vnorm.cbv_vm env c ctyp
+  if Coq_config.bytecode_compiler then
+    let ctyp = Retyping.get_type_of env sigma c in
+    Vnorm.cbv_vm env sigma c ctyp
+  else
+    compute env sigma c
 
 let warn_native_compute_disabled =
   CWarnings.create ~name:"native-compute-disabled" ~category:"native-compiler"
@@ -35,24 +39,25 @@ let warn_native_compute_disabled =
    strbrk "native_compute disabled at configure time; falling back to vm_compute.")
 
 let cbv_native env sigma c =
-  if Coq_config.no_native_compiler then
-    (warn_native_compute_disabled ();
-     cbv_vm env sigma c)
-  else
+  if Coq_config.native_compiler then
     let ctyp = Retyping.get_type_of env sigma c in
     Nativenorm.native_norm env sigma c ctyp
+  else
+    (warn_native_compute_disabled ();
+     cbv_vm env sigma c)
 
 let whd_cbn flags env sigma t =
   let (state,_) =
-    (whd_state_gen true true flags env sigma (t,Reductionops.Stack.empty))
-  in Reductionops.Stack.zip ~refold:true state
+    (whd_state_gen ~refold:true ~tactic_mode:true flags env sigma (t,Reductionops.Stack.empty))
+  in
+  Reductionops.Stack.zip ~refold:true sigma state
 
 let strong_cbn flags =
   strong (whd_cbn flags)
 
 let simplIsCbn = ref (false)
 let _ = Goptions.declare_bool_option {
-  Goptions.optsync = true; Goptions.optdepr = false;
+  Goptions.optdepr = false;
   Goptions.optname =
     "Plug the simpl tactic to the new cbn mechanism";
   Goptions.optkey = ["SimplIsCbn"];
@@ -73,7 +78,7 @@ let set_strategy_one ref l  =
         let cb = Global.lookup_constant sp in
 	(match cb.const_body with
 	  | OpaqueDef _ ->
-            errorlabstrm "set_transparent_const"
+            user_err ~hdr:"set_transparent_const"
               (str "Cannot make" ++ spc () ++
 		 Nametab.pr_global_env Id.Set.empty (ConstRef sp) ++
 		 spc () ++ str "transparent because it was declared opaque.");
@@ -175,19 +180,19 @@ let red_expr_tab = Summary.ref String.Map.empty ~name:"Declare Reduction"
 
 let declare_reduction s f =
   if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab
-  then errorlabstrm "Redexpr.declare_reduction"
+  then user_err ~hdr:"Redexpr.declare_reduction"
     (str "There is already a reduction expression of name " ++ str s)
   else reduction_tab := String.Map.add s f !reduction_tab
 
 let check_custom = function
   | ExtraRedExpr s ->
       if not (String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab)
-      then errorlabstrm "Redexpr.check_custom" (str "Reference to undefined reduction expression " ++ str s)
+      then user_err ~hdr:"Redexpr.check_custom" (str "Reference to undefined reduction expression " ++ str s)
   |_ -> ()
 
 let decl_red_expr s e =
   if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab
-  then errorlabstrm "Redexpr.decl_red_expr"
+  then user_err ~hdr:"Redexpr.decl_red_expr"
     (str "There is already a reduction expression of name " ++ str s)
   else begin
     check_custom e;
@@ -195,13 +200,13 @@ let decl_red_expr s e =
   end
 
 let out_arg = function
-  | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable")
+  | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable.")
   | ArgArg x -> x
 
 let out_with_occurrences (occs,c) =
   (Locusops.occurrences_map (List.map out_arg) occs, c)
 
-let e_red f = { e_redfun = fun env evm c -> Sigma.here (f env (Sigma.to_evar_map evm) c) evm }
+let e_red f env evm c = evm, f env evm c
 
 let head_style = false (* Turn to true to have a semantics where simpl
    only reduce at the head when an evaluable reference is given, e.g.
@@ -247,16 +252,19 @@ let reduction_of_red_expr env =
       with Not_found ->
 	(try reduction_of_red_expr (String.Map.find s !red_expr_tab)
 	 with Not_found ->
-	   errorlabstrm "Redexpr.reduction_of_red_expr"
+	   user_err ~hdr:"Redexpr.reduction_of_red_expr"
              (str "unknown user-defined reduction \"" ++ str s ++ str "\"")))
   | CbvVm o -> (contextualize cbv_vm cbv_vm o, VMcast)
   | CbvNative o -> (contextualize cbv_native cbv_native o, NATIVEcast)
   in
     reduction_of_red_expr
 
+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
-    (Mod_subst.subst_mps subs)
+    (subst_mps subs)
     (Mod_subst.subst_evaluable_reference subs)
     (Patternops.subst_pattern subs)
 
diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli
index d4c2c4a6..1e59f436 100644
--- a/proofs/redexpr.mli
+++ b/proofs/redexpr.mli
@@ -1,15 +1,18 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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)         *)
 (************************************************************************)
 
 (** Interpretation layer of redexprs such as hnf, cbv, etc. *)
 
 open Names
-open Term
+open Constr
+open EConstr
 open Pattern
 open Genredexpr
 open Reductionops
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 3f552706..909556b1 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -1,16 +1,19 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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 Util
-open Sigma.Notations
 open Proofview.Notations
 open Context.Named.Declaration
 
+module NamedDecl = Context.Named.Declaration
+
 let extract_prefix env info =
   let ctx1 = List.rev (Environ.named_context env) in
   let ctx2 = List.rev (Evd.evar_context info) in
@@ -26,12 +29,12 @@ let typecheck_evar ev env sigma =
   let info = Evd.find sigma ev in
   (** Typecheck the hypotheses. *)
   let type_hyp (sigma, env) decl =
-    let t = get_type decl in
+    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 body t
+    | LocalDef (_,body,_) -> Typing.e_check env evdref (EConstr.of_constr body) t
     in
     (!evdref, Environ.push_named decl env)
   in
@@ -40,7 +43,7 @@ let typecheck_evar ev env sigma =
   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 (Evd.evar_concl info) in
+  let _ = Typing.e_sort_of env evdref (EConstr.of_constr (Evd.evar_concl info)) in
   !evdref
 
 let typecheck_proof c concl env sigma =
@@ -68,38 +71,48 @@ let add_side_effect env = function
 let add_side_effects env effects =
   List.fold_left (fun env eff -> add_side_effect env eff) env effects
 
-let make_refine_enter ?(unsafe = true) f =
-  { enter = fun gl ->
-  let gl = Proofview.Goal.assume gl in
+let generic_refine ~typecheck f gl =
   let sigma = Proofview.Goal.sigma gl in
-  let sigma = Sigma.to_evar_map sigma in
   let env = Proofview.Goal.env gl in
   let concl = Proofview.Goal.concl gl in
+  let state = Proofview.Goal.state gl in
   (** Save the [future_goals] state to restore them after the
       refinement. *)
-  let prev_future_goals = Evd.future_goals sigma in
-  let prev_principal_goal = Evd.principal_future_goal sigma in
+  let prev_future_goals = Evd.save_future_goals sigma in
   (** Create the refinement term *)
-  let ((v,c), sigma) = Sigma.run (Evd.reset_future_goals sigma) f in
-  let evs = Evd.future_goals sigma in
-  let evkmain = Evd.principal_future_goal sigma in
+  Proofview.Unsafe.tclEVARS (Evd.reset_future_goals sigma) >>= fun () ->
+  f >>= fun (v, c) ->
+  Proofview.tclEVARMAP >>= fun sigma ->
+  Proofview.V82.wrap_exceptions begin fun () ->
+  let evs = Evd.save_future_goals sigma in
   (** Redo the effects in sigma in the monad's env *)
   let privates_csts = Evd.eval_side_effects sigma in
   let sideff = Safe_typing.side_effects_of_private_constants privates_csts in
   let env = add_side_effects env sideff in
   (** Check that the introduced evars are well-typed *)
   let fold accu ev = typecheck_evar ev env accu in
-  let sigma = if unsafe then sigma else CList.fold_left fold sigma evs 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 unsafe then sigma else typecheck_proof c concl env sigma in
+  let sigma = if typecheck then typecheck_proof c concl env sigma else sigma in
   (** Check that the goal itself does not appear in the refined term *)
   let self = Proofview.Goal.goal gl in
   let _ =
     if not (Evarutil.occur_evar_upto sigma self c) then ()
     else Pretype_errors.error_occur_check env sigma self c
   in
+  (** Restore the [future goals] state. *)
+  let sigma = Evd.restore_future_goals sigma prev_future_goals in
+  (** Select the goals *)
+  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 sigma = match evkmain with
+  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 *)
+    sigma
+  | Some self ->
+    match evkmain with
     | None -> Evd.define self c sigma
     | Some evk ->
         let id = Evd.evar_ident self sigma in
@@ -108,25 +121,37 @@ let make_refine_enter ?(unsafe = true) f =
         | None -> sigma
         | Some id -> Evd.rename evk id sigma
   in
-  (** Restore the [future goals] state. *)
-  let sigma = Evd.restore_future_goals sigma prev_future_goals prev_principal_goal in
-  (** Select the goals *)
-  let comb = CList.map_filter (Proofview.Unsafe.advance sigma) (CList.rev evs) in
+  (** 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
   Proofview.Trace.name_tactic trace (Proofview.tclUNIT v) >>= fun v ->
   Proofview.Unsafe.tclSETENV (Environ.reset_context env) <*>
   Proofview.Unsafe.tclEVARS sigma <*>
   Proofview.Unsafe.tclSETGOALS comb <*>
+  Proofview.Unsafe.tclPUTSHELF shelf <*>
+  Proofview.Unsafe.tclPUTGIVENUP given_up <*>
   Proofview.tclUNIT v
-  }
+  end
 
-let refine_one ?(unsafe = true) f =
-  Proofview.Goal.enter_one (make_refine_enter ~unsafe f)
+let lift c =
+  Proofview.tclEVARMAP >>= fun sigma ->
+  Proofview.V82.wrap_exceptions begin fun () ->
+  let (sigma, c) = c sigma in
+  Proofview.Unsafe.tclEVARS sigma >>= fun () ->
+  Proofview.tclUNIT c
+  end
 
-let refine ?(unsafe = true) f =
-  let f = { run = fun sigma -> let Sigma (c,sigma,p) = f.run sigma in Sigma (((),c),sigma,p) } in
-  Proofview.Goal.enter (make_refine_enter ~unsafe f)
+let make_refine_enter ~typecheck f gl = generic_refine ~typecheck (lift f) gl
+
+let refine_one ~typecheck f =
+  Proofview.Goal.enter_one (make_refine_enter ~typecheck f)
+
+let refine ~typecheck f =
+  let f evd =
+    let (evd,c) = f evd in (evd,((), c))
+  in
+  Proofview.Goal.enter (make_refine_enter ~typecheck f)
 
 (** Useful definitions *)
 
@@ -134,21 +159,19 @@ let with_type env evd c t =
   let my_type = Retyping.get_type_of env evd c in
   let j = Environ.make_judge c my_type in
   let (evd,j') =
-    Coercion.inh_conv_coerce_to true (Loc.ghost) env evd j t
+    Coercion.inh_conv_coerce_to true env evd j t
   in
   evd , j'.Environ.uj_val
 
-let refine_casted ?unsafe f = Proofview.Goal.enter { enter = begin fun gl ->
-  let gl = Proofview.Goal.assume gl in
+let refine_casted ~typecheck f = Proofview.Goal.enter begin fun gl ->
   let concl = Proofview.Goal.concl gl in
   let env = Proofview.Goal.env gl in
-  let f = { run = fun h ->
-    let Sigma (c, h, p) = f.run h in
-    let sigma, c = with_type env (Sigma.to_evar_map h) c concl in
-    Sigma (c, Sigma.Unsafe.of_evar_map sigma, p)
-  } in
-  refine ?unsafe f
-end }
+  let f h =
+    let (h, c) = f h in
+    with_type env h c concl
+  in
+  refine ~typecheck f
+end
 
 (** {7 solve_constraints}
 
diff --git a/proofs/refine.mli b/proofs/refine.mli
index a44632ef..70a23a9f 100644
--- a/proofs/refine.mli
+++ b/proofs/refine.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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)         *)
 (************************************************************************)
 
 (** The primitive refine tactic used to fill the holes in partial proofs. This
@@ -17,30 +19,33 @@ open Proofview
 
 (** Printer used to print the constr which refine refines. *)
 val pr_constr :
-  (Environ.env -> Evd.evar_map -> Term.constr -> Pp.std_ppcmds) Hook.t
+  (Environ.env -> Evd.evar_map -> Constr.constr -> Pp.t) Hook.t
 
 (** {7 Refinement primitives} *)
 
-val refine : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic
-(** In [refine ?unsafe t], [t] is a term with holes under some
+val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit tactic
+(** In [refine ~typecheck t], [t] is a term with holes under some
     [evar_map] context. The term [t] is used as a partial solution
     for the current goal (refine is a goal-dependent tactic), the
     new holes created by [t] become the new subgoals. Exceptions
     raised during the interpretation of [t] are caught and result in
-    tactic failures. If [unsafe] is [false] (default is [true]) [t] is
-    type-checked beforehand. *)
+    tactic failures. If [typecheck] is [true] [t] is type-checked beforehand. *)
 
-val refine_one : ?unsafe:bool -> ('a * Constr.t) Sigma.run -> 'a tactic
-(** A generalization of [refine] which assumes exactly one goal under focus *)
+val refine_one : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * ('a * EConstr.t)) -> 'a tactic
+(** A variant of [refine] which assumes exactly one goal under focus *)
+
+val generic_refine : typecheck:bool -> ('a * EConstr.t) tactic ->
+  Proofview.Goal.t -> 'a tactic
+(** The general version of refine. *)
 
 (** {7 Helper functions} *)
 
 val with_type : Environ.env -> Evd.evar_map ->
-  Term.constr -> Term.types -> Evd.evar_map * Term.constr
+  EConstr.constr -> EConstr.types -> Evd.evar_map * EConstr.constr
 (** [with_type env sigma c t] ensures that [c] is of type [t]
     inserting a coercion if needed. *)
 
-val refine_casted : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic
+val refine_casted : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit tactic
 (** Like {!refine} except the refined term is coerced to the conclusion of the
     current goal. *)
 
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index ea8543b0..be32aadd 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -1,19 +1,21 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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 Pp
 open CErrors
 open Util
 open Evd
-open Environ
 open Proof_type
 open Logic
-open Context.Named.Declaration
+
+module NamedDecl = Context.Named.Declaration
 
 let sig_it x = x.it
 let project x = x.sigma
@@ -21,7 +23,7 @@ let project x = x.sigma
 (* Getting env *)
 
 let pf_env gls = Global.env_of_context (Goal.V82.hyps (project gls) (sig_it gls))
-let pf_hyps gls = named_context_of_val (Goal.V82.hyps (project gls) (sig_it gls))
+let pf_hyps gls = EConstr.named_context_of_val (Goal.V82.hyps (project gls) (sig_it gls))
 
 let refiner pr goal_sigma =
   let (sgl,sigma') = prim_refiner pr goal_sigma.sigma goal_sigma.it in
@@ -30,8 +32,8 @@ let refiner pr goal_sigma =
 (* Profiling refiner *)
 let refiner = 
   if Flags.profile then
-    let refiner_key = Profile.declare_profile "refiner" in
-      Profile.profile2 refiner_key refiner
+    let refiner_key = CProfile.declare_profile "refiner" in
+      CProfile.profile2 refiner_key refiner
   else refiner
 
 (*********************)
@@ -60,10 +62,10 @@ let tclIDTAC_MESSAGE s gls =
   Feedback.msg_info (hov 0 s); tclIDTAC gls
 
 (* General failure tactic *)
-let tclFAIL_s s gls = errorlabstrm "Refiner.tclFAIL_s" (str s)
+let tclFAIL_s s gls = user_err ~hdr:"Refiner.tclFAIL_s" (str s)
 
 (* A special exception for levels for the Fail tactic *)
-exception FailError of int * std_ppcmds Lazy.t
+exception FailError of int * Pp.t Lazy.t
 
 (* The Fail tactic *)
 let tclFAIL lvl s g = raise (FailError (lvl,lazy s))
@@ -82,7 +84,7 @@ let thens3parts_tac tacfi tac tacli (sigr,gs) =
   let nf = Array.length tacfi in
   let nl = Array.length tacli in
   let ng = List.length gs in
-  if ng<nf+nl then errorlabstrm "Refiner.thensn_tac" (str "Not enough subgoals.");
+  if ng<nf+nl then user_err ~hdr:"Refiner.thensn_tac" (str "Not enough subgoals.");
   let gll =
       (List.map_i (fun i ->
         apply_sig_tac sigr (if i<nf then tacfi.(i) else if i>=ng-nl then tacli.(nl-ng+i) else tac))
@@ -161,30 +163,10 @@ let tclMAP tacfun l =
 
 (* PROGRESS tac ptree applies tac to the goal ptree and fails if tac leaves
 the goal unchanged *)
-let tclWEAK_PROGRESS tac ptree =
-  let rslt = tac ptree in
-  if Goal.V82.weak_progress rslt ptree then rslt
-  else errorlabstrm "Refiner.WEAK_PROGRESS" (str"Failed to progress.")
-
-(* PROGRESS tac ptree applies tac to the goal ptree and fails if tac leaves
-the goal unchanged *)
 let tclPROGRESS tac ptree =
   let rslt = tac ptree in
   if Goal.V82.progress rslt ptree then rslt
-  else errorlabstrm "Refiner.PROGRESS" (str"Failed to progress.")
-
-(* Same as tclWEAK_PROGRESS but fails also if tactics generates several goals,
-   one of them being identical to the original goal *)
-let tclNOTSAMEGOAL (tac : tactic) goal =
-  let same_goal gls1 evd2 gl2 =
-    Goal.V82.same_goal gls1.sigma gls1.it evd2 gl2
-  in
-  let rslt = tac goal in
-  let {it=gls;sigma=sigma} = rslt in
-  if List.exists (same_goal goal sigma) gls
-  then errorlabstrm "Refiner.tclNOTSAMEGOAL"
-      (str"Tactic generated a subgoal identical to the original goal.")
-  else rslt
+  else user_err ~hdr:"Refiner.PROGRESS" (str"Failed to progress.")
 
 (* Execute tac, show the names of new hypothesis names created by tac
    in the "as" format and then forget everything. From the logical
@@ -197,31 +179,29 @@ let tclNOTSAMEGOAL (tac : tactic) goal =
    destruct), this is not detected by this tactical. *)
 let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
     :Proof_type.goal list Evd.sigma =
-  let oldhyps:Context.Named.t = pf_hyps goal in
+  let oldhyps = pf_hyps goal in
   let rslt:Proof_type.goal list Evd.sigma = tac goal in
   let { it = gls; sigma = sigma; } = rslt in
-  let hyps:Context.Named.t list =
+  let hyps =
     List.map (fun gl -> pf_hyps { it = gl; sigma=sigma; }) gls in
-  let cmp d1 d2 = Names.Id.equal (get_id d1) (get_id d2) in
+  let cmp d1 d2 = Names.Id.equal (NamedDecl.get_id d1) (NamedDecl.get_id d2) in
   let newhyps =
     List.map
       (fun hypl -> List.subtract cmp hypl oldhyps)
       hyps
   in
-  let emacs_str s =
-    if !Flags.print_emacs then s else "" in
   let s = 
     let frst = ref true in
     List.fold_left
     (fun acc lh -> acc ^ (if !frst then (frst:=false;"") else " | ")
       ^ (List.fold_left
-	   (fun acc d -> (Names.Id.to_string (get_id d)) ^ " " ^ acc)
+	   (fun acc d -> (Names.Id.to_string (NamedDecl.get_id d)) ^ " " ^ acc)
 	   "" lh))
     "" newhyps in
   Feedback.msg_notice
-    (str (emacs_str "<infoH>")
+    (str "<infoH>"
       ++  (hov 0 (str s))
-      ++  (str (emacs_str "</infoH>")));
+      ++  (str "</infoH>"));
   tclIDTAC goal;;
 
 
@@ -316,7 +296,7 @@ let tclSOLVE tacl = tclFIRST (List.map tclCOMPLETE tacl)
 
 let tclDO n t =
   let rec dorec k =
-    if k < 0 then errorlabstrm "Refiner.tclDO"
+    if k < 0 then user_err ~hdr:"Refiner.tclDO"
       (str"Wrong argument : Do needs a positive integer.");
     if Int.equal k 0 then tclIDTAC
     else if Int.equal k 1 then t else (tclTHEN t (dorec (k-1)))
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 6dcafb77..5cd703a2 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -1,15 +1,18 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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)         *)
 (************************************************************************)
 
 (** Legacy proof engine. Do not use in newly written code. *)
 
 open Evd
 open Proof_type
+open EConstr
 
 (** The refiner (handles primitive rules and high-level tactics). *)
 
@@ -17,7 +20,7 @@ val sig_it  : 'a sigma -> 'a
 val project : 'a sigma -> evar_map
 
 val pf_env  : goal sigma -> Environ.env
-val pf_hyps : goal sigma -> Context.Named.t
+val pf_hyps : goal sigma -> named_context
 
 val unpackage : 'a sigma -> evar_map ref * 'a
 val repackage : evar_map ref -> 'a -> 'a sigma
@@ -30,16 +33,16 @@ val refiner : rule -> tactic
 
 (** [tclIDTAC] is the identity tactic without message printing*)
 val tclIDTAC          : tactic
-val tclIDTAC_MESSAGE  : Pp.std_ppcmds -> tactic
+val tclIDTAC_MESSAGE  : Pp.t -> tactic
 
 (** [tclEVARS sigma] changes the current evar map *)
 val tclEVARS : evar_map -> tactic
-val tclEVARUNIVCONTEXT : Evd.evar_universe_context -> tactic
+val tclEVARUNIVCONTEXT : UState.t -> tactic
 
-val tclPUSHCONTEXT : Evd.rigid -> Univ.universe_context_set -> tactic -> tactic
-val tclPUSHEVARUNIVCONTEXT : Evd.evar_universe_context -> tactic
+val tclPUSHCONTEXT : Evd.rigid -> Univ.ContextSet.t -> tactic -> tactic
+val tclPUSHEVARUNIVCONTEXT : UState.t -> tactic
 
-val tclPUSHCONSTRAINTS : Univ.constraints -> tactic
+val tclPUSHCONSTRAINTS : Univ.Constraint.t -> tactic
 
 (** [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
    [tac2] to every resulting subgoals *)
@@ -99,7 +102,7 @@ val tclTHENLASTn    : tactic -> tactic array -> tactic
 val tclTHENFIRSTn   : tactic -> tactic array -> tactic
 
 (** A special exception for levels for the Fail tactic *)
-exception FailError of int * Pp.std_ppcmds Lazy.t
+exception FailError of int * Pp.t Lazy.t
 
 (** Takes an exception and either raise it at the next
    level or do nothing. *)
@@ -115,13 +118,11 @@ val tclTRY           : tactic -> tactic
 val tclTHENTRY       : tactic -> tactic -> tactic
 val tclCOMPLETE      : tactic -> tactic
 val tclAT_LEAST_ONCE : tactic -> tactic
-val tclFAIL          : int -> Pp.std_ppcmds -> tactic
-val tclFAIL_lazy     : int -> Pp.std_ppcmds Lazy.t -> tactic
+val tclFAIL          : int -> Pp.t -> tactic
+val tclFAIL_lazy     : int -> Pp.t Lazy.t -> tactic
 val tclDO            : int -> tactic -> tactic
-val tclWEAK_PROGRESS : tactic -> tactic
 val tclPROGRESS      : tactic -> tactic
 val tclSHOWHYPS      : tactic -> tactic
-val tclNOTSAMEGOAL   : tactic -> tactic
 
 (** [tclIFTHENELSE tac1 tac2 tac3 gls] first applies [tac1] to [gls] then,
    if it succeeds, applies [tac2] to the resulting subgoals,
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 330594af..1889054f 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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 Util
@@ -18,9 +20,10 @@ open Tacred
 open Proof_type
 open Logic
 open Refiner
-open Sigma.Notations
 open Context.Named.Declaration
 
+module NamedDecl = Context.Named.Declaration
+
 let re_sig it  gc = { it = it; sigma = gc; }
 
 (**************************************************************)
@@ -39,44 +42,43 @@ let project  = Refiner.project
 let pf_env   = Refiner.pf_env
 let pf_hyps  = Refiner.pf_hyps
 
+let test_conversion env sigma pb c1 c2 =
+  Reductionops.check_conv ~pb env sigma c1 c2
+
 let pf_concl gls = Goal.V82.concl (project gls) (sig_it gls)
 let pf_hyps_types gls  =
   let sign = Environ.named_context (pf_env gls) in
   List.map (function LocalAssum (id,x)
-                   | LocalDef (id,_,x) -> id, x)
+                   | LocalDef (id,_,x) -> id, EConstr.of_constr x)
            sign
 
-let pf_nth_hyp_id gls n = List.nth (pf_hyps gls) (n-1) |> get_id
+let pf_nth_hyp_id gls n = List.nth (pf_hyps gls) (n-1) |> NamedDecl.get_id
 
 let pf_last_hyp gl = List.hd (pf_hyps gl)
 
 let pf_get_hyp gls id =
+  let env, sigma = pf_env gls, project gls in
   try
     Context.Named.lookup id (pf_hyps gls)
   with Not_found ->
-    raise (RefinerError (NoSuchHyp id))
+    raise (RefinerError (env, sigma, NoSuchHyp id))
 
 let pf_get_hyp_typ gls id =
-  pf_get_hyp gls id |> get_type
+  id |> pf_get_hyp gls |> NamedDecl.get_type
 
 let pf_ids_of_hyps gls = ids_of_named_context (pf_hyps gls)
+let pf_ids_set_of_hyps gls =
+  Environ.ids_of_named_context_val (Environ.named_context_val (pf_env gls))
 
 let pf_get_new_id id gls =
-  next_ident_away id (pf_ids_of_hyps gls)
-
-let pf_get_new_ids ids gls =
-  let avoid = pf_ids_of_hyps gls in
-  List.fold_right
-    (fun id acc -> (next_ident_away id (acc@avoid))::acc)
-    ids []
+  next_ident_away id (pf_ids_set_of_hyps gls)
 
-let pf_global gls id = Constrintern.construct_reference (pf_hyps gls) id
+let pf_global gls id = EConstr.of_constr (Universes.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
-  let sigma = Sigma.Unsafe.of_evar_map (project gls) in
-  let Sigma (c, sigma, _) = redfun.e_redfun (pf_env gls) sigma c in
-  (Sigma.to_evar_map sigma, c)
+  let sigma = project gls in
+  redfun (pf_env gls) sigma c
 
 let pf_apply f gls = f (pf_env gls) (project gls)
 let pf_eapply f gls x = 
@@ -87,7 +89,7 @@ let pf_e_reduce = pf_apply
 let pf_whd_all         = pf_reduce whd_all
 let pf_hnf_constr                = pf_reduce hnf_constr
 let pf_nf                        = pf_reduce simpl
-let pf_nf_betaiota               = pf_reduce (fun _ -> nf_betaiota)
+let pf_nf_betaiota               = pf_reduce nf_betaiota
 let pf_compute                   = pf_reduce compute
 let pf_unfoldn ubinds            = pf_reduce (unfoldn ubinds)
 let pf_unsafe_type_of            = pf_reduce unsafe_type_of
@@ -96,15 +98,12 @@ let pf_get_type_of               = pf_reduce Retyping.get_type_of
 
 let pf_conv_x gl                = pf_reduce test_conversion gl Reduction.CONV
 let pf_conv_x_leq gl            = pf_reduce test_conversion gl Reduction.CUMUL
-let pf_const_value              = pf_reduce (fun env _ -> constant_value_in env)
+let pf_const_value              = pf_reduce (fun env _ c -> EConstr.of_constr (constant_value_in env c))
 
 let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind
 let pf_reduce_to_atomic_ind     = pf_reduce reduce_to_atomic_ind
 
-let pf_hnf_type_of gls          = pf_whd_all gls % pf_get_type_of gls
-
-let pf_is_matching              = pf_apply Constr_matching.is_matching_conv
-let pf_matches                  = pf_apply Constr_matching.matches_conv
+let pf_hnf_type_of gls          = pf_get_type_of gls %> pf_whd_all gls
 
 (********************************************)
 (* Definition of the most primitive tactics *)
@@ -112,19 +111,12 @@ let pf_matches                  = pf_apply Constr_matching.matches_conv
 
 let refiner = refiner
 
-let internal_cut_no_check replace id t gl =
-  refiner (Cut (true,replace,id,t)) gl
-
-let internal_cut_rev_no_check replace id t gl =
-  refiner (Cut (false,replace,id,t)) gl
-
 let refine_no_check c gl =
+  let c = EConstr.Unsafe.to_constr c in
   refiner (Refine c) gl
 
 (* Versions with consistency checks *)
 
-let internal_cut b d t = with_check (internal_cut_no_check b d t)
-let internal_cut_rev b d t = with_check (internal_cut_rev_no_check b d t)
 let refine c           = with_check (refine_no_check c)
 
 (* Pretty-printers *)
@@ -134,7 +126,7 @@ 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 (Goal.V82.concl sigma g) in
+  let pc = print_constr_env env sigma (Goal.V82.concl sigma g) in
   str"  " ++ hv 0 (penv ++ fnl () ++
                    str "============================" ++ fnl ()  ++
                    str" "  ++ pc) ++ fnl ()
@@ -150,8 +142,7 @@ let pr_glls glls =
 module New = struct
 
   let project gl =
-    let sigma = Proofview.Goal.sigma gl in
-    Sigma.to_evar_map sigma
+    Proofview.Goal.sigma gl
 
   let pf_apply f gl =
     f (Proofview.Goal.env gl) (project gl)
@@ -161,7 +152,6 @@ module New = struct
 
   let pf_global id gl =
     (** We only check for the existence of an [id] in [hyps] *)
-    let gl = Proofview.Goal.assume gl in
     let hyps = Proofview.Goal.hyps gl in
     Constrintern.construct_reference hyps id
 
@@ -171,9 +161,6 @@ module New = struct
   let pf_unsafe_type_of gl t =
     pf_apply unsafe_type_of gl t
 
-  let pf_get_type_of gl t =
-    pf_apply (Retyping.get_type_of ~lax:true) gl t
-
   let pf_type_of gl t =
     pf_apply type_of gl t
 
@@ -181,39 +168,43 @@ module New = struct
 
   let pf_ids_of_hyps gl =
     (** We only get the identifiers in [hyps] *)
-    let gl = Proofview.Goal.assume gl in
     let hyps = Proofview.Goal.hyps gl in
     ids_of_named_context hyps
 
+  let pf_ids_set_of_hyps gl =
+    (** We only get the identifiers in [hyps] *)
+    let env = Proofview.Goal.env gl in
+    Environ.ids_of_named_context_val (Environ.named_context_val env)
+
   let pf_get_new_id id gl =
-    let ids = pf_ids_of_hyps gl in
+    let ids = pf_ids_set_of_hyps gl in
     next_ident_away id ids
 
   let pf_get_hyp id gl =
     let hyps = Proofview.Goal.env gl in
+    let sigma = project gl in
     let sign =
-      try Environ.lookup_named id hyps
-      with Not_found -> raise (RefinerError (NoSuchHyp id))
+      try EConstr.lookup_named id hyps
+      with Not_found -> raise (RefinerError (hyps, sigma, NoSuchHyp id))
     in
     sign
 
   let pf_get_hyp_typ id gl =
-    pf_get_hyp id gl |> get_type
+    pf_get_hyp id gl |> NamedDecl.get_type
 
   let pf_hyps_types gl =
     let env = Proofview.Goal.env gl in
     let sign = Environ.named_context env in
     List.map (function LocalAssum (id,x)
-                     | LocalDef (id,_,x) -> id, x)
+                     | LocalDef (id,_,x) -> id, EConstr.of_constr x)
              sign
 
   let pf_last_hyp gl =
     let hyps = Proofview.Goal.hyps gl in
     List.hd hyps
 
-  let pf_nf_concl (gl : ([ `LZ ], 'r) Proofview.Goal.t) =
+  let pf_nf_concl (gl : Proofview.Goal.t) =
     (** We normalize the conclusion just after *)
-    let gl = Proofview.Goal.assume gl in
     let concl = Proofview.Goal.concl gl in
     let sigma = project gl in
     nf_evar sigma concl
@@ -229,8 +220,6 @@ module New = struct
   let pf_hnf_type_of gl t =
     pf_whd_all gl (pf_get_type_of gl t)
 
-  let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat t
-
   let pf_whd_all gl t = pf_apply whd_all gl t
   let pf_compute gl t = pf_apply compute gl t
 
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 59f296f6..770d0940 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -1,24 +1,27 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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
-open Term
+open Constr
 open Environ
-open Evd
+open EConstr
 open Proof_type
 open Redexpr
-open Pattern
 open Locus
-open Misctypes
 
 (** Operations for handling terms under a local typing context. *)
 
-type 'a sigma   = 'a Evd.sigma;;
+type 'a sigma   = 'a Evd.sigma
+[@@ocaml.deprecated "alias of Evd.sigma"]
+
+open Evd
 type tactic     = Proof_type.tactic;;
 
 val sig_it  : 'a sigma   -> 'a
@@ -33,22 +36,21 @@ val apply_sig_tac :
 
 val pf_concl              : goal sigma -> types
 val pf_env                : goal sigma -> env
-val pf_hyps               : goal sigma -> Context.Named.t
+val pf_hyps               : goal sigma -> named_context
 (*i val pf_untyped_hyps       : goal sigma -> (Id.t * constr) list i*)
 val pf_hyps_types         : goal sigma -> (Id.t * types) list
 val pf_nth_hyp_id         : goal sigma -> int -> Id.t
-val pf_last_hyp           : goal sigma -> Context.Named.Declaration.t
+val pf_last_hyp           : goal sigma -> named_declaration
 val pf_ids_of_hyps        : goal sigma -> Id.t list
 val pf_global             : goal sigma -> Id.t -> constr
 val pf_unsafe_type_of            : goal sigma -> constr -> types
 val pf_type_of            : goal sigma -> constr -> evar_map * types
 val pf_hnf_type_of        : goal sigma -> constr -> types
 
-val pf_get_hyp            : goal sigma -> Id.t -> Context.Named.Declaration.t
+val pf_get_hyp            : goal sigma -> Id.t -> named_declaration
 val pf_get_hyp_typ        : goal sigma -> Id.t -> types
 
 val pf_get_new_id  : Id.t      -> goal sigma -> Id.t
-val pf_get_new_ids : Id.t list -> goal sigma -> Id.t list
 
 val pf_reduction_of_red_expr : goal sigma -> red_expr -> constr -> evar_map * constr
 
@@ -67,8 +69,8 @@ val pf_whd_all       : goal sigma -> constr -> constr
 val pf_hnf_constr              : goal sigma -> constr -> constr
 val pf_nf                      : goal sigma -> constr -> constr
 val pf_nf_betaiota             : goal sigma -> constr -> constr
-val pf_reduce_to_quantified_ind : goal sigma -> types -> pinductive * types
-val pf_reduce_to_atomic_ind     : goal sigma -> types -> pinductive * types
+val pf_reduce_to_quantified_ind : goal sigma -> types -> (inductive * EInstance.t) * types
+val pf_reduce_to_atomic_ind     : goal sigma -> types -> (inductive * EInstance.t) * types
 val pf_compute                 : goal sigma -> constr -> constr
 val pf_unfoldn    : (occurrences * evaluable_global_reference) list
   -> goal sigma -> constr -> constr
@@ -77,69 +79,61 @@ val pf_const_value : goal sigma -> pconstant -> constr
 val pf_conv_x      : goal sigma -> constr -> constr -> bool
 val pf_conv_x_leq  : goal sigma -> constr -> constr -> bool
 
-val pf_matches     : goal sigma -> constr_pattern -> constr -> patvar_map
-val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool
-
-
 (** {6 The most primitive tactics. } *)
 
 val refiner                   : rule -> tactic
-val internal_cut_no_check     : bool -> Id.t -> types -> tactic
 val refine_no_check           : constr -> tactic
 
 (** {6 The most primitive tactics with consistency and type checking } *)
 
-val internal_cut     : bool -> Id.t -> types -> tactic
-val internal_cut_rev : bool -> Id.t -> types -> tactic
 val refine           : constr -> tactic
 
 (** {6 Pretty-printing functions (debug only). } *)
-val pr_gls    : goal sigma -> Pp.std_ppcmds
-val pr_glls   : goal list sigma -> Pp.std_ppcmds
+val pr_gls    : goal sigma -> Pp.t
+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) -> ('b, 'r) Proofview.Goal.t -> 'a
-  val pf_global : identifier -> ('a, 'r) Proofview.Goal.t -> constr
+  val pf_apply : (env -> evar_map -> 'a) -> Proofview.Goal.t -> 'a
+  val pf_global : Id.t -> Proofview.Goal.t -> Globnames.global_reference
   (** FIXME: encapsulate the level in an existential type. *)
-  val of_old : (Proof_type.goal Evd.sigma -> 'a) -> ([ `NF ], 'r) Proofview.Goal.t -> 'a
+  val of_old : (Proof_type.goal Evd.sigma -> 'a) -> Proofview.Goal.t -> 'a
 
-  val project : ('a, 'r) Proofview.Goal.t -> Evd.evar_map
-  val pf_env : ('a, 'r) Proofview.Goal.t -> Environ.env
-  val pf_concl : ([ `NF ], 'r) Proofview.Goal.t -> types
+  val project : Proofview.Goal.t -> Evd.evar_map
+  val pf_env : Proofview.Goal.t -> Environ.env
+  val pf_concl : Proofview.Goal.t -> types
 
   (** WRONG: To be avoided at all costs, it typechecks the term entirely but
      forgets the universe constraints necessary to retypecheck it *)
-  val pf_unsafe_type_of : ('a, 'r) Proofview.Goal.t -> Term.constr -> Term.types
+  val pf_unsafe_type_of : Proofview.Goal.t -> constr -> types
 
   (** This function does no type inference and expects an already well-typed term.
       It recomputes its type in the fastest way possible (no conversion is ever involved) *)
-  val pf_get_type_of : ('a, 'r) Proofview.Goal.t -> Term.constr -> Term.types
+  val pf_get_type_of : Proofview.Goal.t -> constr -> types
 
   (** This function entirely type-checks the term and computes its type
       and the implied universe constraints. *)
-  val pf_type_of : ('a, 'r) Proofview.Goal.t -> Term.constr -> evar_map * Term.types
-  val pf_conv_x : ('a, 'r) Proofview.Goal.t -> Term.constr -> Term.constr -> bool
-
-  val pf_get_new_id  : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> identifier
-  val pf_ids_of_hyps : ('a, 'r) Proofview.Goal.t -> identifier list
-  val pf_hyps_types : ('a, 'r) Proofview.Goal.t -> (identifier * types) list
+  val pf_type_of : Proofview.Goal.t -> constr -> evar_map * types
+  val pf_conv_x : Proofview.Goal.t -> t -> t -> bool
 
-  val pf_get_hyp : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> Context.Named.Declaration.t
-  val pf_get_hyp_typ        : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> types
-  val pf_last_hyp           : ([ `NF ], 'r) Proofview.Goal.t -> Context.Named.Declaration.t
+  val pf_get_new_id  : Id.t -> Proofview.Goal.t -> Id.t
+  val pf_ids_of_hyps : Proofview.Goal.t -> Id.t list
+  val pf_ids_set_of_hyps : Proofview.Goal.t -> Id.Set.t
+  val pf_hyps_types : Proofview.Goal.t -> (Id.t * types) list
 
-  val pf_nf_concl : ([ `LZ ], 'r) Proofview.Goal.t -> types
-  val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> types -> pinductive * types
+  val pf_get_hyp : Id.t -> Proofview.Goal.t -> named_declaration
+  val pf_get_hyp_typ        : Id.t -> Proofview.Goal.t -> types
+  val pf_last_hyp           : Proofview.Goal.t -> named_declaration
 
-  val pf_hnf_constr : ('a, 'r) Proofview.Goal.t -> constr -> types
-  val pf_hnf_type_of : ('a, 'r) Proofview.Goal.t -> constr -> types
+  val pf_nf_concl : Proofview.Goal.t -> types
+  val pf_reduce_to_quantified_ind : Proofview.Goal.t -> types -> (inductive * EInstance.t) * types
 
-  val pf_whd_all : ('a, 'r) Proofview.Goal.t -> constr -> constr
-  val pf_compute : ('a, 'r) Proofview.Goal.t -> constr -> constr
+  val pf_hnf_constr : Proofview.Goal.t -> constr -> types
+  val pf_hnf_type_of : Proofview.Goal.t -> constr -> types
 
-  val pf_matches : ('a, 'r) Proofview.Goal.t -> constr_pattern -> constr -> patvar_map
+  val pf_whd_all : Proofview.Goal.t -> constr -> constr
+  val pf_compute : Proofview.Goal.t -> constr -> constr
 
-  val pf_nf_evar : ('a, 'r) Proofview.Goal.t -> constr -> constr
+  val pf_nf_evar : Proofview.Goal.t -> constr -> constr
 
 end