Imported Upstream version 8.6upstream/8.6

36 files changed, 703 insertions, 3655 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 88e1bce9..0a90e0db 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Names
 open Nameops
@@ -24,6 +24,7 @@ open Pretype_errors
 open Evarutil
 open Unification
 open Misctypes
+open Sigma.Notations
 
 (* Abbreviations *)
 
@@ -71,7 +72,7 @@ let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) c
 exception NotExtensibleClause
 
 let clenv_push_prod cl =
-  let typ = whd_betadeltaiota (cl_env cl) (cl_sigma cl) (clenv_type cl) in
+  let typ = whd_all (cl_env cl) (cl_sigma cl) (clenv_type cl) in
   let rec clrec typ = match kind_of_term typ with
     | Cast (t,_,_) -> clrec t
     | Prod (na,t,u) ->
@@ -108,7 +109,7 @@ let clenv_environments evd bound t =
       | (n, Cast (t,_,_)) -> clrec (e,metas) n t
       | (n, Prod (na,t1,t2)) ->
 	  let mv = new_meta () in
-	  let dep = dependent (mkRel 1) t2 in
+	  let dep = not (noccurn 1 t2) in
 	  let na' = if dep then na else Anonymous in
 	  let e' = meta_declare mv t1 ~name:na' e in
 	  clrec (e', (mkMeta mv)::metas) (Option.map ((+) (-1)) n)
@@ -119,7 +120,7 @@ let clenv_environments evd bound t =
   clrec (evd,[]) bound t
 
 let mk_clenv_from_env env sigma n (c,cty) =
-  let evd = create_goal_evar_defs sigma in
+  let evd = clear_metas sigma in
   let (evd,args,concl) = clenv_environments evd n cty in
   { templval = mk_freelisted (applist (c,args));
     templtyp = mk_freelisted concl;
@@ -335,22 +336,15 @@ let clenv_pose_metas_as_evars clenv dep_mvs =
       else
         let src = evar_source_of_meta mv clenv.evd in
         let src = adjust_meta_source clenv.evd mv src in
-	let (evd,evar) = new_evar (cl_env clenv) clenv.evd ~src ty 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 clenv = clenv_assign mv evar {clenv with evd=evd} in
 	fold clenv mvs in
   fold clenv dep_mvs
 
 (******************************************************************)
 
-let connect_clenv gls clenv =
-  let evd = evars_reset_evd ~with_conv_pbs:true gls.sigma clenv.evd in
-  { clenv with
-    evd = evd ;
-    env = Goal.V82.env evd (sig_it gls) }
-
-(* let connect_clenv_key = Profile.declare_profile "connect_clenv";; *)
-(* let connect_clenv = Profile.profile2 connect_clenv_key connect_clenv *)
-
 (* [clenv_fchain mv clenv clenv']
  *
  * Resolves the value of "mv" (which must be undefined) in clenv to be
@@ -432,6 +426,44 @@ let check_bindings bl =
 	   str " occurs more than once in binding list.")
     | [] -> ()
 
+let explain_no_such_bound_variable evd id =
+  let fold l (n, clb) =
+    let na = match clb with
+    | Cltyp (na, _) -> na
+    | Clval (na, _, _) -> na
+    in
+    if na != Anonymous then out_name 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 ++
+     (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").")))
+
+let meta_with_name evd id =
+  let na = Name id in
+  let fold (l1, l2 as l) (n, clb) =
+    let (na',def) = match clb with
+    | Cltyp (na, _) -> (na, false)
+    | Clval (na, _, _) -> (na, true)
+    in
+    if Name.equal na na' then if def then (n::l1,l2) else (n::l1,n::l2)
+    else l
+  in
+  let (mvl, mvnodef) = List.fold_left fold ([], []) (Evd.meta_list evd) in
+  match mvnodef, mvl with
+    | _,[]  ->
+      explain_no_such_bound_variable evd id
+    | ([n],_|_,[n]) ->
+        n
+    | _  ->
+        errorlabstrm "Evd.meta_with_name"
+          (str "Binder name \"" ++ pr_id id ++
+           strbrk "\" occurs more than once in clause.")
+
 let meta_of_binder clause loc mvs = function
   | NamedHyp s -> meta_with_name clause.evd s
   | AnonHyp n ->
@@ -459,7 +491,8 @@ let clenv_unify_binding_type clenv c t u =
       let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd c t u in
       TypeProcessed, { clenv with evd = evd }, c
     with 
-      | PretypeError (_,_,ActualTypeNotCoercible (_,_,NotClean _)) as e ->
+      | PretypeError (_,_,ActualTypeNotCoercible (_,_,
+          (NotClean _ | ConversionFailed _))) as e ->
 	  raise e
       | e when precatchable_exception e ->
 	  TypeNotProcessed, clenv, c
@@ -576,7 +609,9 @@ let make_evar_clause env sigma ?len t =
     | Cast (t, _, _) -> clrec (sigma, holes) n t
     | Prod (na, t1, t2) ->
       let store = Typeclasses.set_resolvable Evd.Store.empty false in
-      let sigma, ev = new_evar ~store env sigma t1 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 hole = {
         hole_evar = ev;
@@ -628,7 +663,7 @@ let evar_of_binder holes = function
   try
     let h = List.nth holes (pred n) in
     h.hole_evar
-  with e when Errors.noncritical e ->
+  with e when CErrors.noncritical e ->
     errorlabstrm "" (str "No such binder.")
 
 let define_with_type sigma env ev c =
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 7ecc26ec..e9236b1d 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -6,6 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(** This file defines clausenv, which is a deprecated way to handle open terms
+    in the proof engine. Most of the API here is legacy except for the
+    evar-based clauses. *)
+
 open Names
 open Term
 open Environ
@@ -49,7 +53,6 @@ val refresh_undefined_univs : clausenv -> clausenv * Univ.universe_level_subst
 
 (** {6 linking of clenvs } *)
 
-val connect_clenv : Goal.goal sigma -> clausenv -> clausenv
 val clenv_fchain :
   ?with_univs:bool -> ?flags:unify_flags -> metavariable -> clausenv -> clausenv -> clausenv
 
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 8e922599..98b5bc8b 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -16,7 +16,7 @@ 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
@@ -59,6 +59,19 @@ let clenv_pose_dependent_evars with_evars clenv =
       (RefinerError (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 *)
+let check_tc evd =
+  let has_resolvable = ref false in
+  let check _ evi =
+    let res = Typeclasses.is_resolvable evi in
+    if res then
+      let () = has_resolvable := true in
+      Typeclasses.is_class_evar evd evi
+    else false
+  in
+  let has_typeclass = Evar.Map.exists check (Evd.undefined_map evd) in
+  (has_typeclass, !has_resolvable)
+
 let clenv_refine with_evars ?(with_classes=true) clenv =
   (** ppedrot: a Goal.enter here breaks things, because the tactic below may
       solve goals by side effects, while the compatibility layer keeps those
@@ -67,9 +80,16 @@ let clenv_refine with_evars ?(with_classes=true) clenv =
   let clenv = clenv_pose_dependent_evars with_evars clenv in
   let evd' =
     if with_classes then
-      let evd' = Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars
-        ~fail:(not with_evars) clenv.env clenv.evd
-      in Typeclasses.mark_unresolvables ~filter:Typeclasses.all_goals evd'
+      let (has_typeclass, has_resolvable) = check_tc clenv.evd in
+      let evd' =
+        if has_typeclass then
+          Typeclasses.resolve_typeclasses ~fast_path:false ~filter:Typeclasses.all_evars
+          ~fail:(not with_evars) clenv.env clenv.evd
+        else clenv.evd
+      in
+      if has_resolvable then
+        Typeclasses.mark_unresolvables ~filter:Typeclasses.all_goals evd'
+      else evd'
     else clenv.evd
   in
   let clenv = { clenv with evd = evd' } in
@@ -83,10 +103,10 @@ open Unification
 let dft = default_unify_flags
 
 let res_pf ?(with_evars=false) ?(with_classes=true) ?(flags=dft ()) clenv =
-  Proofview.Goal.enter begin fun gl ->
+  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
+  end }
 
 (* [unifyTerms] et [unify] ne semble pas gérer les Meta, en
    particulier ne semblent pas vérifier que des instances différentes
@@ -118,12 +138,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 begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     let env = Tacmach.New.pf_env gl in
-    let n = Tacmach.New.pf_nf_concl gl in
-    let evd = create_goal_evar_defs (Proofview.Goal.sigma gl) in
+    let n = Tacmach.New.pf_concl (Proofview.Goal.assume 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 Errors.noncritical e -> Proofview.tclZERO e
-  end
+    with e when CErrors.noncritical e -> Proofview.tclZERO e
+  end }
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index 00e74a24..aa091aec 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(** Legacy components of the previous proof engine. *)
+
 open Term
 open Clenv
 open Tacexpr
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 059ae54c..29cad063 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
+open CErrors
 open Util
 open Names
 open Evd
@@ -46,27 +46,16 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
   let sigma',typed_c =
     let flags = {
       Pretyping.use_typeclasses = true;
-      Pretyping.use_unif_heuristics = true;
+      Pretyping.solve_unification_constraints = true;
       Pretyping.use_hook = None;
       Pretyping.fail_evar = false;
       Pretyping.expand_evars = true } in
     try Pretyping.understand_ltac flags
       env sigma ltac_var (Pretyping.OfType evi.evar_concl) rawc
-    with e when Errors.noncritical e ->
+    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 " ++
-                 str (string_of_existential evk))
+                 pr_existential_key sigma evk ++ str ".")
   in
   define_and_solve_constraints evk typed_c env (evars_reset_evd sigma' sigma)
-
-(* vernac command Existential *)
-
-(* Main component of vernac command Existential *)
-let instantiate_pf_com evk com sigma =
-  let evi = Evd.find sigma evk 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 sigma' = w_refine (evk, evi) (ltac_vars, rawc) sigma in
-  sigma'
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 35a3e5d8..e3778e94 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -13,8 +13,3 @@ open Pretyping
 
 val w_refine : evar * evar_info ->
   glob_constr_ltac_closure -> evar_map -> evar_map
-
-val instantiate_pf_com :
-  Evd.evar -> Constrexpr.constr_expr -> Evd.evar_map -> Evd.evar_map
-
-(** the instantiate tactic was moved to [tactics/evar_tactics.ml] *)
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 1dd5be0e..111a947a 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -9,6 +9,8 @@
 open Util
 open Pp
 open Term
+open Sigma.Notations
+open Context.Named.Declaration
 
 (* This module implements the abstract interface to goals *)
 (* A general invariant of the module, is that a goal whose associated
@@ -70,10 +72,12 @@ module V82 = struct
 		Evd.evar_extra = extra }
     in
     let evi = Typeclasses.mark_unresolvable evi in
-    let (evars, evk) = Evarutil.new_pure_evar_full evars 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 ctxt = Environ.named_context_of_val hyps in
-    let inst = Array.map_of_list (fun (id, _, _) -> mkVar id) ctxt in
+    let inst = Array.map_of_list (mkVar % get_id) ctxt in
     let ev = Term.mkEvar (evk,inst) in
     (evk, ev, evars)
 
@@ -89,7 +93,10 @@ module V82 = struct
   (* Instantiates a goal with an open term, using name of goal for evk' *)
   let partial_solution_to sigma evk evk' c =
     let id = Evd.evar_ident evk sigma in
-    Evd.rename evk' id (partial_solution sigma evk c)
+    let sigma = partial_solution sigma evk c in
+    match id with
+    | None -> sigma
+    | Some id -> Evd.rename evk' id sigma
 
   (* Parts of the progress tactical *)
   let same_goal evars1 gl1 evars2 gl2 =
@@ -123,8 +130,10 @@ 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 (new_sigma, evk) = Evarutil.new_pure_evar_full Evd.empty new_evi in
-    { Evd.it = evk ; sigma = new_sigma; }
+    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
+    { Evd.it = evk ; sigma = sigma; }
 
   (* Used by the compatibility layer and typeclasses *)
   let nf_evar sigma gl =
@@ -139,7 +148,7 @@ module V82 = struct
     let env = env sigma gl in
     let genv = Global.env () in
     let is_proof_var decl =
-      try ignore (Environ.lookup_named (Util.pi1 decl) genv); false
+      try ignore (Environ.lookup_named (get_id decl) genv); false
       with Not_found -> true in
     Environ.fold_named_context_reverse (fun t decl ->
 					  if is_proof_var decl then
diff --git a/proofs/goal.mli b/proofs/goal.mli
index 6152826c..6a79c1f4 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -6,7 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* This module implements the abstract interface to goals *)
+(** This module implements the abstract interface to goals. Most of the code
+    here is useless and should be eventually removed. Consider using
+    {!Proofview.Goal} instead. *)
 
 type goal = Evar.t
 
@@ -67,7 +69,7 @@ module V82 : sig
   val same_goal : Evd.evar_map -> goal -> Evd.evar_map -> goal -> bool
 
  (* Used for congruence closure *)
-  val new_goal_with : Evd.evar_map -> goal -> Context.named_context -> goal Evd.sigma
+  val new_goal_with : Evd.evar_map -> goal -> Context.Named.t -> goal Evd.sigma
 
   (* Used by the compatibility layer and typeclasses *)
   val nf_evar : Evd.evar_map -> goal -> goal * Evd.evar_map
diff --git a/proofs/logic.ml b/proofs/logic.ml
index ed3a1df1..65497c80 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Names
 open Nameops
@@ -22,6 +22,7 @@ open Proof_type
 open Type_errors
 open Retyping
 open Misctypes
+open Context.Named.Declaration
 
 type refiner_error =
 
@@ -58,7 +59,7 @@ let is_unification_error = function
 | _ -> false
 
 let catchable_exception = function
-  | Errors.UserError _ | TypeError _
+  | CErrors.UserError _ | TypeError _
   | RefinerError _ | Indrec.RecursionSchemeError _
   | Nametab.GlobalizationError _
   (* reduction errors *)
@@ -76,10 +77,10 @@ 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 sign id f =
+let apply_to_hyp 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 id
     else sign
 
 let check_typability env sigma c =
@@ -95,12 +96,12 @@ let check_typability env sigma c =
    forces the user to give them in order). *)
 
 let clear_hyps env sigma ids sign cl =
-  let evdref = ref (Evd.create_goal_evar_defs sigma) in
+  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.create_goal_evar_defs sigma) in
+  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)
 
@@ -160,7 +161,8 @@ let reorder_context env sign ord =
       | _ ->
           (match ctxt_head with
             | [] -> error_no_such_hypothesis (List.hd ord)
-            | (x,_,_ as d) :: ctxt ->
+            | d :: ctxt ->
+                let x = 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
@@ -175,7 +177,8 @@ let reorder_val_context env sign ord =
 
 
 
-let check_decl_position env sign (x,_,_ as d) =
+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
   if Id.List.mem x deps then
@@ -200,16 +203,17 @@ let move_location_eq m1 m2 = match m1, m2 with
 
 let rec get_hyp_after h = function
   | [] -> error_no_such_hypothesis h
-  | (hyp,_,_) :: right ->
-      if Id.equal hyp h then
-	match right with (id,_,_)::_ -> MoveBefore id | [] -> MoveFirst
+  | 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 rec splitrec left toleft = function
     | [] -> error_no_such_hypothesis hfrom
-    | (hyp,c,typ) as d :: right ->
+    | d :: right ->
+        let hyp,_,typ = to_tuple d in
       	if Id.equal hyp hfrom then
 	  (left,right,d, toleft || move_location_eq hto MoveLast)
       	else
@@ -227,27 +231,28 @@ let hyp_of_move_location = function
   | MoveBefore id -> id
   | _ -> assert false
 
-let move_hyp toleft (left,(idfrom,_,_ as declfrom),right) hto =
+let move_hyp toleft (left,declfrom,right) hto =
   let env = Global.env() in
-  let test_dep (hyp,c,typ as d) (hyp2,c,typ2 as d2) =
+  let test_dep d d2 =
     if toleft
-    then occur_var_in_decl env hyp2 d
-    else occur_var_in_decl env hyp d2
+    then occur_var_in_decl env (get_id d2) d
+    else occur_var_in_decl env (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);
 	List.rev first @ List.rev middle
-    | (hyp,_,_) :: _ as right when move_location_eq hto (MoveBefore hyp) ->
+    | d :: _ as right when move_location_eq hto (MoveBefore (get_id d)) ->
 	List.rev first @ List.rev middle @ right
-    | (hyp,_,_) as d :: right ->
+    | d :: right ->
+        let hyp = 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 idfrom ++
+	      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 ".")
@@ -271,6 +276,11 @@ let move_hyp toleft (left,(idfrom,_,_ as 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 (left,right,declfrom,toleft) =
+    split_sign hfrom hto (named_context_of_val sign) in
+  move_hyp toleft (left,declfrom,right) hto
+
 (**********************************************************************)
 
 
@@ -458,7 +468,7 @@ and mk_hdgoals sigma goal goalacc trm =
 
 and mk_arggoals sigma goal goalacc funty allargs =
   let foldmap (goalacc, funty, sigma) harg =
-    let t = whd_betadeltaiota (Goal.V82.env sigma goal) sigma funty in
+    let t = whd_all (Goal.V82.env sigma goal) sigma funty in
     let rec collapse t = match kind_of_term t with
     | LetIn (_, c1, _, b) -> collapse (subst1 c1 b)
     | _ -> t
@@ -483,12 +493,14 @@ and mk_casegoals sigma goal goalacc p c =
   (acc'',lbrty,conclty,sigma,p',c')
 
 
-let convert_hyp check sign sigma (id,b,bt as d) =
+let convert_hyp check sign sigma d =
+  let id,b,bt = to_tuple d in
   let env = Global.env() in
   let reorder = ref [] in
   let sign' =
-    apply_to_hyp sign id
-      (fun _ (_,c,ct) _ ->
+    apply_to_hyp check sign id
+      (fun _ d' _ ->
+        let _,c,ct = to_tuple d' in
         let env = Global.env_of_context sign in
         if check && not (is_conv env sigma bt ct) then
 	  errorlabstrm "Logic.convert_hyp"
@@ -522,126 +534,23 @@ let prim_refiner r sigma goal =
 	  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 ([],(id,None,t),named_context_of_val sign)
+	    move_hyp false ([], LocalAssum (id,t),named_context_of_val sign)
 	      nexthyp,
 	      t,cl,sigma
 	  else
-            (if !check && mem_named_context id (named_context_of_val sign) then
+            (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 (id,None,t) sign,t,cl,sigma) in
+	     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.mkApp (mkNamedLambda id t ev2 , [| ev1 |]) 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)
 
-    | FixRule (f,n,rest,j) ->
-     	let rec check_ind env k cl =
-          match kind_of_term (strip_outer_cast cl) with
-            | Prod (na,c1,b) ->
-            	if Int.equal k 1 then
-		  try
-		    fst (find_inductive env sigma c1)
-		  with Not_found ->
-		    error "Cannot do a fixpoint on a non inductive type."
-            	else
-		  check_ind (push_rel (na,None,c1) env) (k-1) b
-            | _ -> error "Not enough products."
-	in
-	let ((sp,_),u) = check_ind env n cl in
-	let firsts,lasts = List.chop j rest in
-	let all = firsts@(f,n,cl)::lasts in
-     	let rec mk_sign sign = function
-	  | (f,n,ar)::oth ->
-	      let ((sp',_),u')  = check_ind env n ar in
-	      if not (eq_mind sp sp') then
-		error "Fixpoints should be on the same mutual inductive declaration.";
-	      if !check && mem_named_context f (named_context_of_val sign) then
-		errorlabstrm "Logic.prim_refiner"
-		  (str "Name " ++ pr_id f ++ str " already used in the environment");
-	      mk_sign (push_named_context_val (f,None,ar) sign) oth
-	  | [] ->
-	      Evd.Monad.List.map (fun (_,_,c) sigma ->
-                let gl,ev,sig' =
-                  Goal.V82.mk_goal sigma sign c (Goal.V82.extra sigma goal) in
-                (gl,ev),sig')
-              all sigma
-	in
-	let (gls_evs,sigma) =  mk_sign sign all in
-	let (gls,evs) = List.split gls_evs in
-	let ids = List.map pi1 all in
-	let evs = List.map (Vars.subst_vars (List.rev ids)) evs in
-	let indxs = Array.of_list (List.map (fun n -> n-1) (List.map pi2 all)) in
-	let funnames = Array.of_list (List.map (fun i -> Name i) ids) in
-	let typarray = Array.of_list (List.map pi3 all) in
-	let bodies = Array.of_list evs in
-	let oterm = Term.mkFix ((indxs,0),(funnames,typarray,bodies)) in
-	let sigma = Goal.V82.partial_solution sigma goal oterm in
-	(gls,sigma)
-
-    | Cofix (f,others,j) ->
-     	let rec check_is_coind env cl =
-	  let b = whd_betadeltaiota env sigma cl in
-          match kind_of_term b with
-            | Prod (na,c1,b) -> check_is_coind (push_rel (na,None,c1) env) b
-            | _ ->
-		try
-		  let _ = find_coinductive env sigma b in ()
-                with Not_found ->
-		  error "All methods must construct elements in coinductive types."
-	in
-	let firsts,lasts = List.chop j others in
-	let all = firsts@(f,cl)::lasts in
-     	List.iter (fun (_,c) -> check_is_coind env c) all;
-        let rec mk_sign sign = function
-          | (f,ar)::oth ->
-	      (try
-                (let _ = lookup_named_val f sign in
-                error "Name already used in the environment.")
-              with
-              |	Not_found ->
-                  mk_sign (push_named_context_val (f,None,ar) sign) oth)
-	  | [] -> 
-              Evd.Monad.List.map (fun (_,c) sigma ->
-                let gl,ev,sigma =
-                  Goal.V82.mk_goal sigma sign c (Goal.V82.extra sigma goal) in
-                (gl,ev),sigma)
-              all sigma
-     	in
-	let (gls_evs,sigma) =  mk_sign sign all in
-	let (gls,evs) = List.split gls_evs in
-	let (ids,types) = List.split all in
-	let evs = List.map (Vars.subst_vars (List.rev ids)) evs in
-	let funnames = Array.of_list (List.map (fun i -> Name i) ids) in
-	let typarray = Array.of_list types in
-	let bodies = Array.of_list evs in
-	let oterm = Term.mkCoFix (0,(funnames,typarray,bodies)) in
-	let sigma = Goal.V82.partial_solution sigma goal oterm in
-        (gls,sigma)
-
     | Refine c ->
 	check_meta_variables 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
 	  (sgl, sigma)
-
-    (* And now the structural rules *)
-    | Thin ids ->
-        let ids = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty ids in
-	let (hyps,concl,nsigma) = clear_hyps env sigma ids sign cl in
-	let (gl,ev,sigma) =
-	  Goal.V82.mk_goal nsigma hyps concl (Goal.V82.extra nsigma goal)
-	in
-	let sigma = Goal.V82.partial_solution_to sigma goal gl ev in
-	  ([gl], sigma)
-
-    | Move (hfrom, hto) ->
-  	let (left,right,declfrom,toleft) =
-	  split_sign hfrom hto (named_context_of_val sign) in
-  	let hyps' =
-	  move_hyp toleft (left,declfrom,right) hto in
-	let (gl,ev,sigma) = mk_goal hyps' cl in
-	let sigma = Goal.V82.partial_solution_to sigma goal gl ev in
-  	  ([gl], sigma)
diff --git a/proofs/logic.mli b/proofs/logic.mli
index ed99d3a3..0dba9ef1 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(** Legacy proof engine. Do not use in newly written code. *)
+
 open Names
 open Term
 open Evd
@@ -53,4 +55,7 @@ exception RefinerError of refiner_error
 val catchable_exception : exn -> bool
 
 val convert_hyp : bool -> Environ.named_context_val -> evar_map ->
-  Context.named_declaration -> Environ.named_context_val
+  Context.Named.Declaration.t -> Environ.named_context_val
+
+val move_hyp_in_named_context : Id.t -> Id.t Misctypes.move_location ->
+  Environ.named_context_val -> Environ.named_context_val
diff --git a/proofs/logic_monad.ml b/proofs/logic_monad.ml
deleted file mode 100644
index 68efa71e..00000000
--- a/proofs/logic_monad.ml
+++ /dev/null
@@ -1,321 +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        *)
-(************************************************************************)
-
-(** This file defines the low-level monadic operations used by the
-    tactic monad. The monad is divided into two layers: a non-logical
-    layer which consists in operations which will not (or cannot) be
-    backtracked in case of failure (input/output or persistent state)
-    and a logical layer which handles backtracking, proof
-    manipulation, and any other effect which needs to backtrack. *)
-
-
-(** {6 Exceptions} *)
-
-
-(** To help distinguish between exceptions raised by the IO monad from
-    the one used natively by Coq, the former are wrapped in
-    [Exception].  It is only used internally so that [catch] blocks of
-    the IO monad would only catch exceptions raised by the [raise]
-    function of the IO monad, and not for instance, by system
-    interrupts. Also used in [Proofview] to avoid capturing exception
-    from the IO monad ([Proofview] catches errors in its compatibility
-    layer, and when lifting goal-level expressions). *)
-exception Exception of exn
-(** This exception is used to signal abortion in [timeout] functions. *)
-exception Timeout
-(** This exception is used by the tactics to signal failure by lack of
-    successes, rather than some other exceptions (like system
-    interrupts). *)
-exception TacticFailure of exn
-
-let _ = Errors.register_handler begin function
-  | Timeout -> Errors.errorlabstrm "Some timeout function" (Pp.str"Timeout!")
-  | Exception e -> Errors.print e
-  | TacticFailure e -> Errors.print e
-  | _ -> Pervasives.raise Errors.Unhandled
-end
-
-(** {6 Non-logical layer} *)
-
-(** The non-logical monad is a simple [unit -> 'a] (i/o) monad. The
-    operations are simple wrappers around corresponding usual
-    operations and require little documentation. *)
-module NonLogical =
-struct
-
-  (* The functions in this module follow the pattern that they are
-     defined with the form [(); fun ()->...]. This is an optimisation
-     which signals to the compiler that the function is usually partially
-     applied up to the [();]. Without this annotation, partial
-     applications can be significantly slower.
-
-     Documentation of this behaviour can be found at:
-     https://ocaml.janestreet.com/?q=node/30 *)
-
-  include Monad.Make(struct
-    type 'a t = unit -> 'a
-
-    let return a = (); fun () -> a
-    let (>>=) a k = (); fun () -> k (a ()) ()
-    let (>>) a k = (); fun () -> a (); k ()
-    let map f a = (); fun () -> f (a ())
-  end)
-
-  type 'a ref = 'a Pervasives.ref
-
-  let ignore a = (); fun () -> ignore (a ())
-
-  let ref a = (); fun () -> Pervasives.ref a
-
-  (** [Pervasives.(:=)] *)
-  let (:=) r a = (); fun () -> r := a
-
-  (** [Pervasives.(!)] *)
-  let (!) = fun r -> (); fun () -> ! r
-
-  (** [Pervasives.raise]. Except that exceptions are wrapped with
-      {!Exception}. *)
-  let raise ?info = fun e -> (); fun () -> Exninfo.raise ?info (Exception e)
-
-  (** [try ... with ...] but restricted to {!Exception}. *)
-  let catch = fun s h -> ();
-    fun () -> try s ()
-      with Exception e as src ->
-        let (src, info) = Errors.push src in
-        h (e, info) ()
-
-  let read_line = fun () -> try Pervasives.read_line () with e ->
-    let (e, info) = Errors.push e in raise ~info e ()
-
-  let print_char = fun c -> (); fun () -> print_char c
-
-  let timeout = fun n t -> (); fun () ->
-    Control.timeout n t (Exception Timeout)
-
-  let make f = (); fun () ->
-    try f ()
-    with e when Errors.noncritical e ->
-      let (e, info) = Errors.push e in
-      Util.iraise (Exception e, info)
-
-  (** Use the current logger. The buffer is also flushed. *)
-  let print_debug s = make (fun _ -> Pp.msg_info s;Pp.pp_flush ())
-  let print_info s =  make (fun _ -> Pp.msg_info s;Pp.pp_flush ())
-  let print_warning s =  make (fun _ -> Pp.msg_warning s;Pp.pp_flush ())
-  let print_error s =  make (fun _ -> Pp.msg_error s;Pp.pp_flush ())
-  let print_notice s = make (fun _ -> Pp.msg_notice s;Pp.pp_flush ())
-
-  let run = fun x ->
-    try x () with Exception e as src ->
-      let (src, info) = Errors.push src in
-      Util.iraise (e, info)
-end
-
-(** {6 Logical layer} *)
-
-(** The logical monad is a backtracking monad on top of which is
-    layered a state monad (which is used to implement all of read/write,
-    read only, and write only effects). The state monad being layered on
-    top of the backtracking monad makes it so that the state is
-    backtracked on failure.
-
-    Backtracking differs from regular exception in that, writing (+)
-    for exception catching and (>>=) for bind, we require the
-    following extra distributivity laws:
-
-    x+(y+z) = (x+y)+z
-
-    zero+x = x
-
-    x+zero = x
-
-    (x+y)>>=k = (x>>=k)+(y>>=k) *)
-
-(** A view type for the logical monad, which is a form of list, hence
-    we can decompose it with as a list. *)
-type ('a, 'b) list_view =
-  | Nil of Exninfo.iexn
-  | Cons of 'a * 'b
-
-module type Param = sig
-
-  (** Read only *)
-  type e
-
-  (** Write only *)
-  type w
-
-  (** [w] must be a monoid *)
-  val wunit : w
-  val wprod : w -> w -> w
-
-  (** Read-write *)
-  type s
-
-  (** Update-only. Essentially a writer on [u->u]. *)
-  type u
-
-  (** [u] must be pointed. *)
-  val uunit : u
-
-end
-
-
-module Logical (P:Param) =
-struct
-
-  (** All three of environment, writer and state are coded as a single
-      state-passing-style monad.*)
-  type state = {
-    rstate : P.e;
-    ustate : P.u;
-    wstate : P.w;
-    sstate : P.s;
-  }
-
-  (** Double-continuation backtracking monads are reasonable folklore
-      for "search" implementations (including the Tac interactive
-      prover's tactics). Yet it's quite hard to wrap your head around
-      these.  I recommand reading a few times the "Backtracking,
-      Interleaving, and Terminating Monad Transformers" paper by
-      O. Kiselyov, C. Shan, D. Friedman, and A. Sabry.  The peculiar
-      shape of the monadic type is reminiscent of that of the
-      continuation monad transformer.
-
-      The paper also contains the rationale for the [split] abstraction.
-
-      An explanation of how to derive such a monad from mathematical
-      principles can be found in "Kan Extensions for Program
-      Optimisation" by Ralf Hinze.
-
-      A somewhat concrete view is that the type ['a iolist] is, in fact
-      the impredicative encoding of the following stream type:
-
-      [type 'a _iolist' = Nil of exn | Cons of 'a*'a iolist'
-      and 'a iolist = 'a _iolist NonLogical.t]
-
-      Using impredicative encoding avoids intermediate allocation and
-      is, empirically, very efficient in Ocaml. It also has the
-      practical benefit that the monadic operation are independent of
-      the underlying monad, which simplifies the code and side-steps
-      the limited inlining of Ocaml.
-
-      In that vision, [bind] is simply [concat_map] (though the cps
-      version is significantly simpler), [plus] is concatenation, and
-      [split] is pattern-matching. *)
-  type rich_exn = Exninfo.iexn
-
-  type 'a iolist =
-    { iolist : 'r. state -> (rich_exn -> 'r NonLogical.t) ->
-      ('a -> state -> (rich_exn -> 'r NonLogical.t) -> 'r NonLogical.t) ->
-      'r NonLogical.t }
-
-  include Monad.Make(struct
-
-    type 'a t = 'a iolist
-
-    let return x =
-      { iolist = fun s nil cons -> cons x s nil }
-
-    let (>>=) m f =
-      { iolist = fun s nil cons ->
-        m.iolist s nil (fun x s next -> (f x).iolist s next cons) }
-
-    let (>>) m f =
-      { iolist = fun s nil cons ->
-        m.iolist s nil (fun () s next -> f.iolist s next cons) }
-
-    let map f m =
-      { iolist = fun s nil cons -> m.iolist s nil (fun x s next -> cons (f x) s next) }
-
-  end)
-
-  let zero e =
-    { iolist = fun _ nil cons -> nil e }
-
-  let plus m1 m2 =
-    { iolist = fun s nil cons -> m1.iolist s (fun e -> (m2 e).iolist s nil cons) cons }
-
-  let ignore m =
-    { iolist = fun s nil cons -> m.iolist s nil (fun _ s next -> cons () s next) }
-
-  let lift m =
-    { iolist = fun s nil cons -> NonLogical.(m >>= fun x -> cons x s nil) }
-
-  (** State related *)
-
-  let get =
-    { iolist = fun s nil cons -> cons s.sstate s nil }
-
-  let set (sstate : P.s) =
-    { iolist = fun s nil cons -> cons () { s with sstate } nil }
-
-  let modify (f : P.s -> P.s) =
-    { iolist = fun s nil cons -> cons () { s with sstate = f s.sstate } nil }
-
-  let current =
-    { iolist = fun s nil cons -> cons s.rstate s nil }
-
-  let local e m =
-    { iolist = fun s nil cons ->
-      m.iolist { s with rstate = e } nil
-        (fun x s' next -> cons x {s' with rstate = s.rstate} next) }
-
-  let put w =
-    { iolist = fun s nil cons -> cons () { s with wstate = P.wprod s.wstate w } nil }
-
-  let update (f : P.u -> P.u) =
-    { iolist = fun s nil cons -> cons () { s with ustate = f s.ustate } nil }
-
-  (** List observation *)
-
-  let once m =
-    { iolist = fun s nil cons -> m.iolist s nil (fun x s _ -> cons x s nil) }
-
-  let break f m =
-    { iolist = fun s nil cons ->
-      m.iolist s nil (fun x s next -> cons x s (fun e -> match f e with None -> next e | Some e -> nil e))
-    }
-
-  (** For [reflect] and [split] see the "Backtracking, Interleaving,
-      and Terminating Monad Transformers" paper.  *)
-  type 'a reified = ('a, rich_exn -> 'a reified) list_view NonLogical.t
-
-  let rec reflect (m : ('a * state) reified) : 'a iolist =
-    { iolist = fun s0 nil cons ->
-      let next = function
-      | Nil e -> nil e
-      | Cons ((x, s), l) -> cons x s (fun e -> (reflect (l e)).iolist s0 nil cons)
-      in
-      NonLogical.(m >>= next)
-    }
-
-  let split m : ('a, rich_exn -> 'a t) list_view t =
-    let rnil e = NonLogical.return (Nil e) in
-    let rcons p s l = NonLogical.return (Cons ((p, s), l)) in
-    { iolist = fun s nil cons ->
-      let open NonLogical in
-      m.iolist s rnil rcons >>= begin function
-      | Nil e -> cons (Nil e) s nil
-      | Cons ((x, s), l) ->
-        let l e = reflect (l e) in
-        cons (Cons (x, l)) s nil
-      end }
-
-  let run m r s =
-    let s = { wstate = P.wunit; ustate = P.uunit; rstate = r; sstate = s } in
-    let rnil e = NonLogical.return (Nil e) in
-    let rcons x s l =
-      let p = (x, s.sstate, s.wstate, s.ustate) in
-      NonLogical.return (Cons (p, l))
-    in
-    m.iolist s rnil rcons
-
-  let repr x = x
-
- end
diff --git a/proofs/logic_monad.mli b/proofs/logic_monad.mli
deleted file mode 100644
index 96655d53..00000000
--- a/proofs/logic_monad.mli
+++ /dev/null
@@ -1,162 +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        *)
-(************************************************************************)
-
-(** This file defines the low-level monadic operations used by the
-    tactic monad. The monad is divided into two layers: a non-logical
-    layer which consists in operations which will not (or cannot) be
-    backtracked in case of failure (input/output or persistent state)
-    and a logical layer which handles backtracking, proof
-    manipulation, and any other effect which needs to backtrack. *)
-
-
-(** {6 Exceptions} *)
-
-
-(** To help distinguish between exceptions raised by the IO monad from
-    the one used natively by Coq, the former are wrapped in
-    [Exception].  It is only used internally so that [catch] blocks of
-    the IO monad would only catch exceptions raised by the [raise]
-    function of the IO monad, and not for instance, by system
-    interrupts. Also used in [Proofview] to avoid capturing exception
-    from the IO monad ([Proofview] catches errors in its compatibility
-    layer, and when lifting goal-level expressions). *)
-exception Exception of exn
-(** This exception is used to signal abortion in [timeout] functions. *)
-exception Timeout
-(** This exception is used by the tactics to signal failure by lack of
-    successes, rather than some other exceptions (like system
-    interrupts). *)
-exception TacticFailure of exn
-
-
-(** {6 Non-logical layer} *)
-
-(** The non-logical monad is a simple [unit -> 'a] (i/o) monad. The
-    operations are simple wrappers around corresponding usual
-    operations and require little documentation. *)
-module NonLogical : sig
-
-  include Monad.S
-
-  val ignore : 'a t -> unit t
-
-  type 'a ref
-
-  val ref : 'a -> 'a ref t
-  (** [Pervasives.(:=)] *)
-  val (:=) : 'a ref -> 'a -> unit t
-  (** [Pervasives.(!)] *)
-  val (!) : 'a ref -> 'a t
-
-  val read_line : string t
-  val print_char : char -> unit t
-
-  (** Loggers. The buffer is also flushed. *)
-  val print_debug : Pp.std_ppcmds -> unit t
-  val print_warning : Pp.std_ppcmds -> unit t
-  val print_notice : Pp.std_ppcmds -> unit t
-  val print_info : Pp.std_ppcmds -> unit t
-  val print_error : Pp.std_ppcmds -> unit t
-
-  (** [Pervasives.raise]. Except that exceptions are wrapped with
-      {!Exception}. *)
-  val raise : ?info:Exninfo.info -> exn -> 'a t
-  (** [try ... with ...] but restricted to {!Exception}. *)
-  val catch : 'a t -> (Exninfo.iexn -> 'a t) -> 'a t
-  val timeout : int -> 'a t -> 'a t
-
-  (** Construct a monadified side-effect. Exceptions raised by the argument are
-      wrapped with {!Exception}. *)
-  val make : (unit -> 'a) -> 'a t
-
-  (** [run] performs effects. *)
-  val run : 'a t -> 'a
-
-end
-
-
-(** {6 Logical layer} *)
-
-(** The logical monad is a backtracking monad on top of which is
-    layered a state monad (which is used to implement all of read/write,
-    read only, and write only effects). The state monad being layered on
-    top of the backtracking monad makes it so that the state is
-    backtracked on failure.
-
-    Backtracking differs from regular exception in that, writing (+)
-    for exception catching and (>>=) for bind, we require the
-    following extra distributivity laws:
-
-    x+(y+z) = (x+y)+z
-
-    zero+x = x
-
-    x+zero = x
-
-    (x+y)>>=k = (x>>=k)+(y>>=k) *)
-
-(** A view type for the logical monad, which is a form of list, hence
-    we can decompose it with as a list. *)
-type ('a, 'b) list_view =
-| Nil of Exninfo.iexn
-| Cons of 'a * 'b
-
-(** The monad is parametrised in the types of state, environment and
-    writer. *)
-module type Param = sig
-
-  (** Read only *)
-  type e
-
-  (** Write only *)
-  type w
-
-  (** [w] must be a monoid *)
-  val wunit : w
-  val wprod : w -> w -> w
-
-  (** Read-write *)
-  type s
-
-  (** Update-only. Essentially a writer on [u->u]. *)
-  type u
-
-  (** [u] must be pointed. *)
-  val uunit : u
-
-end
-
-module Logical (P:Param) : sig
-
-  include Monad.S
-
-  val ignore : 'a t -> unit t
-
-  val set : P.s -> unit t
-  val get : P.s t
-  val modify : (P.s -> P.s) -> unit t
-  val put : P.w -> unit t
-  val current : P.e t
-  val local : P.e -> 'a t -> 'a t
-  val update : (P.u -> P.u) -> unit t
-
-  val zero : Exninfo.iexn -> 'a t
-  val plus : 'a t -> (Exninfo.iexn -> 'a t) -> 'a t
-  val split : 'a t -> (('a,(Exninfo.iexn->'a t)) list_view) t
-  val once : 'a t -> 'a t
-  val break : (Exninfo.iexn -> Exninfo.iexn option) -> 'a t -> 'a t
-
-  val lift : 'a NonLogical.t -> 'a t
-
-  type 'a reified
-
-  val repr : 'a reified -> ('a, Exninfo.iexn -> 'a reified) list_view NonLogical.t
-
-  val run : 'a t -> P.e -> P.s -> ('a * P.s * P.w * P.u) reified
-
-end
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index b635cc96..eddbf72a 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -13,6 +13,17 @@ open Entries
 open Environ
 open Evd
 
+let use_unification_heuristics_ref = ref true
+let _ = Goptions.declare_bool_option {
+  Goptions.optsync = true; Goptions.optdepr = false;
+  Goptions.optname = "Solve unification constraints at every \".\"";
+  Goptions.optkey = ["Solve";"Unification";"Constraints"];
+  Goptions.optread = (fun () -> !use_unification_heuristics_ref);
+  Goptions.optwrite = (fun a -> use_unification_heuristics_ref:=a);
+}
+
+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
 
@@ -39,7 +50,7 @@ let cook_this_proof p =
   match p with
   | { Proof_global.id;entries=[constr];persistence;universes } ->
       (id,(constr,universes,persistence))
-  | _ -> Errors.anomaly ~label:"Pfedit.cook_proof" (Pp.str "more than one proof term.")
+  | _ -> CErrors.anomaly ~label:"Pfedit.cook_proof" (Pp.str "more than one proof term.")
 
 let cook_proof () =
   cook_this_proof (fst
@@ -59,9 +70,9 @@ let get_universe_binders () =
   Proof_global.get_universe_binders ()
 
 exception NoSuchGoal
-let _ = Errors.register_handler begin function
-  | NoSuchGoal -> Errors.error "No such goal."
-  | _ -> raise Errors.Unhandled
+let _ = CErrors.register_handler begin function
+  | NoSuchGoal -> CErrors.error "No such goal."
+  | _ -> raise CErrors.Unhandled
 end
 let get_nth_V82_goal i =
   let p = Proof_global.give_me_the_proof () in
@@ -71,26 +82,38 @@ let get_nth_V82_goal i =
   with Failure _ -> raise NoSuchGoal
     
 let get_goal_context_gen i =
-  try
-let { it=goal ; sigma=sigma; } =  get_nth_V82_goal i in
-(sigma, Refiner.pf_env { it=goal ; sigma=sigma; })
-  with Proof_global.NoCurrentProof -> Errors.error "No focused proof."
+  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 NoSuchGoal -> Errors.error "No such goal."
+  with Proof_global.NoCurrentProof -> CErrors.error "No focused proof."
+     | NoSuchGoal -> CErrors.error "No such goal."
 
 let get_current_goal_context () =
   try get_goal_context_gen 1
-  with NoSuchGoal ->
+  with Proof_global.NoCurrentProof -> CErrors.error "No focused proof."
+     | NoSuchGoal -> 
     (* spiwack: returning empty evar_map, since if there is no goal, under focus,
         there is no accessible evar either *)
-    (Evd.empty, Global.env ())
+    let env = Global.env () in
+    (Evd.from_env env, env)
+
+let get_current_context () =
+  try get_goal_context_gen 1
+  with Proof_global.NoCurrentProof ->
+    let env = Global.env () in
+    (Evd.from_env env, env)
+     | NoSuchGoal ->
+        (* No more focused goals ? *)
+        let p = get_pftreestate () 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
-    | _ -> Errors.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 
@@ -103,24 +126,28 @@ let solve ?with_end_tac gi info_lvl tac pr =
     in
     let tac = match gi with
       | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i tac
+      | Vernacexpr.SelectList l -> Proofview.tclFOCUSLIST l tac
       | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id tac
       | Vernacexpr.SelectAll -> tac
-      | Vernacexpr.SelectAllParallel ->
-          Errors.anomaly(str"SelectAllParallel not handled by Stm")
+    in
+    let tac =
+      if use_unification_heuristics () then
+        Proofview.tclTHEN tac Refine.solve_constraints
+      else tac
     in
     let (p,(status,info)) = Proof.run_tactic (Global.env ()) tac pr in
     let () =
       match info_lvl with
       | None -> ()
-      | Some i -> Pp.msg_info (hov 0 (Proofview.Trace.pr_info ~lvl:i info))
+      | Some i -> Feedback.msg_info (hov 0 (Proofview.Trace.pr_info ~lvl:i info))
     in
     (p,status)
   with
-    | Proof_global.NoCurrentProof  -> Errors.error "No focused proof"
+    | 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
-	                            Errors.errorlabstrm "" msg
+	                            CErrors.errorlabstrm "" msg
         | _ -> assert false
 
 let by tac = Proof_global.with_current_proof (fun _ -> solve (Vernacexpr.SelectNth 1) None tac)
@@ -138,22 +165,24 @@ let next = let n = ref 0 in fun () -> incr n; !n
 
 let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theorem) typ tac =
   let evd = Evd.from_ctx ctx in
-  start_proof id goal_kind evd sign typ (fun _ -> ());
+  let terminator = Proof_global.make_terminator (fun _ -> ()) in
+  start_proof id goal_kind evd sign typ terminator;
   try
     let status = by tac in
     let _,(const,univs,_) = cook_proof () in
     delete_current_proof ();
     const, status, fst univs
   with reraise ->
-    let reraise = Errors.push reraise in
+    let reraise = CErrors.push reraise in
     delete_current_proof ();
     iraise reraise
 
-let build_by_tactic ?(side_eff=true) env ctx ?(poly=false) typ tac =
+let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac =
   let id = Id.of_string ("temporary_proof"^string_of_int (next())) in
   let sign = val_of_named_context (named_context env) in
   let gk = Global, poly, Proof Theorem in
-  let ce, status, univs = build_constant_by_tactic id ctx sign ~goal_kind:gk typ tac in
+  let ce, status, univs =
+    build_constant_by_tactic id sigma sign ~goal_kind:gk typ tac in
   let ce =
     if side_eff then Safe_typing.inline_private_constants_in_definition_entry env ce
     else { ce with
@@ -176,7 +205,7 @@ let refine_by_tactic env sigma ty tac =
     try Proof.run_tactic env tac prf
     with Logic_monad.TacticFailure e as src ->
       (** Catch the inner error of the monad tactic *)
-      let (_, info) = Errors.push src in
+      let (_, info) = CErrors.push src in
       iraise (e, info)
   in
   (** Plug back the retrieved sigma *)
@@ -203,7 +232,7 @@ let refine_by_tactic env sigma ty tac =
 (* Support for resolution of evars in tactic interpretation, including
    resolution by application of tactics *)
 
-let implicit_tactic = ref None
+let implicit_tactic = Summary.ref None ~name:"implicit-tactic"
 
 let declare_implicit_tactic tac = implicit_tactic := Some tac
 
@@ -214,12 +243,15 @@ let solve_by_implicit_tactic env sigma evk =
   match (!implicit_tactic, snd (evar_source evk sigma)) with
   | Some tac, (Evar_kinds.ImplicitArg _ | Evar_kinds.QuestionMark _)
       when
-	Context.named_context_equal (Environ.named_context_of_val evi.evar_hyps)
+	Context.Named.equal (Environ.named_context_of_val evi.evar_hyps)
 	(Environ.named_context env) ->
-      let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (Errors.UserError ("",Pp.str"Proof is not complete."))) []) in
+      let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (CErrors.UserError ("",Pp.str"Proof is not complete."))) []) in
       (try
-        let (ans, _, _) = 
-	  build_by_tactic env (Evd.evar_universe_context sigma) evi.evar_concl tac in
-        ans
+        let c = Evarutil.nf_evars_universes sigma evi.evar_concl 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
        with e when Logic.catchable_exception e -> raise Exit)
   | _ -> raise Exit
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index cd899201..ea604e08 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(** Global proof state. A quite redundant wrapper on {!Proof_global}. *)
+
 open Loc
 open Names
 open Term
@@ -93,6 +95,14 @@ val get_goal_context : int -> Evd.evar_map * env
 
 val get_current_goal_context : unit -> Evd.evar_map * env
 
+(** [get_current_context ()] returns the context of the
+  current focused goal. If there is no focused goal but there
+  is a proof in progress, it returns the corresponding evar_map.
+  If there is no pending proof then it returns the current global
+  environment and empty evar_map. *)
+
+val get_current_context : unit -> Evd.evar_map * env
+
 (** [current_proof_statement] *)
 
 val current_proof_statement :
@@ -157,7 +167,8 @@ val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> unit
 val build_constant_by_tactic :
   Id.t -> Evd.evar_universe_context -> named_context_val -> ?goal_kind:goal_kind ->
   types -> unit Proofview.tactic -> 
-  Safe_typing.private_constants Entries.definition_entry * bool * Evd.evar_universe_context
+  Safe_typing.private_constants Entries.definition_entry * bool *
+    Evd.evar_universe_context
 
 val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?poly:polymorphic ->
   types -> unit Proofview.tactic -> 
@@ -179,5 +190,4 @@ val declare_implicit_tactic : unit Proofview.tactic -> unit
 val clear_implicit_tactic : unit -> unit
 
 (* Raise Exit if cannot solve *)
-(* FIXME: interface: it may incur some new universes etc... *)
-val solve_by_implicit_tactic : env -> Evd.evar_map -> Evd.evar -> constr
+val solve_by_implicit_tactic : env -> Evd.evar_map -> Evd.evar -> Evd.evar_map * constr
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 0489305a..5c963d53 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -64,17 +64,17 @@ exception NoSuchGoals of int * int
 
 exception FullyUnfocused
 
-let _ = Errors.register_handler begin function
+let _ = CErrors.register_handler begin function
   | CannotUnfocusThisWay ->
-    Errors.error "This proof is focused, but cannot be unfocused this way"
+    CErrors.error "This proof is focused, but cannot be unfocused this way"
   | NoSuchGoals (i,j) when Int.equal i j ->
-      Errors.errorlabstrm "Focus" Pp.(str"No such goal (" ++ int i ++ str").")
+      CErrors.errorlabstrm "Focus" Pp.(str"No such goal (" ++ int i ++ str").")
   | NoSuchGoals (i,j) ->
-      Errors.errorlabstrm "Focus" Pp.(
+      CErrors.errorlabstrm "Focus" Pp.(
         str"Not every goal in range ["++ int i ++ str","++int j++str"] exist."
       )
-  | FullyUnfocused -> Errors.error "The proof is not focused"
-  | _ -> raise Errors.Unhandled
+  | FullyUnfocused -> CErrors.error "The proof is not focused"
+  | _ -> raise CErrors.Unhandled
 end
 
 let check_cond_kind c k =
@@ -300,12 +300,12 @@ exception UnfinishedProof
 exception HasShelvedGoals
 exception HasGivenUpGoals
 exception HasUnresolvedEvar
-let _ = Errors.register_handler begin function
-  | UnfinishedProof -> Errors.error "Some goals have not been solved."
-  | HasShelvedGoals -> Errors.error "Some goals have been left on the shelf."
-  | HasGivenUpGoals -> Errors.error "Some goals have been given up."
-  | HasUnresolvedEvar -> Errors.error "Some existential variables are uninstantiated."
-  | _ -> raise Errors.Unhandled
+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."
+  | _ -> raise CErrors.Unhandled
 end
 
 let return p =
@@ -334,21 +334,30 @@ let compact p =
 (*** Tactics ***)
 
 let run_tactic env tac pr =
+  let open Proofview.Notations in
   let sp = pr.proofview in
-  let (_,tacticced_proofview,(status,to_shelve,give_up),info_trace) =
+  let undef sigma l = List.filter (fun g -> Evd.is_undefined sigma g) l in
+  let tac =
+    tac >>= fun () ->
+    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 sigma = List.fold_left Proofview.Unsafe.mark_as_goal sigma retrieved in
+    Proofview.Unsafe.tclEVARS sigma >>= fun () ->
+    Proofview.tclUNIT retrieved
+  in
+  let (retrieved,proofview,(status,to_shelve,give_up),info_trace) =
     Proofview.apply env tac sp
   in
-  let sigma = Proofview.return tacticced_proofview in
-  (* Already solved goals are not to be counted as shelved. Nor are
-     they to be marked as unresolvable. *)
-  let undef l = List.filter (fun g -> Evd.is_undefined sigma g) l in
-  let retrieved = undef (List.rev (Evd.future_goals sigma)) in
-  let shelf = (undef pr.shelf)@retrieved@(undef to_shelve) in
+  let sigma = Proofview.return proofview in
+  let to_shelve = undef sigma to_shelve in
+  let shelf = (undef sigma pr.shelf)@retrieved@to_shelve in
   let proofview =
     List.fold_left
-      Proofview.Unsafe.mark_as_goal
-      tacticced_proofview
-      retrieved
+      Proofview.Unsafe.mark_as_unresolvable
+      proofview
+      to_shelve
   in
   let given_up = pr.given_up@give_up in
   let proofview = Proofview.Unsafe.reset_future_goals proofview in
@@ -387,9 +396,27 @@ module V82 = struct
       { p with proofview = Proofview.V82.grab p.proofview }
 
 
+  (* Main component of vernac command Existential *)
   let instantiate_evar n com pr =
-    let sp = pr.proofview in
-    let proofview = Proofview.V82.instantiate_evar n com sp in
+    let tac =
+      Proofview.tclBIND Proofview.tclEVARMAP begin fun sigma ->
+      let (evk, evi) =
+        let evl = Evarutil.non_instantiated sigma in
+        let evl = Evar.Map.bindings evl in
+        if (n <= 0) then
+          CErrors.error "incorrect existential variable index"
+        else if CList.length evl < n then
+          CErrors.error "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 sigma = Evar_refiner.w_refine (evk, evi) (ltac_vars, rawc) sigma in
+      Proofview.Unsafe.tclEVARS sigma
+    end in
+    let ((), proofview, _, _) = Proofview.apply (Global.env ()) tac pr.proofview in
     let shelf =
       List.filter begin fun g ->
         Evd.is_undefined (Proofview.return proofview) g
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index f22cdbcc..e753e972 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -23,8 +23,9 @@ open Names
 (* Type of proof modes :
     - 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 : string ;
+  name : proof_mode_name ;
   set : unit -> unit ;
   reset : unit -> unit
 }
@@ -33,10 +34,10 @@ let proof_modes = Hashtbl.create 6
 let find_proof_mode n =
   try Hashtbl.find proof_modes n
   with Not_found ->
-    Errors.error (Format.sprintf "No proof mode named \"%s\"." n)
+    CErrors.error (Format.sprintf "No proof mode named \"%s\"." n)
 
 let register_proof_mode ({name = n} as m) =
-  Hashtbl.add proof_modes n (Ephemeron.create m)
+  Hashtbl.add proof_modes n (CEphemeron.create m)
 
 (* initial mode: standard mode *)
 let standard = { name = "No" ; set = (fun ()->()) ; reset = (fun () -> ()) }
@@ -45,6 +46,9 @@ let _ = register_proof_mode standard
 (* Default proof mode, to be set at the beginning of proofs. *)
 let default_proof_mode = ref (find_proof_mode "No")
 
+let get_default_proof_mode_name () =
+  (CEphemeron.default !default_proof_mode standard).name
+
 let _ =
   Goptions.declare_string_option {Goptions.
     optsync = true ;
@@ -52,7 +56,7 @@ let _ =
     optname = "default proof mode" ;
     optkey = ["Default";"Proof";"Mode"] ;
     optread = begin fun () ->
-      (Ephemeron.default !default_proof_mode standard).name
+      (CEphemeron.default !default_proof_mode standard).name
     end;
     optwrite = begin fun n ->
       default_proof_mode := find_proof_mode n
@@ -83,15 +87,18 @@ type closed_proof = proof_object * proof_terminator
 
 type pstate = {
   pid : Id.t;
-  terminator : proof_terminator Ephemeron.key;
+  terminator : proof_terminator CEphemeron.key;
   endline_tactic : Tacexpr.raw_tactic_expr option;
   section_vars : Context.section_context option;
   proof : Proof.proof;
   strength : Decl_kinds.goal_kind;
-  mode : proof_mode Ephemeron.key;
+  mode : proof_mode CEphemeron.key;
   universe_binders: universe_binders option;
 }
 
+let make_terminator f = f
+let apply_terminator f = f
+
 (* The head of [!pstates] is the actual current proof, the other ones are
    to be resumed when the current proof is closed or aborted. *)
 let pstates = ref ([] : pstate list)
@@ -103,11 +110,11 @@ let current_proof_mode = ref !default_proof_mode
 let update_proof_mode () =
   match !pstates with
   | { mode = m } :: _ ->
-      Ephemeron.iter_opt !current_proof_mode (fun x -> x.reset ());
+      CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ());
       current_proof_mode := m;
-      Ephemeron.iter_opt !current_proof_mode (fun x -> x.set ())
+      CEphemeron.iter_opt !current_proof_mode (fun x -> x.set ())
   | _ ->
-      Ephemeron.iter_opt !current_proof_mode (fun x -> x.reset ());
+      CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ());
       current_proof_mode := find_proof_mode "No"
 
 (* combinators for the current_proof lists *)
@@ -115,15 +122,15 @@ let push a l = l := a::!l;
   update_proof_mode ()
 
 exception NoSuchProof
-let _ = Errors.register_handler begin function
-  | NoSuchProof -> Errors.error "No such proof."
-  | _ -> raise Errors.Unhandled
+let _ = CErrors.register_handler begin function
+  | NoSuchProof -> CErrors.error "No such proof."
+  | _ -> raise CErrors.Unhandled
 end
 
 exception NoCurrentProof
-let _ = Errors.register_handler begin function
-  | NoCurrentProof -> Errors.error "No focused proof (No proof-editing in progress)."
-  | _ -> raise Errors.Unhandled
+let _ = CErrors.register_handler begin function
+  | NoCurrentProof -> CErrors.error "No focused proof (No proof-editing in progress)."
+  | _ -> raise CErrors.Unhandled
 end
 
 (*** Proof Global manipulation ***)
@@ -183,7 +190,7 @@ let check_no_pending_proof () =
   if not (there_are_pending_proofs ()) then
     ()
   else begin
-    Errors.error (Pp.string_of_ppcmds
+    CErrors.error (Pp.string_of_ppcmds
       (str"Proof editing in progress" ++ msg_proofs () ++ fnl() ++
        str"Use \"Abort All\" first or complete proof(s)."))
   end
@@ -195,7 +202,7 @@ let discard (loc,id) =
   let n = List.length !pstates in
   discard_gen id;
   if Int.equal (List.length !pstates) n then
-    Errors.user_err_loc
+    CErrors.user_err_loc
       (loc,"Pfedit.delete_proof",str"No such proof" ++ msg_proofs ())
 
 let discard_current () =
@@ -215,9 +222,9 @@ let set_proof_mode mn =
   set_proof_mode (find_proof_mode mn) (get_current_proof_name ())
 
 let activate_proof_mode mode =
-  Ephemeron.iter_opt (find_proof_mode mode) (fun x -> x.set ())
-let disactivate_proof_mode mode =
-  Ephemeron.iter_opt (find_proof_mode mode) (fun x -> x.reset ())
+  CEphemeron.iter_opt (find_proof_mode mode) (fun x -> x.set ())
+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
     [id] with goals [goals] (a list of pairs of environment and
@@ -230,7 +237,7 @@ let disactivate_proof_mode mode =
 let start_proof sigma id ?pl str goals terminator =
   let initial_state = {
     pid = id;
-    terminator = Ephemeron.create terminator;
+    terminator = CEphemeron.create terminator;
     proof = Proof.start sigma goals;
     endline_tactic = None;
     section_vars = None;
@@ -242,7 +249,7 @@ let start_proof sigma id ?pl str goals terminator =
 let start_dependent_proof id ?pl str goals terminator =
   let initial_state = {
     pid = id;
-    terminator = Ephemeron.create terminator;
+    terminator = CEphemeron.create terminator;
     proof = Proof.dependent_start goals;
     endline_tactic = None;
     section_vars = None;
@@ -264,18 +271,19 @@ let _ = Goptions.declare_bool_option
       Goptions.optwrite = (fun b -> proof_using_auto_clear := b) }
 
 let set_used_variables l =
+  let open Context.Named.Declaration in
   let env = Global.env () in
   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 pi1 ctx) Id.Set.empty in
+    List.fold_right Id.Set.add (List.map 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
-    | (x,None,_) ->
+    | LocalAssum (x,_) ->
        if Id.Set.mem x all_safe then orig
        else (ctx, all_safe, (Loc.ghost,x)::to_clear) 
-    | (x,Some bo, ty) as decl ->
+    | 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
@@ -288,7 +296,7 @@ let set_used_variables l =
   | [] -> raise NoCurrentProof
   | p :: rest ->
       if not (Option.is_empty p.section_vars) then
-        Errors.error "Used section variables can be declared only once";
+        CErrors.error "Used section variables can be declared only once";
       pstates := { p with section_vars = Some ctx} :: rest;
       ctx, to_clear
 
@@ -299,6 +307,11 @@ 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)
+
 let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
   let { pid; section_vars; strength; proof; terminator; universe_binders } =
     cur_pstate () in
@@ -329,7 +342,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
         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 = Evd.evar_universe_context_set initunivs universes in
+          let ctx = constrain_variables initunivs 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. *)
@@ -338,7 +351,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
           (initunivs, typ), ((body, ctx_body), eff)
         else
           let initunivs = Univ.UContext.empty in
-          let ctx = Evd.evar_universe_context_set initunivs universes 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 *)
@@ -353,7 +366,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
         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,Evd.evar_universe_context_set initunivs (Future.force univs)),eff)
+          (pt,constrain_variables initunivs (Future.force univs)),eff)
   in
   let entries =
     Future.map2 (fun p (_, t) ->
@@ -375,7 +388,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
   in
   { id = pid; entries = entries; persistence = strength;
     universes = (universes, binders) },
-  fun pr_ending -> Ephemeron.get terminator pr_ending
+  fun pr_ending -> CEphemeron.get terminator pr_ending
 
 type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context
 
@@ -395,7 +408,7 @@ let return_proof ?(allow_partial=false) () =
   let evd =
     let error s =
       let prf = str " (in proof " ++ Id.print pid ++ str ")" in
-      raise (Errors.UserError("last tactic before Qed",s ++ prf))
+      raise (CErrors.UserError("last tactic before Qed",s ++ prf))
     in
     try Proof.return proof with
     | Proof.UnfinishedProof ->
@@ -423,11 +436,11 @@ let close_proof ~keep_body_ucst_separate fix_exn =
 
 (** Gets the current terminator without checking that the proof has
     been completed. Useful for the likes of [Admitted]. *)
-let get_terminator () = Ephemeron.get ( cur_pstate() ).terminator
+let get_terminator () = CEphemeron.get ( cur_pstate() ).terminator
 let set_terminator hook =
   match !pstates with
   | [] -> raise NoCurrentProof
-  | p :: ps -> pstates := { p with terminator = Ephemeron.create hook } :: ps
+  | p :: ps -> pstates := { p with terminator = CEphemeron.create hook } :: ps
 
 
 
@@ -458,7 +471,7 @@ module Bullet = struct
   type behavior = {
     name : string;
     put : Proof.proof -> t -> Proof.proof;
-    suggest: Proof.proof -> string option
+    suggest: Proof.proof -> std_ppcmds
   }
 
   let behaviors = Hashtbl.create 4
@@ -468,7 +481,7 @@ module Bullet = struct
   let none = {
     name = "None";
     put = (fun x _ -> x);
-    suggest = (fun _ -> None)
+    suggest = (fun _ -> mt ())
   }
   let _ = register_behavior none
 
@@ -484,36 +497,30 @@ module Bullet = struct
     (* give a message only if more informative than the standard coq message *)
     let suggest_on_solved_goal sugg =
       match sugg with
-      | NeedClosingBrace -> Some "Try unfocusing with \"}\"."
-      | NoBulletInUse -> None
-      | ProofFinished -> None
-      | Suggest b -> Some ("Focus next goal with bullet "
-			   ^ Pp.string_of_ppcmds (Pp.(pr_bullet b))
-			   ^".")
-      | Unfinished b -> Some ("The current bullet "
-			      ^ Pp.string_of_ppcmds (Pp.(pr_bullet b))
-			      ^ " is unfinished.")
+      | 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 -> "Try unfocusing with \"}\"."
+      | NeedClosingBrace -> str"Try unfocusing with \"}\"."
       | NoBulletInUse -> assert false (* This should never raise an error. *)
-      | ProofFinished -> "No more subgoals."
-      | Suggest b -> ("Bullet " ^ Pp.string_of_ppcmds (Pp.(pr_bullet b))
-		      ^ " is mandatory here.")
-      | Unfinished b -> ("Current bullet " ^ Pp.string_of_ppcmds (Pp.(pr_bullet b))
-			 ^ " is not finished.")
+      | 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 _ =
-      Errors.register_handler
+      CErrors.register_handler
 	(function
 	| FailedBullet (b,sugg) ->
-	  let prefix = "Wrong bullet " ^ Pp.string_of_ppcmds (Pp.(pr_bullet b)) ^ " : " in
-	  Errors.errorlabstrm "Focus" (str prefix ++ str (suggest_on_error sugg))
-	| _ -> raise Errors.Unhandled)
+	  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 *)
@@ -610,7 +617,7 @@ module Bullet = struct
     let _ = register_behavior strict
   end
 
-  (* Current bullet behavior, controled by the option *)
+  (* Current bullet behavior, controlled by the option *)
   let current_behavior = ref Strict.strict
 
   let _ =
@@ -626,7 +633,7 @@ module Bullet = struct
 	current_behavior :=
           try Hashtbl.find behaviors n
           with Not_found ->
-            Errors.error ("Unknown bullet behavior: \"" ^ n ^ "\".")
+            CErrors.error ("Unknown bullet behavior: \"" ^ n ^ "\".")
       end
     }
 
@@ -657,21 +664,26 @@ let _ =
 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
-  | Vernacexpr.SelectAllParallel -> "par"
 
 let parse_goal_selector = function
   | "all" -> Vernacexpr.SelectAll
   | i ->
-      let err_msg = "A selector must be \"all\" or a natural number." in
+      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 Errors.error err_msg;
+              if i < 0 then CErrors.error err_msg;
               Vernacexpr.SelectNth i
-        with Failure _ -> Errors.error err_msg
+        with Failure _ -> CErrors.error err_msg
       end
 
 let _ =
@@ -700,7 +712,7 @@ type state = pstate list
 let freeze ~marshallable =
   match marshallable with
   | `Yes ->
-      Errors.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 ()
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 7fbd183e..59daa296 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -16,8 +16,9 @@
     - A function [reset] to reset the *standard mode* from it 
 
 *)
+type proof_mode_name = string
 type proof_mode = {
-  name : string ;
+  name : proof_mode_name ;
   set : unit -> unit ;
   reset : unit -> unit
 }
@@ -27,6 +28,7 @@ type 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
 
 val there_are_pending_proofs : unit -> bool
 val check_no_pending_proof : unit -> unit
@@ -40,7 +42,7 @@ 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 : string -> unit
+val set_proof_mode : proof_mode_name -> unit
 
 exception NoCurrentProof
 val give_me_the_proof : unit -> Proof.proof
@@ -70,9 +72,12 @@ type proof_ending =
   | Proved of Vernacexpr.opacity_flag *
              (Vernacexpr.lident * Decl_kinds.theorem_kind option) option *
               proof_object
-type proof_terminator = proof_ending -> unit
+type proof_terminator
 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]
     with goals [goals] (a list of pairs of environment and
     conclusion); [str] describes what kind of theorem/definition this
@@ -150,8 +155,8 @@ val get_universe_binders : unit -> universe_binders option
 (**********************************************************)
 
 
-val activate_proof_mode : string -> unit
-val disactivate_proof_mode : string -> unit
+val activate_proof_mode : proof_mode_name -> unit
+val disactivate_current_proof_mode : unit -> unit
 
 (**********************************************************)
 (*                                                        *)
@@ -169,7 +174,7 @@ module Bullet : sig
   type behavior = {
     name : string;
     put : Proof.proof -> t -> Proof.proof;
-    suggest: Proof.proof -> string option
+    suggest: Proof.proof -> Pp.std_ppcmds
   }
 
   (** A registered behavior can then be accessed in Coq
@@ -186,7 +191,7 @@ module Bullet : sig
   (** Handles focusing/defocusing with bullets:
        *)
   val put : Proof.proof -> t -> Proof.proof
-  val suggest : Proof.proof -> string option
+  val suggest : Proof.proof -> Pp.std_ppcmds
 end
 
 
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
deleted file mode 100644
index dd2c7b25..00000000
--- a/proofs/proof_type.ml
+++ /dev/null
@@ -1,52 +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        *)
-(************************************************************************)
-
-(*i*)
-open Evd
-open Names
-open Term
-open Tacexpr
-open Glob_term
-open Nametab
-open Misctypes
-(*i*)
-
-(* This module defines the structure of proof tree and the tactic type. So, it
-   is used by Proof_tree and Refiner *)
-
-(** Types of goals, tactics, rules ... *)
-
-type goal = Goal.goal
-
-type tactic = goal sigma -> goal list sigma 
-
-type prim_rule =
-  | Cut of bool * bool * Id.t * types
-  | FixRule of Id.t * int * (Id.t * int * constr) list * int
-  | Cofix of Id.t * (Id.t * constr) list * int
-  | Refine of constr
-  | Thin of Id.t list
-  | Move of Id.t * Id.t move_location
-
-(** Nowadays, the only rules we'll consider are the primitive rules *)
-
-type rule = prim_rule
-
-(** Ltac traces *)
-
-type ltac_call_kind =
-  | LtacMLCall of glob_tactic_expr
-  | LtacNotationCall of KerName.t
-  | LtacNameCall of ltac_constant
-  | LtacAtomCall of glob_atomic_tactic_expr
-  | LtacVarCall of Id.t * glob_tactic_expr
-  | LtacConstrInterp of glob_constr * Pretyping.ltac_var_map
-
-type ltac_trace = (Loc.t * ltac_call_kind) list
-
-let (ltac_trace_info : ltac_trace Exninfo.t) = Exninfo.make ()
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index aa05f58a..c1207962 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(** Legacy proof engine. Do not use in newly written code. *)
+
 open Evd
 open Names
 open Term
@@ -19,57 +21,12 @@ open Misctypes
 
 type prim_rule =
   | Cut of bool * bool * Id.t * types
-  | FixRule of Id.t * int * (Id.t * int * constr) list * int
-  | Cofix of Id.t * (Id.t * constr) list * int
   | Refine of constr
-  | Thin of Id.t list
-  | Move of Id.t * Id.t move_location
 
 (** Nowadays, the only rules we'll consider are the primitive rules *)
 
 type rule = prim_rule
 
-(** The type [goal sigma] is the type of subgoal. It has the following form
-{v   it    = \{ evar_concl = [the conclusion of the subgoal]
-             evar_hyps = [the hypotheses of the subgoal]
-             evar_body = Evar_Empty;
-             evar_info = \{ pgm    : [The Realizer pgm if any]
-                           lc     : [Set of evar num occurring in subgoal] \}\}
-   sigma = \{ stamp = [an int chardacterizing the ed field, for quick compare]
-             ed : [A set of existential variables depending in the subgoal]
-               number of first evar,
-               it = \{ evar_concl = [the type of first evar]
-                      evar_hyps = [the context of the evar]
-                      evar_body = [the body of the Evar if any]
-                      evar_info = \{ pgm    : [Useless ??]
-                                    lc     : [Set of evars occurring
-                                              in the type of evar] \} \};
-               ...
-               number of last evar,
-               it = \{ evar_concl = [the type of evar]
-                      evar_hyps = [the context of the evar]
-                      evar_body = [the body of the Evar if any]
-                      evar_info = \{ pgm    : [Useless ??]
-                                    lc     : [Set of evars occurring
-                                              in the type of evar] \} \} \} v}
-*)
-
 type goal = Goal.goal
 
 type tactic = goal sigma -> goal list sigma
-
-(** Ltac traces *)
-
-(** TODO: Move those definitions somewhere sensible *)
-
-type ltac_call_kind =
-  | LtacMLCall of glob_tactic_expr
-  | LtacNotationCall of KerName.t
-  | LtacNameCall of ltac_constant
-  | LtacAtomCall of glob_atomic_tactic_expr
-  | LtacVarCall of Id.t * glob_tactic_expr
-  | LtacConstrInterp of glob_constr * Pretyping.ltac_var_map
-
-type ltac_trace = (Loc.t * ltac_call_kind) list
-
-val ltac_trace_info : ltac_trace Exninfo.t
diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml
index a69645b1..caa9b328 100644
--- a/proofs/proof_using.ml
+++ b/proofs/proof_using.ml
@@ -10,6 +10,7 @@ open Names
 open Environ
 open Util
 open Vernacexpr
+open Context.Named.Declaration
 
 let to_string e =
   let rec aux = function
@@ -33,7 +34,8 @@ let in_nameset =
 
 let rec close_fwd e s =
   let s' =
-    List.fold_left (fun s (id,b,ty) ->      
+    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
@@ -61,13 +63,13 @@ and set_of_id env ty id =
         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 pi1 (named_context env)) Id.Set.empty
+    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 pi1 (named_context env)) Id.Set.empty
+  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
@@ -126,7 +128,7 @@ let suggest_Proof_using name env vars ids_typ context_ids =
   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);
-  msg_info (
+  Feedback.msg_info (
     str"The proof of "++ str name ++ spc() ++
     str "should start with one of the following commands:"++spc()++
     v 0 (
diff --git a/proofs/proof_using.mli b/proofs/proof_using.mli
index 1bf38b69..b2c65412 100644
--- a/proofs/proof_using.mli
+++ b/proofs/proof_using.mli
@@ -6,6 +6,8 @@
 (*         *       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
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index 32bf5576..804a5436 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -2,18 +2,13 @@ Miscprint
 Goal
 Evar_refiner
 Proof_using
-Proof_type
-Proof_errors
-Logic_monad
-Proofview_monad
 Logic
-Proofview
+Refine
 Proof
 Proof_global
 Redexpr
 Refiner
 Tacmach
 Pfedit
-Tactic_debug
 Clenv
 Clenvtac
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
deleted file mode 100644
index a6d9735f..00000000
--- a/proofs/proofview.ml
+++ /dev/null
@@ -1,1257 +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        *)
-(************************************************************************)
-
-
-(** This files defines the basic mechanism of proofs: the [proofview]
-    type is the state which tactics manipulate (a global state for
-    existential variables, together with the list of goals), and the type
-    ['a tactic] is the (abstract) type of tactics modifying the proof
-    state and returning a value of type ['a]. *)
-
-open Pp
-open Util
-open Proofview_monad
-
-(** Main state of tactics *)
-type proofview = Proofview_monad.proofview
-
-type entry = (Term.constr * Term.types) list
-
-(** Returns a stylised view of a proofview for use by, for instance,
-    ide-s. *)
-(* spiwack: the type of [proofview] will change as we push more
-   refined functions to ide-s. This would be better than spawning a
-   new nearly identical function everytime. Hence the generic name. *)
-(* In this version: returns the list of focused goals together with
-   the [evar_map] context. *)
-let proofview p =
-  p.comb , p.solution
-
-let compact el ({ solution } as pv) =
-  let nf = Evarutil.nf_evar solution in
-  let size = Evd.fold (fun _ _ i -> i+1) solution 0 in
-  let new_el = List.map (fun (t,ty) -> nf t, nf ty) el in
-  let pruned_solution = Evd.drop_all_defined solution in
-  let apply_subst_einfo _ ei =
-    Evd.({ ei with
-       evar_concl =  nf ei.evar_concl;
-       evar_hyps = Environ.map_named_val nf ei.evar_hyps;
-       evar_candidates = Option.map (List.map nf) ei.evar_candidates }) in
-  let new_solution = Evd.raw_map_undefined apply_subst_einfo pruned_solution in
-  let new_size = Evd.fold (fun _ _ i -> i+1) new_solution 0 in
-  msg_info (Pp.str (Printf.sprintf "Evars: %d -> %d\n" size new_size));
-  new_el, { pv with solution = new_solution; }
-
-
-(** {6 Starting and querying a proof view} *)
-
-type telescope =
-  | TNil of Evd.evar_map
-  | TCons of Environ.env * Evd.evar_map * Term.types * (Evd.evar_map -> Term.constr -> telescope)
-
-let dependent_init =
-  (* Goals are created with a store which marks them as unresolvable
-     for type classes. *)
-  let store = Typeclasses.set_resolvable Evd.Store.empty false in
-  (* Goals don't have a source location. *)
-  let src = (Loc.ghost,Evar_kinds.GoalEvar) in
-  (* Main routine *)
-  let rec aux = function
-  | TNil sigma -> [], { solution = sigma; comb = []; shelf = [] }
-  | TCons (env, sigma, typ, t) ->
-    let (sigma, econstr ) = Evarutil.new_evar env sigma ~src ~store typ in
-    let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in
-    let (gl, _) = Term.destEvar econstr in
-    let entry = (econstr, typ) :: ret in
-    entry, { solution = sol; comb = gl :: comb; shelf = [] }
-  in
-  fun t ->
-    let entry, v = aux t in
-    (* The created goal are not to be shelved. *)
-    let solution = Evd.reset_future_goals v.solution in
-    entry, { v with solution }
-
-let init =
-  let rec aux sigma = function
-    | [] -> TNil sigma
-    | (env,g)::l -> TCons (env,sigma,g,(fun sigma _ -> aux sigma l))
-  in
-  fun sigma l -> dependent_init (aux sigma l)
-
-let initial_goals initial = initial
-
-let finished = function
-  | {comb = []} -> true
-  | _  -> false
-
-let return { solution=defs } = defs
-
-let return_constr { solution = defs } c = Evarutil.nf_evar defs c
-
-let partial_proof entry pv = CList.map (return_constr pv) (CList.map fst entry)
-
-
-(** {6 Focusing commands} *)
-
-(** A [focus_context] represents the part of the proof view which has
-    been removed by a focusing action, it can be used to unfocus later
-    on. *)
-(* First component is a reverse list of the goals which come before
-   and second component is the list of the goals which go after (in
-   the expected order). *)
-type focus_context = Evar.t list * Evar.t list
-
-
-(** Returns a stylised view of a focus_context for use by, for
-    instance, ide-s. *)
-(* spiwack: the type of [focus_context] will change as we push more
-   refined functions to ide-s. This would be better than spawning a
-   new nearly identical function everytime. Hence the generic name. *)
-(* In this version: the goals in the context, as a "zipper" (the first
-   list is in reversed order). *)
-let focus_context f = f
-
-(** This (internal) function extracts a sublist between two indices,
-    and returns this sublist together with its context: if it returns
-    [(a,(b,c))] then [a] is the sublist and (rev b)@a@c is the
-    original list.  The focused list has lenght [j-i-1] and contains
-    the goals from number [i] to number [j] (both included) the first
-    goal of the list being numbered [1].  [focus_sublist i j l] raises
-    [IndexOutOfRange] if [i > length l], or [j > length l] or [j <
-    i]. *)
-let focus_sublist i j l =
-  let (left,sub_right) = CList.goto (i-1) l in
-  let (sub, right) = 
-    try CList.chop (j-i+1) sub_right
-    with Failure _ -> raise CList.IndexOutOfRange
-  in
-  (sub, (left,right))
-
-(** Inverse operation to the previous one. *)
-let unfocus_sublist (left,right) s =
-  CList.rev_append left (s@right)
-
-
-(** [focus i j] focuses a proofview on the goals from index [i] to
-    index [j] (inclusive, goals are indexed from [1]). I.e. goals
-    number [i] to [j] become the only focused goals of the returned
-    proofview.  It returns the focused proofview, and a context for
-    the focus stack. *)
-let focus i j sp =
-  let (new_comb, context) = focus_sublist i j sp.comb in
-  ( { sp with comb = new_comb } , context )
-
-
-(** [advance sigma g] returns [Some g'] if [g'] is undefined and is
-    the current avatar of [g] (for instance [g] was changed by [clear]
-    into [g']). It returns [None] if [g] has been (partially)
-    solved. *)
-(* spiwack: [advance] is probably performance critical, and the good
-   behaviour of its definition may depend sensitively to the actual
-   definition of [Evd.find]. Currently, [Evd.find] starts looking for
-   a value in the heap of undefined variable, which is small. Hence in
-   the most common case, where [advance] is applied to an unsolved
-   goal ([advance] is used to figure if a side effect has modified the
-   goal) it terminates quickly. *)
-let rec advance sigma g =
-  let open Evd in
-  let evi = Evd.find sigma g in
-  match evi.evar_body with
-  | Evar_empty -> Some g
-  | Evar_defined v ->
-      if Option.default false (Store.get evi.evar_extra Evarutil.cleared) then
-        let (e,_) = Term.destEvar v in
-        advance sigma e
-      else
-        None
-
-(** [undefined defs l] is the list of goals in [l] which are still
-    unsolved (after advancing cleared goals). *)
-let undefined defs l = CList.map_filter (advance defs) l
-
-(** Unfocuses a proofview with respect to a context. *)
-let unfocus c sp =
-  { sp with comb = undefined sp.solution (unfocus_sublist c sp.comb) }
-
-
-(** {6 The tactic monad} *)
-
-(** - Tactics are objects which apply a transformation to all the
-    subgoals of the current view at the same time. By opposition to
-    the old vision of applying it to a single goal. It allows tactics
-    such as [shelve_unifiable], tactics to reorder the focused goals,
-    or global automation tactic for dependent subgoals (instantiating
-    an evar has influences on the other goals of the proof in
-    progress, not being able to take that into account causes the
-    current eauto tactic to fail on some instances where it could
-    succeed).  Another benefit is that it is possible to write tactics
-    that can be executed even if there are no focused goals.
-    - Tactics form a monad ['a tactic], in a sense a tactic can be
-    seen as a function (without argument) which returns a value of
-    type 'a and modifies the environment (in our case: the view).
-    Tactics of course have arguments, but these are given at the
-    meta-level as OCaml functions.  Most tactics in the sense we are
-    used to return [()], that is no really interesting values. But
-    some might pass information around.  The tactics seen in Coq's
-    Ltac are (for now at least) only [unit tactic], the return values
-    are kept for the OCaml toolkit.  The operation or the monad are
-    [Proofview.tclUNIT] (which is the "return" of the tactic monad)
-    [Proofview.tclBIND] (which is the "bind") and [Proofview.tclTHEN]
-    (which is a specialized bind on unit-returning tactics).
-    - Tactics have support for full-backtracking. Tactics can be seen
-    having multiple success: if after returning the first success a
-    failure is encountered, the tactic can backtrack and use a second
-    success if available. The state is backtracked to its previous
-    value, except the non-logical state defined in the {!NonLogical}
-    module below.
-*)
-(* spiwack: as far as I'm aware this doesn't really relate to
-   F. Kirchner and C. Muñoz. *)
-
-module Proof = Logical
-
-(** type of tactics:
-
-   tactics can
-   - access the environment,
-   - report unsafe status, shelved goals and given up goals
-   - access and change the current [proofview]
-   - backtrack on previous changes of the proofview *)
-type +'a tactic = 'a Proof.t
-
-(** Applies a tactic to the current proofview. *)
-let apply env t sp =
-  let open Logic_monad in
-  let ans = Proof.repr (Proof.run t false (sp,env)) in
-  let ans = Logic_monad.NonLogical.run ans in
-  match ans with
-  | Nil (e, info) -> iraise (TacticFailure e, info)
-  | Cons ((r, (state, _), status, info), _) ->
-    let (status, gaveup) = status in
-    let status = (status, state.shelf, gaveup) in
-    let state = { state with shelf = [] } in
-    r, state, status, Trace.to_tree info
-
-
-
-(** {7 Monadic primitives} *)
-
-(** Unit of the tactic monad. *)
-let tclUNIT = Proof.return
-
-(** Bind operation of the tactic monad. *)
-let tclBIND = Proof.(>>=)
-
-(** Interpretes the ";" (semicolon) of Ltac. As a monadic operation,
-    it's a specialized "bind". *)
-let tclTHEN = Proof.(>>)
-
-(** [tclIGNORE t] has the same operational content as [t], but drops
-    the returned value. *)
-let tclIGNORE = Proof.ignore
-
-module Monad = Proof
-
-
-
-(** {7 Failure and backtracking} *)
-
-
-(** [tclZERO e] fails with exception [e]. It has no success. *)
-let tclZERO ?info e =
-  let info = match info with
-  | None -> Exninfo.null
-  | Some info -> info
-  in
-  Proof.zero (e, info)
-
-(** [tclOR t1 t2] behaves like [t1] as long as [t1] succeeds. Whenever
-    the successes of [t1] have been depleted and it failed with [e],
-    then it behaves as [t2 e]. In other words, [tclOR] inserts a
-    backtracking point. *)
-let tclOR = Proof.plus
-
-(** [tclORELSE t1 t2] is equal to [t1] if [t1] has at least one
-    success or [t2 e] if [t1] fails with [e]. It is analogous to
-    [try/with] handler of exception in that it is not a backtracking
-    point. *)
-let tclORELSE t1 t2 =
-  let open Logic_monad in
-  let open Proof in
-  split t1 >>= function
-    | Nil e -> t2 e
-    | Cons (a,t1') -> plus (return a) t1'
-
-(** [tclIFCATCH a s f] is a generalisation of {!tclORELSE}: if [a]
-    succeeds at least once then it behaves as [tclBIND a s] otherwise,
-    if [a] fails with [e], then it behaves as [f e]. *)
-let tclIFCATCH a s f =
-  let open Logic_monad in
-  let open Proof in
-  split a >>= function
-    | Nil e -> f e
-    | Cons (x,a') -> plus (s x) (fun e -> (a' e) >>= fun x' -> (s x'))
-
-(** [tclONCE t] behave like [t] except it has at most one success:
-    [tclONCE t] stops after the first success of [t]. If [t] fails
-    with [e], [tclONCE t] also fails with [e]. *)
-let tclONCE = Proof.once
-
-exception MoreThanOneSuccess
-let _ = Errors.register_handler begin function
-  | MoreThanOneSuccess -> Errors.error "This tactic has more than one success."
-  | _ -> raise Errors.Unhandled
-end
-
-(** [tclEXACTLY_ONCE e t] succeeds as [t] if [t] has exactly one
-    success. Otherwise it fails. The tactic [t] is run until its first
-    success, then a failure with exception [e] is simulated. It [t]
-    yields another success, then [tclEXACTLY_ONCE e t] fails with
-    [MoreThanOneSuccess] (it is a user error). Otherwise,
-    [tclEXACTLY_ONCE e t] succeeds with the first success of
-    [t]. Notice that the choice of [e] is relevant, as the presence of
-    further successes may depend on [e] (see {!tclOR}). *)
-let tclEXACTLY_ONCE e t =
-  let open Logic_monad in
-  let open Proof in
-  split t >>= function
-    | Nil (e, info) -> tclZERO ~info e
-    | Cons (x,k) ->
-        Proof.split (k (e, Exninfo.null)) >>= function
-          | Nil _ -> tclUNIT x
-          | _ -> tclZERO MoreThanOneSuccess
-
-
-(** [tclCASE t] wraps the {!Proofview_monad.Logical.split} primitive. *)
-type 'a case =
-| Fail of iexn
-| Next of 'a * (iexn -> 'a tactic)
-let tclCASE t =
-  let open Logic_monad in
-  let map = function
-  | Nil e -> Fail e
-  | Cons (x, t) -> Next (x, t)
-  in
-  Proof.map map (Proof.split t)
-
-let tclBREAK = Proof.break
-
-
-
-(** {7 Focusing tactics} *)
-
-exception NoSuchGoals of int
-
-(* This hook returns a string to be appended to the usual message.
-   Primarily used to add a suggestion about the right bullet to use to
-   focus the next goal, if applicable. *)
-let nosuchgoals_hook:(int -> string option) ref = ref ((fun n -> None))
-let set_nosuchgoals_hook f = nosuchgoals_hook := f
-
-
-
-(* This uses the hook above *)
-let _ = Errors.register_handler begin function
-  | NoSuchGoals n ->
-    let suffix:string option = (!nosuchgoals_hook) n in
-    Errors.errorlabstrm ""
-      (str "No such " ++ str (String.plural n "goal") ++ str "."
-       ++ pr_opt str suffix)
-  | _ -> raise Errors.Unhandled
-end
-
-(** [tclFOCUS_gen nosuchgoal i j t] applies [t] in a context where
-    only the goals numbered [i] to [j] are focused (the rest of the goals
-    is restored at the end of the tactic). If the range [i]-[j] is not
-    valid, then it [tclFOCUS_gen nosuchgoal i j t] is [nosuchgoal]. *)
-let tclFOCUS_gen nosuchgoal i j t =
-  let open Proof in
-  Pv.get >>= fun initial ->
-  try
-    let (focused,context) = focus i j initial in
-    Pv.set focused >>
-    t >>= fun result ->
-    Pv.modify (fun next -> unfocus context next) >>
-    return result
-  with CList.IndexOutOfRange -> nosuchgoal
-
-let tclFOCUS i j t = tclFOCUS_gen (tclZERO (NoSuchGoals (j+1-i))) i j t
-let tclTRYFOCUS i j t = tclFOCUS_gen (tclUNIT ()) i j t
-
-(** Like {!tclFOCUS} but selects a single goal by name. *)
-let tclFOCUSID id t =
-  let open Proof in
-  Pv.get >>= fun initial ->
-  try
-    let ev = Evd.evar_key id initial.solution in
-    try
-      let n = CList.index Evar.equal ev initial.comb in
-      (* goal is already under focus *)
-      let (focused,context) = focus n n initial in
-      Pv.set focused >>
-        t >>= fun result ->
-      Pv.modify (fun next -> unfocus context next) >>
-        return result
-    with Not_found ->
-      (* otherwise, save current focus and work purely on the shelve *)
-      Comb.set [ev] >>
-        t >>= fun result ->
-      Comb.set initial.comb  >>
-        return result
-  with Not_found -> tclZERO (NoSuchGoals 1)
-
-(** {7 Dispatching on goals} *)
-
-exception SizeMismatch of int*int
-let _ = Errors.register_handler begin function
-  | SizeMismatch (i,_) ->
-      let open Pp in
-      let errmsg =
-        str"Incorrect number of goals" ++ spc() ++
-        str"(expected "++int i++str(String.plural i " tactic") ++ str")."
-      in
-      Errors.errorlabstrm "" errmsg
-  | _ -> raise Errors.Unhandled
-end
-
-(** A variant of [Monad.List.iter] where we iter over the focused list
-    of goals. The argument tactic is executed in a focus comprising
-    only of the current goal, a goal which has been solved by side
-    effect is skipped. The generated subgoals are concatenated in
-    order.  *)
-let iter_goal i =
-  let open Proof in
-  Comb.get >>= fun initial ->
-  Proof.List.fold_left begin fun (subgoals as cur) goal ->
-    Solution.get >>= fun step ->
-    match advance step goal with
-    | None -> return cur
-    | Some goal ->
-        Comb.set [goal] >>
-        i goal >>
-        Proof.map (fun comb -> comb :: subgoals) Comb.get
-  end [] initial >>= fun subgoals ->
-  Solution.get >>= fun evd ->
-  Comb.set CList.(undefined evd (flatten (rev subgoals)))
-
-(** A variant of [Monad.List.fold_left2] where the first list is the
-    list of focused goals. The argument tactic is executed in a focus
-    comprising only of the current goal, a goal which has been solved
-    by side effect is skipped. The generated subgoals are concatenated
-    in order. *)
-let fold_left2_goal i s l =
-  let open Proof in
-  Pv.get >>= fun initial ->
-  let err =
-    return () >>= fun () -> (* Delay the computation of list lengths. *)
-    tclZERO (SizeMismatch (CList.length initial.comb,CList.length l))
-  in 
-  Proof.List.fold_left2 err begin fun ((r,subgoals) as cur) goal a ->
-    Solution.get >>= fun step ->
-    match advance step goal with
-    | None -> return cur
-    | Some goal ->
-        Comb.set [goal] >>
-        i goal a r >>= fun r ->
-        Proof.map (fun comb -> (r, comb :: subgoals)) Comb.get
-  end (s,[]) initial.comb l >>= fun (r,subgoals) ->
-  Solution.get >>= fun evd ->
-  Comb.set CList.(undefined evd (flatten (rev subgoals))) >>
-  return r
-
-(** Dispatch tacticals are used to apply a different tactic to each
-    goal under focus. They come in two flavours: [tclDISPATCH] takes a
-    list of [unit tactic]-s and build a [unit tactic]. [tclDISPATCHL]
-    takes a list of ['a tactic] and returns an ['a list tactic].
-
-    They both work by applying each of the tactic in a focus
-    restricted to the corresponding goal (starting with the first
-    goal). In the case of [tclDISPATCHL], the tactic returns a list of
-    the same size as the argument list (of tactics), each element
-    being the result of the tactic executed in the corresponding goal.
-
-    When the length of the tactic list is not the number of goal,
-    raises [SizeMismatch (g,t)] where [g] is the number of available
-    goals, and [t] the number of tactics passed.
-
-    [tclDISPATCHGEN join tacs] generalises both functions as the
-    successive results of [tacs] are stored in reverse order in a
-    list, and [join] is used to convert the result into the expected
-    form. *)
-let tclDISPATCHGEN0 join tacs =
-  match tacs with
-  | [] ->
-      begin 
-        let open Proof in
-        Comb.get >>= function
-        | [] -> tclUNIT (join [])
-        | comb -> tclZERO (SizeMismatch (CList.length comb,0))
-      end
-  | [tac] ->
-      begin
-        let open Proof in
-        Pv.get >>= function
-        | { comb=[goal] ; solution } ->
-            begin match advance solution goal with
-            | None -> tclUNIT (join [])
-            | Some _ -> Proof.map (fun res -> join [res]) tac
-            end
-        | {comb} -> tclZERO (SizeMismatch(CList.length comb,1))
-      end
-  | _ ->
-      let iter _ t cur = Proof.map (fun y -> y :: cur) t in
-      let ans = fold_left2_goal iter [] tacs in
-      Proof.map join ans
-
-let tclDISPATCHGEN join tacs =
-  let branch t = InfoL.tag (Info.DBranch) t in
-  let tacs = CList.map branch tacs in
-  InfoL.tag (Info.Dispatch) (tclDISPATCHGEN0 join tacs)
-
-let tclDISPATCH tacs = tclDISPATCHGEN Pervasives.ignore tacs
-
-let tclDISPATCHL tacs = tclDISPATCHGEN CList.rev tacs
-
-
-(** [extend_to_list startxs rx endxs l] builds a list
-    [startxs@[rx,...,rx]@endxs] of the same length as [l]. Raises
-    [SizeMismatch] if [startxs@endxs] is already longer than [l]. *)
-let extend_to_list startxs rx endxs l =
-  (* spiwack: I use [l] essentially as a natural number *)
-  let rec duplicate acc = function
-    | [] -> acc
-    | _::rest -> duplicate (rx::acc) rest
-  in
-  let rec tail to_match rest =
-    match rest, to_match with
-    | [] , _::_ -> raise (SizeMismatch(0,0)) (* placeholder *)
-    | _::rest , _::to_match -> tail to_match rest
-    | _ , [] -> duplicate endxs rest
-  in
-  let rec copy pref rest =
-    match rest,pref with
-    | [] , _::_ -> raise (SizeMismatch(0,0)) (* placeholder *)
-    | _::rest, a::pref -> a::(copy pref rest)
-    | _ , [] -> tail endxs rest
-  in
-  copy startxs l
-
-(** [tclEXTEND b r e] is a variant of {!tclDISPATCH}, where the [r]
-    tactic is "repeated" enough time such that every goal has a tactic
-    assigned to it ([b] is the list of tactics applied to the first
-    goals, [e] to the last goals, and [r] is applied to every goal in
-    between). *)
-let tclEXTEND tacs1 rtac tacs2 =
-  let open Proof in
-  Comb.get >>= fun comb ->
-  try
-    let tacs = extend_to_list tacs1 rtac tacs2 comb in
-    tclDISPATCH tacs
-  with SizeMismatch _ ->
-    tclZERO (SizeMismatch(
-      CList.length comb,
-      (CList.length tacs1)+(CList.length tacs2)))
-(* spiwack: failure occurs only when the number of goals is too
-   small. Hence we can assume that [rtac] is replicated 0 times for
-   any error message. *)
-
-(** [tclEXTEND [] tac []]. *)
-let tclINDEPENDENT tac =
-  let open Proof in
-  Pv.get >>= fun initial ->
-  match initial.comb with
-  | [] -> tclUNIT ()
-  | [_] -> tac
-  | _ ->
-      let tac = InfoL.tag (Info.DBranch) tac in
-      InfoL.tag (Info.Dispatch) (iter_goal (fun _ -> tac))
-
-
-
-(** {7 Goal manipulation} *)
-
-(** Shelves all the goals under focus. *)
-let shelve =
-  let open Proof in
-  Comb.get >>= fun initial ->
-  Comb.set [] >>
-  InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve")) >>
-  Shelf.modify (fun gls -> gls @ initial)
-
-
-(** [contained_in_info e evi] checks whether the evar [e] appears in
-    the hypotheses, the conclusion or the body of the evar_info
-    [evi]. Note: since we want to use it on goals, the body is actually
-    supposed to be empty. *)
-let contained_in_info sigma e evi =
-  Evar.Set.mem e (Evd.evars_of_filtered_evar_info (Evarutil.nf_evar_info sigma evi))
-
-(** [depends_on sigma src tgt] checks whether the goal [src] appears
-    as an existential variable in the definition of the goal [tgt] in
-    [sigma]. *)
-let depends_on sigma src tgt =
-  let evi = Evd.find sigma tgt in
-  contained_in_info sigma src evi
-
-(** [unifiable sigma g l] checks whether [g] appears in another
-    subgoal of [l]. The list [l] may contain [g], but it does not
-    affect the result. *)
-let unifiable sigma g l =
-  CList.exists (fun tgt -> not (Evar.equal g tgt) && depends_on sigma g tgt) l
-
-(** [partition_unifiable sigma l] partitions [l] into a pair [(u,n)]
-    where [u] is composed of the unifiable goals, i.e. the goals on
-    whose definition other goals of [l] depend, and [n] are the
-    non-unifiable goals. *)
-let partition_unifiable sigma l =
-  CList.partition (fun g -> unifiable sigma g l) l
-
-(** Shelves the unifiable goals under focus, i.e. the goals which
-    appear in other goals under focus (the unfocused goals are not
-    considered). *)
-let shelve_unifiable =
-  let open Proof in
-  Pv.get >>= fun initial ->
-  let (u,n) = partition_unifiable initial.solution initial.comb in
-  Comb.set n >>
-  InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve_unifiable")) >>
-  Shelf.modify (fun gls -> gls @ u)
-
-(** [guard_no_unifiable] fails with error [UnresolvedBindings] if some
-    goals are unifiable (see {!shelve_unifiable}) in the current focus. *)
-let guard_no_unifiable =
-  let open Proof in
-  Pv.get >>= fun initial ->
-  let (u,n) = partition_unifiable initial.solution initial.comb in
-  match u with
-  | [] -> tclUNIT ()
-  | gls ->
-      let l = CList.map (fun g -> Evd.dependent_evar_ident g initial.solution) gls in
-      let l = CList.map (fun id -> Names.Name id) l in
-      tclZERO (Logic.RefinerError (Logic.UnresolvedBindings l))
-
-(** [unshelve l p] adds all the goals in [l] at the end of the focused
-    goals of p *)
-let unshelve l p =
-  (* advance the goals in case of clear *)
-  let l = undefined p.solution l in
-  { p with comb = p.comb@l }
-
-let with_shelf tac =
-  let open Proof in
-  Pv.get >>= fun pv ->
-  let { shelf; solution } = pv in
-  Pv.set { pv with shelf = []; solution = Evd.reset_future_goals solution } >>
-  tac >>= fun ans ->
-  Pv.get >>= fun npv ->
-  let { shelf = gls; solution = sigma } = npv in
-  let gls' = Evd.future_goals sigma in
-  let fgoals = Evd.future_goals solution in
-  let pgoal = Evd.principal_future_goal solution in
-  let sigma = Evd.restore_future_goals sigma fgoals pgoal in
-  Pv.set { npv with shelf; solution = sigma } >>
-  tclUNIT (CList.rev_append gls' gls, ans)
-
-(** [goodmod p m] computes the representative of [p] modulo [m] in the
-    interval [[0,m-1]].*)
-let goodmod p m =
-  let p' = p mod m in
-  (* if [n] is negative [n mod l] is negative of absolute value less
-     than [l], so [(n mod l)+l] is the representative of [n] in the
-     interval [[0,l-1]].*)
-  if p' < 0 then p'+m else p'
-
-let cycle n =
-  let open Proof in
-  InfoL.leaf (Info.Tactic (fun () -> Pp.(str"cycle "++int n))) >>
-  Comb.modify begin fun initial ->
-    let l = CList.length initial in
-    let n' = goodmod n l in
-    let (front,rear) = CList.chop n' initial in
-    rear@front
-  end
-
-let swap i j =
-  let open Proof in
-  InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"swap"++spc()++int i++spc()++int j)))) >>
-  Comb.modify begin fun initial ->
-    let l = CList.length initial in
-    let i = if i>0 then i-1 else i and j = if j>0 then j-1 else j in
-    let i = goodmod i l and j = goodmod j l in
-    CList.map_i begin fun k x ->
-      match k with
-      | k when Int.equal k i -> CList.nth initial j
-      | k when Int.equal k j -> CList.nth initial i
-      | _ -> x
-    end 0 initial
-  end
-
-let revgoals =
-  let open Proof in
-  InfoL.leaf (Info.Tactic (fun () -> Pp.str"revgoals")) >>
-  Comb.modify CList.rev
-
-let numgoals =
-  let open Proof in
-  Comb.get >>= fun comb ->
-  return (CList.length comb)
-
-
-
-(** {7 Access primitives} *)
-
-let tclEVARMAP = Solution.get
-
-let tclENV = Env.get
-
-
-
-(** {7 Put-like primitives} *)
-
-
-let emit_side_effects eff x =
-  { x with solution = Evd.emit_side_effects eff x.solution }
-
-let tclEFFECTS eff =
-  let open Proof in
-  return () >>= fun () -> (* The Global.env should be taken at exec time *)
-  Env.set (Global.env ()) >>
-  Pv.modify (fun initial -> emit_side_effects eff initial)
-
-let mark_as_unsafe = Status.put false
-
-(** Gives up on the goal under focus. Reports an unsafe status. Proofs
-    with given up goals cannot be closed. *)
-let give_up =
-  let open Proof in
-  Comb.get >>= fun initial ->
-  Comb.set [] >>
-  mark_as_unsafe >>
-  InfoL.leaf (Info.Tactic (fun () -> Pp.str"give_up")) >>
-  Giveup.put initial
-
-
-
-(** {7 Control primitives} *)
-
-
-module Progress = struct
-
-  let eq_constr = Evarutil.eq_constr_univs_test
-
-  (** equality function on hypothesis contexts *)
-  let eq_named_context_val sigma1 sigma2 ctx1 ctx2 =
-    let open Environ in
-    let c1 = named_context_of_val ctx1 and c2 = named_context_of_val ctx2 in
-    let eq_named_declaration (i1, c1, t1) (i2, c2, t2) =
-      Names.Id.equal i1 i2 && Option.equal (eq_constr sigma1 sigma2) c1 c2 
-      && (eq_constr sigma1 sigma2) t1 t2
-    in List.equal eq_named_declaration c1 c2
-
-  let eq_evar_body sigma1 sigma2 b1 b2 =
-    let open Evd in
-    match b1, b2 with
-    | Evar_empty, Evar_empty -> true
-    | Evar_defined t1, Evar_defined t2 -> eq_constr sigma1 sigma2 t1 t2
-    | _ -> false
-
-  let eq_evar_info sigma1 sigma2 ei1 ei2 =
-    let open Evd in
-    eq_constr sigma1 sigma2 ei1.evar_concl ei2.evar_concl &&
-    eq_named_context_val sigma1 sigma2 (ei1.evar_hyps) (ei2.evar_hyps) &&
-    eq_evar_body sigma1 sigma2 ei1.evar_body ei2.evar_body
-
-  (** Equality function on goals *)
-  let goal_equal evars1 gl1 evars2 gl2 =
-    let evi1 = Evd.find evars1 gl1 in
-    let evi2 = Evd.find evars2 gl2 in
-    eq_evar_info evars1 evars2 evi1 evi2
-
-end
-
-let tclPROGRESS t =
-  let open Proof in
-  Pv.get >>= fun initial ->
-  t >>= fun res ->
-  Pv.get >>= fun final ->
-  (* [*_test] test absence of progress. [quick_test] is approximate
-     whereas [exhaustive_test] is complete. *)
-  let quick_test =
-    initial.solution == final.solution && initial.comb == final.comb
-  in
-  let exhaustive_test =
-    Util.List.for_all2eq begin fun i f ->
-      Progress.goal_equal initial.solution i final.solution f
-    end initial.comb final.comb
-  in
-  let test =
-    quick_test || exhaustive_test
-  in
-  if not test then
-    tclUNIT res
-  else
-    tclZERO (Errors.UserError ("Proofview.tclPROGRESS" , Pp.str"Failed to progress."))
-
-exception Timeout
-let _ = Errors.register_handler begin function
-  | Timeout -> Errors.errorlabstrm "Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!")
-  | _ -> Pervasives.raise Errors.Unhandled
-end
-
-let tclTIMEOUT n t =
-  let open Proof in
-  (* spiwack: as one of the monad is a continuation passing monad, it
-     doesn't force the computation to be threaded inside the underlying
-     (IO) monad. Hence I force it myself by asking for the evaluation of
-     a dummy value first, lest [timeout] be called when everything has
-     already been computed. *)
-  let t = Proof.lift (Logic_monad.NonLogical.return ()) >> t in
-  Proof.get >>= fun initial ->
-  Proof.current >>= fun envvar ->
-  Proof.lift begin
-    Logic_monad.NonLogical.catch
-      begin
-        let open Logic_monad.NonLogical in
-        timeout n (Proof.repr (Proof.run t envvar initial)) >>= fun r ->
-        match r with
-        | Logic_monad.Nil e -> return (Util.Inr e)
-        | Logic_monad.Cons (r, _) -> return (Util.Inl r)
-      end
-      begin let open Logic_monad.NonLogical in function (e, info) ->
-        match e with
-        | Logic_monad.Timeout -> return (Util.Inr (Timeout, info))
-        | Logic_monad.TacticFailure e ->
-          return (Util.Inr (e, info))
-        | e -> Logic_monad.NonLogical.raise ~info e
-      end
-  end >>= function
-    | Util.Inl (res,s,m,i) ->
-        Proof.set s >>
-        Proof.put m >>
-        Proof.update (fun _ -> i) >>
-        return res
-    | Util.Inr (e, info) -> tclZERO ~info e
-
-let tclTIME s t =
-  let pr_time t1 t2 n msg =
-    let msg =
-      if n = 0 then
-        str msg
-      else
-        str (msg ^ " after ") ++ int n ++ str (String.plural n " backtracking")
-    in
-    msg_info(str "Tactic call" ++ pr_opt str s ++ str " ran for " ++
-             System.fmt_time_difference t1 t2 ++ str " " ++ surround msg) in
-  let rec aux n t =
-    let open Proof in
-    tclUNIT () >>= fun () ->
-    let tstart = System.get_time() in
-    Proof.split t >>= let open Logic_monad in function
-    | Nil (e, info) ->
-      begin
-        let tend = System.get_time() in
-        pr_time tstart tend n "failure";
-        tclZERO ~info e
-      end
-    | Cons (x,k) ->
-        let tend = System.get_time() in
-        pr_time tstart tend n "success";
-        tclOR (tclUNIT x) (fun e -> aux (n+1) (k e))
-  in aux 0 t
-
-
-
-(** {7 Unsafe primitives} *)
-
-module Unsafe = struct
-
-  let tclEVARS evd =
-    Pv.modify (fun ps -> { ps with solution = evd })
-
-  let tclNEWGOALS gls =
-    Pv.modify begin fun step ->
-      let gls = undefined step.solution gls in
-      { step with comb = step.comb @ gls }
-    end
-
-  let tclGETGOALS = Comb.get
-
-  let tclSETGOALS = Comb.set
-
-  let tclEVARSADVANCE evd =
-    Pv.modify (fun ps -> { ps with solution = evd; comb = undefined evd ps.comb })
-
-  let tclEVARUNIVCONTEXT ctx = 
-    Pv.modify (fun ps -> { ps with solution = Evd.set_universe_context ps.solution ctx })
-
-  let reset_future_goals p =
-    { p with solution = Evd.reset_future_goals p.solution }
-
-  let mark_as_goal_evm evd content =
-    let info = Evd.find evd content in
-    let info =
-      { info with Evd.evar_source = match info.Evd.evar_source with
-      | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x
-      | loc,_ -> loc,Evar_kinds.GoalEvar }
-    in
-    let info = Typeclasses.mark_unresolvable info in
-    Evd.add evd content info
-
-  let mark_as_goal p gl =
-    { p with solution = mark_as_goal_evm p.solution gl }
-
-end
-
-
-
-(** {7 Notations} *)
-
-module Notations = struct
-  let (>>=) = tclBIND
-  let (<*>) = tclTHEN
-  let (<+>) t1 t2 = tclOR t1 (fun _ -> t2)
-end
-
-open Notations
-
-
-
-(** {6 Goal-dependent tactics} *)
-
-(* To avoid shadowing by the local [Goal] module *)
-module GoalV82 = Goal.V82
-
-let catchable_exception = function
-  | Logic_monad.Exception _ -> false
-  | e -> Errors.noncritical e
-
-
-module Goal = struct
-
-  type 'a t = {
-    env : Environ.env;
-    sigma : Evd.evar_map;
-    concl : Term.constr ;
-    self : Evar.t ; (* for compatibility with old-style definitions *)
-  }
-
-  let assume (gl : 'a t) = (gl :> [ `NF ] t)
-
-  let env { env=env } = env
-  let sigma { sigma=sigma } = sigma
-  let hyps { env=env } = Environ.named_context env
-  let concl { concl=concl } = concl
-  let extra { sigma=sigma; self=self } = Goal.V82.extra sigma self
-
-  let raw_concl { concl=concl } = concl
-
-
-  let gmake_with info env sigma goal = 
-    { env = Environ.reset_with_named_context (Evd.evar_filtered_hyps info) env ;
-      sigma = sigma ;
-      concl = Evd.evar_concl info ;
-      self = goal }
-
-  let nf_gmake env sigma goal =
-    let info = Evarutil.nf_evar_info sigma (Evd.find sigma goal) in
-    let sigma = Evd.add sigma goal info in
-    gmake_with info env sigma goal , sigma
-
-  let nf_enter f =
-    InfoL.tag (Info.Dispatch) begin
-    iter_goal begin fun goal ->
-      Env.get >>= fun env ->
-      tclEVARMAP >>= fun sigma ->
-      try
-        let (gl, sigma) = nf_gmake env sigma goal in
-        tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) (f gl))
-      with e when catchable_exception e ->
-        let (e, info) = Errors.push e in
-        tclZERO ~info e
-    end
-    end
-
-  let normalize { self } =
-    Env.get >>= fun env ->
-    tclEVARMAP >>= fun sigma ->
-    let (gl,sigma) = nf_gmake env sigma self in
-    tclTHEN (Unsafe.tclEVARS sigma) (tclUNIT gl)
-
-  let gmake env sigma goal =
-    let info = Evd.find sigma goal in
-    gmake_with info env sigma goal
-
-  let enter f =
-    let f gl = InfoL.tag (Info.DBranch) (f gl) in
-    InfoL.tag (Info.Dispatch) begin
-    iter_goal begin fun goal ->
-      Env.get >>= fun env ->
-      tclEVARMAP >>= fun sigma ->
-      try f (gmake env sigma goal)
-      with e when catchable_exception e ->
-        let (e, info) = Errors.push e in
-        tclZERO ~info e
-    end
-    end
-
-  let goals =
-    Env.get >>= fun env ->
-    Pv.get >>= fun step ->
-    let sigma = step.solution in
-    let map goal =
-      match advance sigma goal with
-      | None -> None (** ppedrot: Is this check really necessary? *)
-      | Some goal ->
-        let gl =
-          tclEVARMAP >>= fun sigma ->
-          tclUNIT (gmake env sigma goal)
-        in
-        Some gl
-    in
-    tclUNIT (CList.map_filter map step.comb)
-
-  (* compatibility *)
-  let goal { self=self } = self
-
-end
-
-
-
-(** {6 The refine tactic} *)
-
-module Refine =
-struct
-
-  let extract_prefix env info =
-    let ctx1 = List.rev (Environ.named_context env) in
-    let ctx2 = List.rev (Evd.evar_context info) in
-    let rec share l1 l2 accu = match l1, l2 with
-    | d1 :: l1, d2 :: l2 ->
-      if d1 == d2 then share l1 l2 (d1 :: accu)
-      else (accu, d2 :: l2)
-    | _ -> (accu, l2)
-    in
-    share ctx1 ctx2 []
-
-  let typecheck_evar ev env sigma =
-    let info = Evd.find sigma ev in
-    (** Typecheck the hypotheses. *)
-    let type_hyp (sigma, env) (na, body, t as decl) =
-      let evdref = ref sigma in
-      let _ = Typing.sort_of env evdref t in
-      let () = match body with
-      | None -> ()
-      | Some body -> Typing.check env evdref body t
-      in
-      (!evdref, Environ.push_named decl env)
-    in
-    let (common, changed) = extract_prefix env info in
-    let env = Environ.reset_with_named_context (Environ.val_of_named_context common) env in
-    let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in
-    (** Typecheck the conclusion *)
-    let evdref = ref sigma in
-    let _ = Typing.sort_of env evdref (Evd.evar_concl info) in
-    !evdref
-
-  let typecheck_proof c concl env sigma =
-    let evdref = ref sigma in
-    let () = Typing.check env evdref c concl in
-    !evdref
-
-  let (pr_constrv,pr_constr) =
-    Hook.make ~default:(fun _env _sigma _c -> Pp.str"<constr>") ()
-
-  let refine ?(unsafe = true) f = Goal.enter begin fun gl ->
-    let sigma = Goal.sigma gl in
-    let env = Goal.env gl in
-    let concl = Goal.concl 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
-    (** Create the refinement term *)
-    let (sigma, c) = f (Evd.reset_future_goals sigma) in
-    let evs = Evd.future_goals sigma in
-    let evkmain = Evd.principal_future_goal sigma 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
-    (** Check that the refined term is typesafe *)
-    let sigma = if unsafe then sigma else typecheck_proof c concl env sigma in
-    (** Check that the goal itself does not appear in the refined term *)
-    let _ =
-      if not (Evarutil.occur_evar_upto sigma gl.Goal.self c) then ()
-      else Pretype_errors.error_occur_check env sigma gl.Goal.self c
-    in
-    (** Proceed to the refinement *)
-    let sigma = match evkmain with
-      | None -> Evd.define gl.Goal.self c sigma
-      | Some evk ->
-          let id = Evd.evar_ident gl.Goal.self sigma in
-          Evd.rename evk id (Evd.define gl.Goal.self c 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 = undefined sigma (CList.rev evs) in
-    let sigma = CList.fold_left Unsafe.mark_as_goal_evm sigma comb in
-    let open Proof in
-    InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"refine"++spc()++ Hook.get pr_constrv env sigma c)))) >>
-    Pv.modify (fun ps -> { ps with solution = sigma; comb; })
-  end
-
-  (** Useful definitions *)
-
-  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
-    in
-    evd , j'.Environ.uj_val
-
-  let refine_casted ?unsafe f = Goal.enter begin fun gl ->
-    let concl = Goal.concl gl in
-    let env = Goal.env gl in
-    let f h = let (h, c) = f h in with_type env h c concl in
-    refine ?unsafe f
-  end
-end
-
-
-
-(** {6 Trace} *)
-
-module Trace = struct
-
-  let record_info_trace = InfoL.record_trace
-
-  let log m = InfoL.leaf (Info.Msg m)
-  let name_tactic m t = InfoL.tag (Info.Tactic m) t
-
-  let pr_info ?(lvl=0) info =
-    assert (lvl >= 0);
-    Info.(print (collapse lvl info))
-
-end
-
-
-
-(** {6 Non-logical state} *)
-
-module NonLogical = Logic_monad.NonLogical
-
-let tclLIFT = Proof.lift
-
-let tclCHECKINTERRUPT =
-   tclLIFT (NonLogical.make Control.check_for_interrupt)
-
-
-
-
-
-(*** Compatibility layer with <= 8.2 tactics ***)
-module V82 = struct
-  type tac = Evar.t Evd.sigma -> Evar.t list Evd.sigma
-
-  let tactic tac =
-    (* spiwack: we ignore the dependencies between goals here,
-       expectingly preserving the semantics of <= 8.2 tactics *)
-    (* spiwack: convenience notations, waiting for ocaml 3.12 *)
-    let open Proof in
-    Pv.get >>= fun ps ->
-    try
-      let tac gl evd = 
-        let glsigma  =
-          tac { Evd.it = gl ; sigma = evd; }  in
-        let sigma = glsigma.Evd.sigma in
-        let g = glsigma.Evd.it in
-        ( g, sigma )
-      in
-        (* Old style tactics expect the goals normalized with respect to evars. *)
-      let (initgoals,initevd) =
-        Evd.Monad.List.map (fun g s -> GoalV82.nf_evar s g) ps.comb ps.solution
-      in
-      let (goalss,evd) = Evd.Monad.List.map tac initgoals initevd in
-      let sgs = CList.flatten goalss in
-      let sgs = undefined evd sgs in
-      InfoL.leaf (Info.Tactic (fun () -> Pp.str"<unknown>")) >>
-      Pv.set { ps with solution = evd; comb = sgs; }
-    with e when catchable_exception e ->
-      let (e, info) = Errors.push e in
-      tclZERO ~info e
-
-
-  (* normalises the evars in the goals, and stores the result in
-     solution. *)
-  let nf_evar_goals =
-    Pv.modify begin fun ps ->
-    let map g s = GoalV82.nf_evar s g in
-    let (goals,evd) = Evd.Monad.List.map map ps.comb ps.solution in
-    { ps with solution = evd; comb = goals; }
-    end
-      
-  let has_unresolved_evar pv =
-    Evd.has_undefined pv.solution
-
-  (* Main function in the implementation of Grab Existential Variables.*)
-  let grab pv =
-    let undef = Evd.undefined_map pv.solution in
-    let goals = CList.rev_map fst (Evar.Map.bindings undef) in
-    { pv with comb = goals }
-      
-    
-
-  (* Returns the open goals of the proofview together with the evar_map to 
-     interpret them. *)
-  let goals { comb = comb ; solution = solution; } =
-   { Evd.it = comb ; sigma = solution }
-
-  let top_goals initial { solution=solution; } =
-    let goals = CList.map (fun (t,_) -> fst (Term.destEvar t)) initial in
-    { Evd.it = goals ; sigma=solution; }
-
-  let top_evars initial =
-    let evars_of_initial (c,_) =
-      Evar.Set.elements (Evd.evars_of_term c)
-    in
-    CList.flatten (CList.map evars_of_initial initial)
-
-  let instantiate_evar n com pv =
-    let (evk,_) =
-      let evl = Evarutil.non_instantiated pv.solution in
-      let evl = Evar.Map.bindings evl in
-      if (n <= 0) then
-	Errors.error "incorrect existential variable index"
-      else if CList.length evl < n then
-	  Errors.error "not so many uninstantiated existential variables"
-      else
-	CList.nth evl (n-1)
-    in
-    { pv with
-	solution = Evar_refiner.instantiate_pf_com evk com pv.solution }
-
-  let of_tactic t gls =
-    try
-      let init = { shelf = []; solution = gls.Evd.sigma ; comb = [gls.Evd.it] } in
-      let (_,final,_,_) = apply (GoalV82.env gls.Evd.sigma gls.Evd.it) t init in
-      { Evd.sigma = final.solution ; it = final.comb }
-    with Logic_monad.TacticFailure e as src ->
-      let (_, info) = Errors.push src in
-      iraise (e, info)
-
-  let put_status = Status.put
-
-  let catchable_exception = catchable_exception
-
-  let wrap_exceptions f =
-    try f ()
-    with e when catchable_exception e ->
-      let (e, info) = Errors.push e in tclZERO ~info e
-
-end
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
deleted file mode 100644
index 2157459f..00000000
--- a/proofs/proofview.mli
+++ /dev/null
@@ -1,580 +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        *)
-(************************************************************************)
-
-(** This files defines the basic mechanism of proofs: the [proofview]
-    type is the state which tactics manipulate (a global state for
-    existential variables, together with the list of goals), and the type
-    ['a tactic] is the (abstract) type of tactics modifying the proof
-    state and returning a value of type ['a]. *)
-
-open Util
-open Term
-
-(** Main state of tactics *)
-type proofview
-
-(** Returns a stylised view of a proofview for use by, for instance,
-    ide-s. *)
-(* spiwack: the type of [proofview] will change as we push more
-   refined functions to ide-s. This would be better than spawning a
-   new nearly identical function everytime. Hence the generic name. *)
-(* In this version: returns the list of focused goals together with
-   the [evar_map] context. *)
-val proofview : proofview -> Goal.goal list * Evd.evar_map
-
-
-(** {6 Starting and querying a proof view} *)
-
-(** Abstract representation of the initial goals of a proof. *)
-type entry
-
-(** Optimize memory consumption *)
-val compact : entry -> proofview -> entry * proofview
-
-(** Initialises a proofview, the main argument is a list of
-    environments (including a [named_context] which are used as
-    hypotheses) pair with conclusion types, creating accordingly many
-    initial goals. Because a proof does not necessarily starts in an
-    empty [evar_map] (indeed a proof can be triggered by an incomplete
-    pretyping), [init] takes an additional argument to represent the
-    initial [evar_map]. *)
-val init : Evd.evar_map -> (Environ.env * Term.types) list -> entry * proofview
-
-(** A [telescope] is a list of environment and conclusion like in
-    {!init}, except that each element may depend on the previous
-    goals. The telescope passes the goals in the form of a
-    [Term.constr] which represents the goal as an [evar]. The
-    [evar_map] is threaded in state passing style. *)
-type telescope =
-  | TNil of Evd.evar_map
-  | TCons of Environ.env * Evd.evar_map * Term.types * (Evd.evar_map -> Term.constr -> telescope)
-
-(** Like {!init}, but goals are allowed to be dependent on one
-    another. Dependencies between goals is represented with the type
-    [telescope] instead of [list]. Note that the first [evar_map] of
-    the telescope plays the role of the [evar_map] argument in
-    [init]. *)
-val dependent_init  : telescope -> entry * proofview
-
-(** [finished pv] is [true] if and only if [pv] is complete. That is,
-    if it has an empty list of focused goals. There could still be
-    unsolved subgoaled, but they would then be out of focus. *)
-val finished : proofview -> bool
-
-(** Returns the current [evar] state. *)
-val return : proofview -> Evd.evar_map
-
-val partial_proof : entry -> proofview -> constr list
-val initial_goals : entry -> (constr * types) list
-
-
-
-(** {6 Focusing commands} *)
-
-(** A [focus_context] represents the part of the proof view which has
-    been removed by a focusing action, it can be used to unfocus later
-    on. *)
-type focus_context
-
-(** Returns a stylised view of a focus_context for use by, for
-    instance, ide-s. *)
-(* spiwack: the type of [focus_context] will change as we push more
-   refined functions to ide-s. This would be better than spawning a
-   new nearly identical function everytime. Hence the generic name. *)
-(* In this version: the goals in the context, as a "zipper" (the first
-   list is in reversed order). *)
-val focus_context : focus_context -> Goal.goal list * Goal.goal list
-
-(** [focus i j] focuses a proofview on the goals from index [i] to
-    index [j] (inclusive, goals are indexed from [1]). I.e. goals
-    number [i] to [j] become the only focused goals of the returned
-    proofview.  It returns the focused proofview, and a context for
-    the focus stack. *)
-val focus : int -> int -> proofview -> proofview * focus_context
-
-(** Unfocuses a proofview with respect to a context. *)
-val unfocus : focus_context -> proofview -> proofview
-
-
-(** {6 The tactic monad} *)
-
-(** - Tactics are objects which apply a transformation to all the
-    subgoals of the current view at the same time. By opposition to
-    the old vision of applying it to a single goal. It allows tactics
-    such as [shelve_unifiable], tactics to reorder the focused goals,
-    or global automation tactic for dependent subgoals (instantiating
-    an evar has influences on the other goals of the proof in
-    progress, not being able to take that into account causes the
-    current eauto tactic to fail on some instances where it could
-    succeed).  Another benefit is that it is possible to write tactics
-    that can be executed even if there are no focused goals.
-    - Tactics form a monad ['a tactic], in a sense a tactic can be
-    seen as a function (without argument) which returns a value of
-    type 'a and modifies the environment (in our case: the view).
-    Tactics of course have arguments, but these are given at the
-    meta-level as OCaml functions.  Most tactics in the sense we are
-    used to return [()], that is no really interesting values. But
-    some might pass information around.  The tactics seen in Coq's
-    Ltac are (for now at least) only [unit tactic], the return values
-    are kept for the OCaml toolkit.  The operation or the monad are
-    [Proofview.tclUNIT] (which is the "return" of the tactic monad)
-    [Proofview.tclBIND] (which is the "bind") and [Proofview.tclTHEN]
-    (which is a specialized bind on unit-returning tactics).
-    - Tactics have support for full-backtracking. Tactics can be seen
-    having multiple success: if after returning the first success a
-    failure is encountered, the tactic can backtrack and use a second
-    success if available. The state is backtracked to its previous
-    value, except the non-logical state defined in the {!NonLogical}
-    module below.
-*)
-
-
-(** The abstract type of tactics *)
-type +'a tactic 
-
-(** Applies a tactic to the current proofview. Returns a tuple
-    [a,pv,(b,sh,gu)] where [a] is the return value of the tactic, [pv]
-    is the updated proofview, [b] a boolean which is [true] if the
-    tactic has not done any action considered unsafe (such as
-    admitting a lemma), [sh] is the list of goals which have been
-    shelved by the tactic, and [gu] the list of goals on which the
-    tactic has given up. In case of multiple success the first one is
-    selected. If there is no success, fails with
-    {!Logic_monad.TacticFailure}*)
-val apply : Environ.env -> 'a tactic -> proofview -> 'a
-                                                   * proofview
-                                                   * (bool*Goal.goal list*Goal.goal list)
-                                                   * Proofview_monad.Info.tree
-
-(** {7 Monadic primitives} *)
-
-(** Unit of the tactic monad. *)
-val tclUNIT : 'a -> 'a tactic
- 
-(** Bind operation of the tactic monad. *)
-val tclBIND : 'a tactic -> ('a -> 'b tactic) -> 'b tactic
-
-(** Interprets the ";" (semicolon) of Ltac. As a monadic operation,
-    it's a specialized "bind". *)
-val tclTHEN : unit tactic -> 'a tactic -> 'a tactic
-
-(** [tclIGNORE t] has the same operational content as [t], but drops
-    the returned value. *)
-val tclIGNORE : 'a tactic -> unit tactic
-
-(** Generic monadic combinators for tactics. *)
-module Monad : Monad.S with type +'a t = 'a tactic
-
-(** {7 Failure and backtracking} *)
-
-(** [tclZERO e] fails with exception [e]. It has no success. *)
-val tclZERO : ?info:Exninfo.info -> exn -> 'a tactic
-
-(** [tclOR t1 t2] behaves like [t1] as long as [t1] succeeds. Whenever
-    the successes of [t1] have been depleted and it failed with [e],
-    then it behaves as [t2 e]. In other words, [tclOR] inserts a
-    backtracking point. *)
-val tclOR : 'a tactic -> (iexn -> 'a tactic) -> 'a tactic
-
-(** [tclORELSE t1 t2] is equal to [t1] if [t1] has at least one
-    success or [t2 e] if [t1] fails with [e]. It is analogous to
-    [try/with] handler of exception in that it is not a backtracking
-    point. *)
-val tclORELSE : 'a tactic -> (iexn -> 'a tactic) -> 'a tactic
-
-(** [tclIFCATCH a s f] is a generalisation of {!tclORELSE}: if [a]
-    succeeds at least once then it behaves as [tclBIND a s] otherwise,
-    if [a] fails with [e], then it behaves as [f e]. *)
-val tclIFCATCH : 'a tactic -> ('a -> 'b tactic) -> (iexn -> 'b tactic) -> 'b tactic
-
-(** [tclONCE t] behave like [t] except it has at most one success:
-    [tclONCE t] stops after the first success of [t]. If [t] fails
-    with [e], [tclONCE t] also fails with [e]. *)
-val tclONCE : 'a tactic -> 'a tactic
-
-(** [tclEXACTLY_ONCE e t] succeeds as [t] if [t] has exactly one
-    success. Otherwise it fails. The tactic [t] is run until its first
-    success, then a failure with exception [e] is simulated. It [t]
-    yields another success, then [tclEXACTLY_ONCE e t] fails with
-    [MoreThanOneSuccess] (it is a user error). Otherwise,
-    [tclEXACTLY_ONCE e t] succeeds with the first success of
-    [t]. Notice that the choice of [e] is relevant, as the presence of
-    further successes may depend on [e] (see {!tclOR}). *)
-exception MoreThanOneSuccess
-val tclEXACTLY_ONCE : exn -> 'a tactic -> 'a tactic
-
-(** [tclCASE t] splits [t] into its first success and a
-    continuation. It is the most general primitive to control
-    backtracking. *)
-type 'a case =
-  | Fail of iexn
-  | Next of 'a * (iexn -> 'a tactic)
-val tclCASE : 'a tactic -> 'a case tactic
-
-(** [tclBREAK p t] is a generalization of [tclONCE t]. Instead of
-    stopping after the first success, it succeeds like [t] until a
-    failure with an exception [e] such that [p e = Some e'] is raised. At
-    which point it drops the remaining successes, failing with [e'].
-    [tclONCE t] is equivalent to [tclBREAK (fun e -> Some e) t]. *)
-val tclBREAK : (iexn -> iexn option) -> 'a tactic -> 'a tactic
-
-
-(** {7 Focusing tactics} *)
-
-(** [tclFOCUS i j t] applies [t] after focusing on the goals number
-    [i] to [j] (see {!focus}). The rest of the goals is restored after
-    the tactic action. If the specified range doesn't correspond to
-    existing goals, fails with [NoSuchGoals] (a user error). this
-    exception is caught at toplevel with a default message + a hook
-    message that can be customized by [set_nosuchgoals_hook] below.
-    This hook is used to add a suggestion about bullets when
-    applicable. *)
-exception NoSuchGoals of int
-val set_nosuchgoals_hook: (int -> string option) -> unit
-
-val tclFOCUS : int -> int -> 'a tactic -> 'a tactic
-
-(** [tclFOCUSID x t] applies [t] on a (single) focused goal like
-    {!tclFOCUS}. The goal is found by its name rather than its
-    number.*)
-val tclFOCUSID : Names.Id.t -> 'a tactic -> 'a tactic
-
-(** [tclTRYFOCUS i j t] behaves like {!tclFOCUS}, except that if the
-    specified range doesn't correspond to existing goals, behaves like
-    [tclUNIT ()] instead of failing. *)
-val tclTRYFOCUS : int -> int -> unit tactic -> unit tactic
-
-
-(** {7 Dispatching on goals} *)
-
-(** Dispatch tacticals are used to apply a different tactic to each
-    goal under focus. They come in two flavours: [tclDISPATCH] takes a
-    list of [unit tactic]-s and build a [unit tactic]. [tclDISPATCHL]
-    takes a list of ['a tactic] and returns an ['a list tactic].
-
-    They both work by applying each of the tactic in a focus
-    restricted to the corresponding goal (starting with the first
-    goal). In the case of [tclDISPATCHL], the tactic returns a list of
-    the same size as the argument list (of tactics), each element
-    being the result of the tactic executed in the corresponding goal.
-
-    When the length of the tactic list is not the number of goal,
-    raises [SizeMismatch (g,t)] where [g] is the number of available
-    goals, and [t] the number of tactics passed. *)
-exception SizeMismatch of int*int
-val tclDISPATCH : unit tactic list -> unit tactic
-val tclDISPATCHL : 'a tactic list -> 'a list tactic
-
-(** [tclEXTEND b r e] is a variant of {!tclDISPATCH}, where the [r]
-    tactic is "repeated" enough time such that every goal has a tactic
-    assigned to it ([b] is the list of tactics applied to the first
-    goals, [e] to the last goals, and [r] is applied to every goal in
-    between). *)
-val tclEXTEND : unit tactic list -> unit tactic -> unit tactic list -> unit tactic
-
-(** [tclINDEPENDENT tac] runs [tac] on each goal successively, from
-    the first one to the last one. Backtracking in one goal is
-    independent of backtracking in another. It is equivalent to
-    [tclEXTEND [] tac []]. *)
-val tclINDEPENDENT : unit tactic -> unit tactic
-
-
-(** {7 Goal manipulation} *)
-
-(** Shelves all the goals under focus. The goals are placed on the
-    shelf for later use (or being solved by side-effects). *)
-val shelve : unit tactic
-
-(** Shelves the unifiable goals under focus, i.e. the goals which
-    appear in other goals under focus (the unfocused goals are not
-    considered). *)
-val shelve_unifiable : unit tactic
-
-(** [guard_no_unifiable] fails with error [UnresolvedBindings] if some
-    goals are unifiable (see {!shelve_unifiable}) in the current focus. *)
-val guard_no_unifiable : unit tactic
-
-(** [unshelve l p] adds all the goals in [l] at the end of the focused
-    goals of p *)
-val unshelve : Goal.goal list -> proofview -> proofview
-
-(** [with_shelf tac] executes [tac] and returns its result together with the set
-    of goals shelved by [tac]. The current shelf is unchanged. *)
-val with_shelf : 'a tactic -> (Goal.goal list * 'a) tactic
-
-(** If [n] is positive, [cycle n] puts the [n] first goal last. If [n]
-    is negative, then it puts the [n] last goals first.*)
-val cycle : int -> unit tactic
-
-(** [swap i j] swaps the position of goals number [i] and [j]
-    (negative numbers can be used to address goals from the end. Goals
-    are indexed from [1]. For simplicity index [0] corresponds to goal
-    [1] as well, rather than raising an error. *)
-val swap : int -> int -> unit tactic
-
-(** [revgoals] reverses the list of focused goals. *)
-val revgoals : unit tactic
-
-(** [numgoals] returns the number of goals under focus. *)
-val numgoals : int tactic
-
-
-(** {7 Access primitives} *)
-
-(** [tclEVARMAP] doesn't affect the proof, it returns the current
-    [evar_map]. *)
-val tclEVARMAP : Evd.evar_map tactic
-
-(** [tclENV] doesn't affect the proof, it returns the current
-    environment. It is not the environment of a particular goal,
-    rather the "global" environment of the proof. The goal-wise
-    environment is obtained via {!Proofview.Goal.env}. *)
-val tclENV : Environ.env tactic
-
-
-(** {7 Put-like primitives} *)
-
-(** [tclEFFECTS eff] add the effects [eff] to the current state. *)
-val tclEFFECTS : Safe_typing.private_constants -> unit tactic
-
-(** [mark_as_unsafe] declares the current tactic is unsafe. *)
-val mark_as_unsafe : unit tactic
-
-(** Gives up on the goal under focus. Reports an unsafe status. Proofs
-    with given up goals cannot be closed. *)
-val give_up : unit tactic
-
-
-(** {7 Control primitives} *)
-
-(** [tclPROGRESS t] checks the state of the proof after [t]. It it is
-    identical to the state before, then [tclePROGRESS t] fails, otherwise
-    it succeeds like [t]. *)
-val tclPROGRESS : 'a tactic -> 'a tactic
-
-(** Checks for interrupts *)
-val tclCHECKINTERRUPT : unit tactic
-
-exception Timeout
-(** [tclTIMEOUT n t] can have only one success.
-    In case of timeout if fails with [tclZERO Timeout]. *)
-val tclTIMEOUT : int -> 'a tactic -> 'a tactic
-
-(** [tclTIME s t] displays time for each atomic call to t, using s as an
-    identifying annotation if present *)
-val tclTIME : string option -> 'a tactic -> 'a tactic
-
-(** {7 Unsafe primitives} *)
-
-(** The primitives in the [Unsafe] module should be avoided as much as
-    possible, since they can make the proof state inconsistent. They are
-    nevertheless helpful, in particular when interfacing the pretyping and
-    the proof engine. *)
-module Unsafe : sig
-
-  (** [tclEVARS sigma] replaces the current [evar_map] by [sigma]. If
-      [sigma] has new unresolved [evar]-s they will not appear as
-      goal. If goals have been solved in [sigma] they will still
-      appear as unsolved goals. *)
-  val tclEVARS : Evd.evar_map -> unit tactic
-    
-  (** Like {!tclEVARS} but also checks whether goals have been solved. *)
-  val tclEVARSADVANCE : Evd.evar_map -> unit tactic
-
-  (** [tclNEWGOALS gls] adds the goals [gls] to the ones currently
-      being proved, appending them to the list of focused goals. If a
-      goal is already solved, it is not added. *)
-  val tclNEWGOALS : Goal.goal list -> unit tactic
-
-  (** [tclSETGOALS gls] sets goals [gls] as the goals being under focus. If a
-      goal is already solved, it is not set. *)
-  val tclSETGOALS : Goal.goal list -> unit tactic
-
-  (** [tclGETGOALS] returns the list of goals under focus. *)
-  val tclGETGOALS : Goal.goal list tactic
-
-  (** Sets the evar universe context. *)
-  val tclEVARUNIVCONTEXT : Evd.evar_universe_context -> unit tactic
-
-  (** Clears the future goals store in the proof view. *)
-  val reset_future_goals : proofview -> proofview
-
-  (** Give an evar the status of a goal (changes its source location
-      and makes it unresolvable for type classes. *)
-  val mark_as_goal : proofview -> Evar.t -> proofview
-end
-
-(** {7 Notations} *)
-
-module Notations : sig
-
-  (** {!tclBIND} *)
-  val (>>=) : 'a tactic -> ('a -> 'b tactic) -> 'b tactic
-  (** {!tclTHEN} *)
-  val (<*>) : unit tactic -> 'a tactic -> 'a tactic
-  (** {!tclOR}: [t1+t2] = [tclOR t1 (fun _ -> t2)]. *)
-  val (<+>) : 'a tactic -> 'a tactic -> 'a tactic
-
-end
-
-
-(** {6 Goal-dependent tactics} *)
-
-module Goal : sig
-
-  (** The type of goals. The parameter type is a phantom argument indicating
-      whether the data contained in the goal has been normalized w.r.t. the
-      current sigma. If it is the case, it is flagged [ `NF ]. You may still
-      access the un-normalized data using {!assume} if you known you do not rely
-      on the assumption of being normalized, at your own risk. *)
-  type 'a t
-
-  (** Assume that you do not need the goal to be normalized. *)
-  val assume : 'a t -> [ `NF ] t
-
-  (** Normalises the argument goal. *)
-  val normalize : 'a t -> [ `NF ] t tactic
-
-  (** [concl], [hyps], [env] and [sigma] given a goal [gl] return
-      respectively the conclusion of [gl], the hypotheses of [gl], the
-      environment of [gl] (i.e. the global environment and the
-      hypotheses) and the current evar map. *)
-  val concl : [ `NF ] t -> Term.constr
-  val hyps : [ `NF ] t -> Context.named_context
-  val env : 'a t -> Environ.env
-  val sigma : 'a t -> Evd.evar_map
-  val extra : 'a t -> Evd.Store.t
-
-  (** Returns the goal's conclusion even if the goal is not
-      normalised. *)
-  val raw_concl : 'a t -> Term.constr
-
-  (** [nf_enter t] applies the goal-dependent tactic [t] in each goal
-      independently, in the manner of {!tclINDEPENDENT} except that
-      the current goal is also given as an argument to [t]. The goal
-      is normalised with respect to evars. *)
-  val nf_enter : ([ `NF ] t -> unit tactic) -> unit tactic
-
-  (** Like {!nf_enter}, but does not normalize the goal beforehand. *)
-  val enter : ([ `LZ ] t -> unit tactic) -> unit tactic
-
-  (** Recover the list of current goals under focus, without evar-normalization *)
-  val goals : [ `LZ ] t tactic list tactic
-
-  (** Compatibility: avoid if possible *)
-  val goal : [ `NF ] t -> Evar.t
-
-end
-
-
-(** {6 The refine tactic} *)
-
-module Refine : sig
-
-  (** Printer used to print the constr which refine refines. *)
-  val pr_constr :
-    (Environ.env -> Evd.evar_map -> Term.constr -> Pp.std_ppcmds) Hook.t
-
-  (** {7 Refinement primitives} *)
-
-  val refine : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * Constr.t) -> unit tactic
-  (** In [refine ?unsafe 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. Exception
-      raised during the interpretation of [t] are caught and result in
-      tactic failures. If [unsafe] is [true] (default) [t] is
-      type-checked beforehand. *)
-
-  (** {7 Helper functions} *)
-
-  val with_type : Environ.env -> Evd.evar_map ->
-    Term.constr -> Term.types -> Evd.evar_map * Term.constr
-  (** [with_type env sigma c t] ensures that [c] is of type [t]
-      inserting a coercion if needed. *)
-
-  val refine_casted : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map*Constr.t) -> unit tactic
-  (** Like {!refine} except the refined term is coerced to the conclusion of the
-      current goal. *)
-
-end
-
-
-(** {6 Trace} *)
-
-module Trace : sig
-
-  (** [record_info_trace t] behaves like [t] except the [info] trace
-      is stored. *)
-  val record_info_trace : 'a tactic -> 'a tactic
-
-  val log : Proofview_monad.lazy_msg -> unit tactic
-  val name_tactic : Proofview_monad.lazy_msg -> 'a tactic -> 'a tactic
-
-  val pr_info : ?lvl:int -> Proofview_monad.Info.tree -> Pp.std_ppcmds
-
-end
-
-
-(** {6 Non-logical state} *)
-
-(** The [NonLogical] module allows the execution of effects (including
-    I/O) in tactics (non-logical side-effects are not discarded at
-    failures). *)
-module NonLogical : module type of Logic_monad.NonLogical
-
-(** [tclLIFT c] is a tactic which behaves exactly as [c]. *)
-val tclLIFT : 'a NonLogical.t -> 'a tactic
-
-
-(**/**)
-
-(*** Compatibility layer with <= 8.2 tactics ***)
-module V82 : sig
-  type tac = Evar.t Evd.sigma -> Evar.t list Evd.sigma
-  val tactic : tac -> unit tactic
-
-  (* normalises the evars in the goals, and stores the result in
-     solution. *)
-  val nf_evar_goals : unit tactic
-
-  val has_unresolved_evar : proofview -> bool
-
-  (* Main function in the implementation of Grab Existential Variables.
-     Resets the proofview's goals so that it contains all unresolved evars
-     (in chronological order of insertion). *)
-  val grab : proofview -> proofview
-
-  (* Returns the open goals of the proofview together with the evar_map to 
-     interpret them. *)
-  val goals : proofview -> Evar.t list Evd.sigma
-
-  val top_goals : entry -> proofview -> Evar.t list Evd.sigma
-  
-  (* returns the existential variable used to start the proof *)
-  val top_evars : entry -> Evd.evar list
-    
-  (* Implements the Existential command *)
-  val instantiate_evar : int -> Constrexpr.constr_expr -> proofview -> proofview
-
-  (* Caution: this function loses quite a bit of information. It
-     should be avoided as much as possible.  It should work as
-     expected for a tactic obtained from {!V82.tactic} though. *)
-  val of_tactic : 'a tactic -> tac
-
-  (* marks as unsafe if the argument is [false] *)
-  val put_status : bool -> unit tactic
-
-  (* exception for which it is deemed to be safe to transmute into
-     tactic failure. *)
-  val catchable_exception : exn -> bool
-
-  (* transforms every Ocaml (catchable) exception into a failure in
-     the monad. *)
-  val wrap_exceptions : (unit -> 'a tactic) -> 'a tactic
-end
diff --git a/proofs/proofview_monad.ml b/proofs/proofview_monad.ml
deleted file mode 100644
index e9bc7761..00000000
--- a/proofs/proofview_monad.ml
+++ /dev/null
@@ -1,275 +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        *)
-(************************************************************************)
-
-(** This file defines the datatypes used as internal states by the
-    tactic monad, and specialises the [Logic_monad] to these type. *)
-
-(** {6 Trees/forest for traces} *)
-
-module Trace = struct
-
-  (** The intent is that an ['a forest] is a list of messages of type
-      ['a]. But messages can stand for a list of more precise
-      messages, hence the structure is organised as a tree. *)
-  type 'a forest = 'a tree list
-  and  'a tree   = Seq of 'a * 'a forest
-
-  (** To build a trace incrementally, we use an intermediary data
-      structure on which we can define an S-expression like language
-      (like a simplified xml except the closing tags do not carry a
-      name). Note that nodes are built from right to left in ['a
-      incr], the result is mirrored when returning so that in the
-      exposed interface, the forest is read from left to right.
-
-      Concretely, we want to add a new tree to a forest: and we are
-      building it by adding new trees to the left of its left-most
-      subtrees which is built the same way. *)
-  type 'a incr = { head:'a forest ; opened: 'a tree list }
-
-  (** S-expression like language as ['a incr] transformers. It is the
-      responsibility of the library builder not to use [close] when no
-      tag is open. *)
-  let empty_incr = { head=[] ; opened=[] }
-  let opn a { head ; opened } = { head ; opened = Seq(a,[])::opened }
-  let close { head ; opened } =
-    match opened with
-    | [a] -> { head = a::head ; opened=[] }
-    | a::Seq(b,f)::opened -> { head ; opened=Seq(b,a::f)::opened }
-    | [] -> assert false
-  let leaf a s = close (opn a s)
-
-  (** Returning a forest. It is the responsibility of the library
-      builder to close all the tags. *)
-  (* spiwack: I may want to close the tags instead, to deal with
-     interruptions. *)
-  let rec mirror f = List.rev_map mirror_tree f
-  and mirror_tree (Seq(a,f)) = Seq(a,mirror f)
-
-  let to_tree = function
-    | { head ; opened=[] } -> mirror head
-    | { head ; opened=_::_} -> assert false
-
-end
-
-
-
-(** {6 State types} *)
-
-(** We typically label nodes of [Trace.tree] with messages to
-    print. But we don't want to compute the result. *)
-type lazy_msg = unit -> Pp.std_ppcmds
-let pr_lazy_msg msg = msg ()
-
-(** Info trace. *)
-module Info = struct
-
-  (** The type of the tags for [info]. *)
-  type tag =
-    | Msg of lazy_msg (** A simple message *)
-    | Tactic of lazy_msg (** A tactic call *)
-    | Dispatch  (** A call to [tclDISPATCH]/[tclEXTEND] *)
-    | DBranch  (** A special marker to delimit individual branch of a dispatch. *)
-
-  type state = tag Trace.incr
-  type tree = tag Trace.forest
-
-
-
-  let pr_in_comments m = Pp.(str"(* "++pr_lazy_msg m++str" *)")
-
-  let unbranch = function
-    | Trace.Seq (DBranch,brs) -> brs
-    | _ -> assert false
-
-
-  let is_empty_branch = let open Trace in function
-    | Seq(DBranch,[]) -> true
-    | _ -> false
-
-  (** Dispatch with empty branches are (supposed to be) equivalent to
-      [idtac] which need not appear, so they are removed from the
-      trace. *)
-  let dispatch brs =
-    let open Trace in
-    if CList.for_all is_empty_branch brs then None
-    else Some (Seq(Dispatch,brs))
-
-  let constr = let open Trace in function
-    | Dispatch -> dispatch
-    | t -> fun br -> Some (Seq(t,br))
-
-  let rec compress_tree = let open Trace in function
-    | Seq(t,f) -> constr t (compress f)
-  and compress f =
-    CList.map_filter compress_tree f
-
-  let rec is_empty = let open Trace in function
-    | Seq(Dispatch,brs) -> List.for_all is_empty brs
-    | Seq(DBranch,br) -> List.for_all is_empty br
-    | _ -> false
-
-  (** [with_sep] is [true] when [Tactic m] must be printed with a
-      trailing semi-colon. *)
-  let rec pr_tree with_sep = let open Trace in function
-    | Seq (Msg m,[]) -> pr_in_comments m
-    | Seq (Tactic m,_) ->
-        let tail = if with_sep then Pp.str";" else Pp.mt () in
-        Pp.(pr_lazy_msg m ++ tail)
-    | Seq (Dispatch,brs) ->
-        let tail = if with_sep then Pp.str";" else Pp.mt () in
-        Pp.(pr_dispatch brs++tail)
-    | Seq (Msg _,_::_) | Seq (DBranch,_) -> assert false
-  and pr_dispatch brs =
-    let open Pp in
-    let brs = List.map unbranch brs in
-    match brs with
-    | [br] -> pr_forest br
-    | _ ->
-        let sep () = spc()++str"|"++spc() in
-        let branches = prlist_with_sep sep pr_forest brs in
-        str"[>"++spc()++branches++spc()++str"]"
-  and pr_forest = function
-    | [] -> Pp.mt ()
-    | [tr] -> pr_tree false tr
-    | tr::l -> Pp.(pr_tree true tr ++ pr_forest l)
-
-  let print f =
-    pr_forest (compress f)
-
-  let rec collapse_tree n t =
-    let open Trace in
-    match n , t with
-    | 0 , t -> [t]
-    | _ , (Seq(Tactic _,[]) as t) -> [t]
-    | n , Seq(Tactic _,f) -> collapse (pred n) f
-    | n , Seq(Dispatch,brs) -> [Seq(Dispatch, (collapse n brs))]
-    | n , Seq(DBranch,br) -> [Seq(DBranch, (collapse n br))]
-    | _ , (Seq(Msg _,_) as t) -> [t]
-  and collapse n f =
-    CList.map_append (collapse_tree n) f
-end
-
-
-(** Type of proof views: current [evar_map] together with the list of
-    focused goals. *)
-type proofview = {
-  solution : Evd.evar_map;
-  comb : Goal.goal list;
-  shelf : Goal.goal list;
-}
-
-(** {6 Instantiation of the logic monad} *)
-
-(** Parameters of the logic monads *)
-module P = struct
-
-  type s = proofview * Environ.env
-
-  (** Recording info trace (true) or not. *)
-  type e = bool
-
-  (** Status (safe/unsafe) * shelved goals * given up *)
-  type w = bool * Evar.t list
-
-  let wunit = true , []
-  let wprod (b1, g1) (b2, g2) = b1 && b2 , g1@g2
-
-  type u = Info.state
-
-  let uunit = Trace.empty_incr
-
-end
-
-module Logical = Logic_monad.Logical(P)
-
-
-(** {6 Lenses to access to components of the states} *)
-
-module type State = sig
-  type t
-  val get : t Logical.t
-  val set : t -> unit Logical.t
-  val modify : (t->t) -> unit Logical.t
-end
-
-module type Writer = sig
-  type t
-  val put : t -> unit Logical.t
-end
-
-module Pv : State with type t := proofview = struct
-  let get = Logical.(map fst get)
-  let set p = Logical.modify (fun (_,e) -> (p,e))
-  let modify f= Logical.modify (fun (p,e) -> (f p,e))
-end
-
-module Solution : State with type t := Evd.evar_map = struct
-  let get = Logical.map (fun {solution} -> solution) Pv.get
-  let set s = Pv.modify (fun pv -> { pv with solution = s })
-  let modify f = Pv.modify (fun pv -> { pv with solution = f pv.solution })
-end
-
-module Comb : State with type t = Evar.t list = struct
-    (* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *)
-  type t = Evar.t list
-  let get = Logical.map (fun {comb} -> comb) Pv.get
-  let set c = Pv.modify (fun pv -> { pv with comb = c })
-  let modify f = Pv.modify (fun pv -> { pv with comb = f pv.comb })
-end
-
-module Env : State with type t := Environ.env = struct
-  let get = Logical.(map snd get)
-  let set e = Logical.modify (fun (p,_) -> (p,e))
-  let modify f = Logical.modify (fun (p,e) -> (p,f e))
-end
-
-module Status : Writer with type t := bool = struct
-  let put s = Logical.put (s, [])
-end
-
-module Shelf : State with type t = Evar.t list = struct
-    (* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *)
-  type t = Evar.t list
-  let get = Logical.map (fun {shelf} -> shelf) Pv.get
-  let set c = Pv.modify (fun pv -> { pv with shelf = c })
-  let modify f = Pv.modify (fun pv -> { pv with shelf = f pv.shelf })
-end
-
-module Giveup : Writer with type t = Evar.t list = struct
-    (* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *)
-  type t = Evar.t list
-  let put gs = Logical.put (true, gs)
-end
-
-(** Lens and utilies pertaining to the info trace *)
-module InfoL = struct
-  let recording = Logical.current
-  let if_recording t =
-    let open Logical in
-    recording >>= fun r ->
-    if r then t else return ()
-
-  let record_trace t = Logical.local true t
-
-  let raw_update = Logical.update
-  let update f = if_recording (raw_update f)
-  let opn a = update (Trace.opn a)
-  let close = update Trace.close
-  let leaf a = update (Trace.leaf a)
-
-  let tag a t =
-    let open Logical in
-    recording >>= fun r ->
-    if r then begin
-      raw_update (Trace.opn a) >>
-      t >>= fun a ->
-      raw_update Trace.close >>
-      return a
-    end else
-      t
-end
diff --git a/proofs/proofview_monad.mli b/proofs/proofview_monad.mli
deleted file mode 100644
index 7a6ea10f..00000000
--- a/proofs/proofview_monad.mli
+++ /dev/null
@@ -1,148 +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        *)
-(************************************************************************)
-
-(** This file defines the datatypes used as internal states by the
-    tactic monad, and specialises the [Logic_monad] to these type. *)
-
-(** {6 Traces} *)
-
-module Trace : sig
-
-  (** The intent is that an ['a forest] is a list of messages of type
-      ['a]. But messages can stand for a list of more precise
-      messages, hence the structure is organised as a tree. *)
-  type 'a forest = 'a tree list
-  and  'a tree   = Seq of 'a * 'a forest
-
-  (** To build a trace incrementally, we use an intermediary data
-      structure on which we can define an S-expression like language
-      (like a simplified xml except the closing tags do not carry a
-      name). *)
-  type 'a incr
-  val to_tree : 'a incr -> 'a forest
-
-  (** [open a] opens a tag with name [a]. *)
-  val opn : 'a -> 'a incr -> 'a incr
-
-  (** [close] closes the last open tag. It is the responsibility of
-      the user to close all the tags. *)
-  val close : 'a incr -> 'a incr
-
-  (** [leaf] creates an empty tag with name [a]. *)
-  val leaf : 'a -> 'a incr -> 'a incr
-
-end
-
-(** {6 State types} *)
-
-(** We typically label nodes of [Trace.tree] with messages to
-    print. But we don't want to compute the result. *)
-type lazy_msg = unit -> Pp.std_ppcmds
-
-(** Info trace. *)
-module Info : sig
-
-  (** The type of the tags for [info]. *)
-  type tag =
-    | Msg of lazy_msg (** A simple message *)
-    | Tactic of lazy_msg (** A tactic call *)
-    | Dispatch  (** A call to [tclDISPATCH]/[tclEXTEND] *)
-    | DBranch  (** A special marker to delimit individual branch of a dispatch. *)
-
-  type state = tag Trace.incr
-  type tree = tag Trace.forest
-
-  val print : tree -> Pp.std_ppcmds
-
-  (** [collapse n t] flattens the first [n] levels of [Tactic] in an
-      info trace, effectively forgetting about the [n] top level of
-      names (if there are fewer, the last name is kept). *)
-  val collapse : int -> tree -> tree
-
-end
-
-(** Type of proof views: current [evar_map] together with the list of
-    focused goals. *)
-type proofview = {
-  solution : Evd.evar_map;
-  comb : Goal.goal list;
-  shelf : Goal.goal list;
-}
-
-(** {6 Instantiation of the logic monad} *)
-
-module P : sig
-  type s = proofview * Environ.env
-
-  (** Status (safe/unsafe) * given up *)
-  type w = bool * Evar.t list
-
-  val wunit : w
-  val wprod : w -> w -> w
-
-  (** Recording info trace (true) or not. *)
-  type e = bool
-
-  type u = Info.state
-
-  val uunit : u
-end
-
-module Logical : module type of Logic_monad.Logical(P)
-
-
-(** {6 Lenses to access to components of the states} *)
-
-module type State = sig
-  type t
-  val get : t Logical.t
-  val set : t -> unit Logical.t
-  val modify : (t->t) -> unit Logical.t
-end
-
-module type Writer = sig
-  type t
-  val put : t -> unit Logical.t
-end
-
-(** Lens to the [proofview]. *)
-module Pv : State with type t := proofview
-
-(** Lens to the [evar_map] of the proofview. *)
-module Solution : State with type t := Evd.evar_map
-
-(** Lens to the list of focused goals. *)
-module Comb : State with type t = Evar.t list
-
-(** Lens to the global environment. *)
-module Env : State with type t := Environ.env
-
-(** Lens to the tactic status ([true] if safe, [false] if unsafe) *)
-module Status : Writer with type t := bool
-
-(** Lens to the list of goals which have been shelved during the
-    execution of the tactic. *)
-module Shelf : State with type t = Evar.t list
-
-(** Lens to the list of goals which were given up during the execution
-    of the tactic. *)
-module Giveup : Writer with type t = Evar.t list
-
-(** Lens and utilies pertaining to the info trace *)
-module InfoL : sig
-  (** [record_trace t] behaves like [t] and compute its [info] trace. *)
-  val record_trace : 'a Logical.t -> 'a Logical.t
-
-  val update : (Info.state -> Info.state) -> unit Logical.t
-  val opn : Info.tag -> unit Logical.t
-  val close : unit Logical.t
-  val leaf : Info.tag -> unit Logical.t
-
-  (** [tag a t] opens tag [a] runs [t] then closes the tag. *)
-  val tag : Info.tag -> 'a Logical.t -> 'a Logical.t
-end
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index ea21917a..72cb05f1 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Names
 open Term
@@ -17,7 +17,7 @@ open Genredexpr
 open Pattern
 open Reductionops
 open Tacred
-open Closure
+open CClosure
 open RedFlags
 open Libobject
 open Misctypes
@@ -29,17 +29,22 @@ let cbv_vm env sigma c =
     error "vm_compute does not support existential variables.";
   Vnorm.cbv_vm env c ctyp
 
+let warn_native_compute_disabled =
+  CWarnings.create ~name:"native-compute-disabled" ~category:"native-compiler"
+  (fun () ->
+   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
-    let () = msg_warning (str "native_compute disabled at configure time; falling back to vm_compute.") in
-    cbv_vm env sigma c
+    (warn_native_compute_disabled ();
+     cbv_vm env sigma c)
   else
     let ctyp = Retyping.get_type_of env sigma c in
     Nativenorm.native_norm env sigma c ctyp
 
 let whd_cbn flags env sigma t =
   let (state,_) =
-    (whd_state_gen true flags env sigma (t,Reductionops.Stack.empty))
+    (whd_state_gen true true flags env sigma (t,Reductionops.Stack.empty))
   in Reductionops.Stack.zip ~refold:true state
 
 let strong_cbn flags =
@@ -141,7 +146,9 @@ let make_flag_constant = function
 let make_flag env f =
   let red = no_red in
   let red = if f.rBeta then red_add red fBETA else red in
-  let red = if f.rIota then red_add red fIOTA else red in
+  let red = if f.rMatch then red_add red fMATCH else red in
+  let red = if f.rFix then red_add red fFIX else red in
+  let red = if f.rCofix then red_add red fCOFIX else red in
   let red = if f.rZeta then red_add red fZETA else red in
   let red =
     if f.rDelta then (* All but rConst *)
@@ -158,8 +165,6 @@ let make_flag env f =
 	  f.rConst red
   in red
 
-let is_reference = function PRef _ | PVar _ -> true | _ -> false
-
 (* table of custom reductino fonctions, not synchronized,
    filled via ML calls to [declare_reduction] *)
 let reduction_tab = ref String.Map.empty
@@ -196,7 +201,7 @@ let out_arg = function
 let out_with_occurrences (occs,c) =
   (Locusops.occurrences_map (List.map out_arg) occs, c)
 
-let e_red f env evm c = evm, f env evm c
+let e_red f = { e_redfun = fun env evm c -> Sigma.here (f env (Sigma.to_evar_map evm) c) evm }
 
 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.
@@ -211,6 +216,11 @@ let contextualize f g = function
       e_red (contextually b (l,c) (fun _ -> h))
   | None -> e_red g
 
+let warn_simpl_unfolding_modifiers =
+  CWarnings.create ~name:"simpl-unfolding-modifiers" ~category:"tactics"
+         (fun () ->
+          Pp.strbrk "The legacy simpl ignores constant unfolding modifiers.")
+
 let reduction_of_red_expr env =
   let make_flag = make_flag env in
   let rec reduction_of_red_expr = function
@@ -223,7 +233,7 @@ let reduction_of_red_expr env =
      let am = if !simplIsCbn then strong_cbn (make_flag f) else simpl in
      let () =
        if not (!simplIsCbn || List.is_empty f.rConst) then
-	 Pp.msg_warning (Pp.strbrk "The legacy simpl does not deal with delta flags.") in
+	 warn_simpl_unfolding_modifiers () in
      (contextualize (if head_style then whd_am else am) am o,DEFAULTcast)
   | Cbv f -> (e_red (cbv_norm_flags (make_flag f)),DEFAULTcast)
   | Cbn f ->
diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli
index b9191108..d4c2c4a6 100644
--- a/proofs/redexpr.mli
+++ b/proofs/redexpr.mli
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(** Interpretation layer of redexprs such as hnf, cbv, etc. *)
+
 open Names
 open Term
 open Pattern
diff --git a/proofs/refine.ml b/proofs/refine.ml
new file mode 100644
index 00000000..3f552706
--- /dev/null
+++ b/proofs/refine.ml
@@ -0,0 +1,162 @@
+(************************************************************************)
+(*  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 Util
+open Sigma.Notations
+open Proofview.Notations
+open 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
+  let rec share l1 l2 accu = match l1, l2 with
+  | d1 :: l1, d2 :: l2 ->
+    if d1 == d2 then share l1 l2 (d1 :: accu)
+    else (accu, d2 :: l2)
+  | _ -> (accu, l2)
+  in
+  share ctx1 ctx2 []
+
+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 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
+    in
+    (!evdref, Environ.push_named decl env)
+  in
+  let (common, changed) = extract_prefix env info in
+  let env = Environ.reset_with_named_context (Environ.val_of_named_context common) env in
+  let (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
+  !evdref
+
+let typecheck_proof c concl env sigma =
+  let evdref = ref sigma in
+  let () = Typing.e_check env evdref c concl in
+  !evdref
+
+let (pr_constrv,pr_constr) =
+  Hook.make ~default:(fun _env _sigma _c -> Pp.str"<constr>") ()
+
+(* Get the side-effect's constant declarations to update the monad's
+  * environmnent *)
+let add_if_undefined kn cb env =
+  try ignore(Environ.lookup_constant kn env); env
+  with Not_found -> Environ.add_constant kn cb env
+
+(* Add the side effects to the monad's environment, if not already done. *)
+let add_side_effect env = function
+  | { Entries.eff = Entries.SEsubproof (kn, cb, eff_env) } ->
+    add_if_undefined kn cb env
+  | { Entries.eff = Entries.SEscheme (l,_) } ->
+    List.fold_left (fun env (_,kn,cb,eff_env) ->
+        add_if_undefined kn cb env) env l
+
+let add_side_effects env effects =
+  List.fold_left (fun env eff -> add_side_effect env eff) env effects
+
+let make_refine_enter ?(unsafe = true) f =
+  { enter = fun gl ->
+  let gl = Proofview.Goal.assume gl in
+  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
+  (** 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
+  (** 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
+  (** 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
+  (** Check that the refined term is typesafe *)
+  let sigma = if unsafe then sigma else typecheck_proof c concl env 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
+  (** Proceed to the refinement *)
+  let sigma = match evkmain with
+    | None -> Evd.define self c sigma
+    | Some evk ->
+        let id = Evd.evar_ident self sigma in
+        let sigma = Evd.define self c sigma in
+        match id with
+        | 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
+  let sigma = CList.fold_left Proofview.Unsafe.mark_as_goal sigma 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.tclUNIT v
+  }
+
+let refine_one ?(unsafe = true) f =
+  Proofview.Goal.enter_one (make_refine_enter ~unsafe f)
+
+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)
+
+(** Useful definitions *)
+
+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
+  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 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 }
+
+(** {7 solve_constraints}
+
+  Ensure no remaining unification problems are left. Run at every "." by default. *)
+
+let solve_constraints =
+  let open Proofview in
+  tclENV >>= fun env -> tclEVARMAP >>= fun sigma ->
+   try let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in
+       Unsafe.tclEVARSADVANCE sigma
+   with e -> tclZERO e
diff --git a/proofs/refine.mli b/proofs/refine.mli
new file mode 100644
index 00000000..a44632ef
--- /dev/null
+++ b/proofs/refine.mli
@@ -0,0 +1,50 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(** The primitive refine tactic used to fill the holes in partial proofs. This
+    is the recommanded way to write tactics when the proof term is easy to
+    write down. Note that this is not the user-level refine tactic defined
+    in Ltac which is actually based on the one below. *)
+
+open Proofview
+
+(** {6 The refine tactic} *)
+
+(** Printer used to print the constr which refine refines. *)
+val pr_constr :
+  (Environ.env -> Evd.evar_map -> Term.constr -> Pp.std_ppcmds) 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
+    [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. *)
+
+val refine_one : ?unsafe:bool -> ('a * Constr.t) Sigma.run -> 'a tactic
+(** A generalization of [refine] which assumes exactly one goal under focus *)
+
+(** {7 Helper functions} *)
+
+val with_type : Environ.env -> Evd.evar_map ->
+  Term.constr -> Term.types -> Evd.evar_map * Term.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
+(** Like {!refine} except the refined term is coerced to the conclusion of the
+    current goal. *)
+
+(** {7 Unification constraint handling} *)
+
+val solve_constraints : unit tactic
+(** Solve any remaining unification problems, applying heuristics. *)
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 14493458..ea8543b0 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -7,13 +7,13 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Evd
 open Environ
 open Proof_type
 open Logic
-
+open Context.Named.Declaration
 
 let sig_it x = x.it
 let project x = x.sigma
@@ -57,7 +57,7 @@ let tclIDTAC gls = goal_goal_list gls
 
 (* the message printing identity tactic *)
 let tclIDTAC_MESSAGE s gls =
-  Pp.msg_info (hov 0 s); pp_flush (); tclIDTAC gls
+  Feedback.msg_info (hov 0 s); tclIDTAC gls
 
 (* General failure tactic *)
 let tclFAIL_s s gls = errorlabstrm "Refiner.tclFAIL_s" (str s)
@@ -197,12 +197,12 @@ 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_context = pf_hyps goal in
+  let oldhyps:Context.Named.t = 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_context list =
+  let hyps:Context.Named.t list =
     List.map (fun gl -> pf_hyps { it = gl; sigma=sigma; }) gls in
-  let cmp (i1, c1, t1) (i2, c2, t2) = Names.Id.equal i1 i2 in
+  let cmp d1 d2 = Names.Id.equal (get_id d1) (get_id d2) in
   let newhyps =
     List.map
       (fun hypl -> List.subtract cmp hypl oldhyps)
@@ -215,12 +215,13 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
     List.fold_left
     (fun acc lh -> acc ^ (if !frst then (frst:=false;"") else " | ")
       ^ (List.fold_left
-	   (fun acc (nm,_,_) -> (Names.Id.to_string nm) ^ " " ^ acc)
+	   (fun acc d -> (Names.Id.to_string (get_id d)) ^ " " ^ acc)
 	   "" lh))
     "" newhyps in
-  pp (str (emacs_str "<infoH>")
+  Feedback.msg_notice
+    (str (emacs_str "<infoH>")
       ++  (hov 0 (str s))
-      ++  (str (emacs_str "</infoH>")) ++ fnl());
+      ++  (str (emacs_str "</infoH>")));
   tclIDTAC goal;;
 
 
@@ -239,8 +240,8 @@ let tclORELSE0 t1 t2 g =
   try
     t1 g
   with (* Breakpoint *)
-    | e when Errors.noncritical e ->
-      let e = Errors.push e in catch_failerror e; t2 g
+    | e when CErrors.noncritical e ->
+      let e = CErrors.push e in catch_failerror e; t2 g
 
 (* ORELSE t1 t2 tries to apply t1 and if it fails or does not progress,
    then applies t2 *)
@@ -252,8 +253,8 @@ let tclORELSE t1 t2 = tclORELSE0 (tclPROGRESS t1) t2
 let tclORELSE_THEN t1 t2then t2else gls =
   match
     try Some(tclPROGRESS t1 gls)
-    with e when Errors.noncritical e ->
-      let e = Errors.push e in catch_failerror e; None
+    with e when CErrors.noncritical e ->
+      let e = CErrors.push e in catch_failerror e; None
   with
     | None -> t2else gls
     | Some sgl ->
@@ -283,12 +284,12 @@ let ite_gen tcal tac_if continue tac_else gl=
       try
         tac_else gl
       with
-        e' when Errors.noncritical e' -> iraise e in
+        e' when CErrors.noncritical e' -> iraise e in
   try
     tcal tac_if0 continue gl
   with (* Breakpoint *)
-  | e when Errors.noncritical e ->
-    let e = Errors.push e in catch_failerror e; tac_else0 e gl
+  | e when CErrors.noncritical e ->
+    let e = CErrors.push e in catch_failerror e; tac_else0 e gl
 
 (* Try the first tactic and, if it succeeds, continue with
    the second one, and if it fails, use the third one *)
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 13a9be59..6dcafb77 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -6,7 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Context
+(** Legacy proof engine. Do not use in newly written code. *)
+
 open Evd
 open Proof_type
 
@@ -16,7 +17,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 -> named_context
+val pf_hyps : goal sigma -> Context.Named.t
 
 val unpackage : 'a sigma -> evar_map ref * 'a
 val repackage : evar_map ref -> 'a -> 'a sigma
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index a75b6fa0..330594af 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -18,6 +18,8 @@ open Tacred
 open Proof_type
 open Logic
 open Refiner
+open Sigma.Notations
+open Context.Named.Declaration
 
 let re_sig it  gc = { it = it; sigma = gc; }
 
@@ -40,21 +42,22 @@ let pf_hyps  = Refiner.pf_hyps
 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 (fun (id,_,x) -> (id, x)) sign
+  List.map (function LocalAssum (id,x)
+                   | LocalDef (id,_,x) -> id, x)
+           sign
 
-let pf_nth_hyp_id gls n = let (id,c,t) = List.nth (pf_hyps gls) (n-1) in id
+let pf_nth_hyp_id gls n = List.nth (pf_hyps gls) (n-1) |> get_id
 
 let pf_last_hyp gl = List.hd (pf_hyps gl)
 
 let pf_get_hyp gls id =
   try
-    Context.lookup_named id (pf_hyps gls)
+    Context.Named.lookup id (pf_hyps gls)
   with Not_found ->
     raise (RefinerError (NoSuchHyp id))
 
 let pf_get_hyp_typ gls id =
-  let (_,_,ty)= (pf_get_hyp gls id) in
-  ty
+  pf_get_hyp gls id |> get_type
 
 let pf_ids_of_hyps gls = ids_of_named_context (pf_hyps gls)
 
@@ -70,7 +73,10 @@ let pf_get_new_ids ids gls =
 let pf_global gls id = Constrintern.construct_reference (pf_hyps gls) id
 
 let pf_reduction_of_red_expr gls re c =
-  (fst (reduction_of_red_expr (pf_env gls) re)) (pf_env gls) (project gls) 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 pf_apply f gls = f (pf_env gls) (project gls)
 let pf_eapply f gls x = 
@@ -78,7 +84,7 @@ let pf_eapply f gls x =
 let pf_reduce = pf_apply
 let pf_e_reduce = pf_apply
 
-let pf_whd_betadeltaiota         = pf_reduce whd_betadeltaiota
+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)
@@ -95,7 +101,7 @@ let pf_const_value              = pf_reduce (fun env _ -> constant_value_in env)
 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 = compose (pf_whd_betadeltaiota gls) (pf_get_type_of gls)
+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
@@ -115,26 +121,11 @@ let internal_cut_rev_no_check replace id t gl =
 let refine_no_check c gl =
   refiner (Refine c) gl
 
-(* This does not check dependencies *)
-let thin_no_check ids gl =
-  if List.is_empty ids then tclIDTAC gl else refiner (Thin ids) gl
-
-let move_hyp_no_check id1 id2 gl =
-  refiner (Move (id1,id2)) gl
-
-let mutual_fix f n others j gl =
-  with_check (refiner (FixRule (f,n,others,j))) gl
-
-let mutual_cofix f others j gl =
-  with_check (refiner (Cofix (f,others,j))) 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)
-let thin c             = with_check (thin_no_check c)
-let move_hyp id id'  = with_check (move_hyp_no_check id id')
 
 (* Pretty-printers *)
 
@@ -158,11 +149,15 @@ let pr_glls glls =
 (* Variants of [Tacmach] functions built with the new proof engine *)
 module New = struct
 
+  let project gl =
+    let sigma = Proofview.Goal.sigma gl in
+    Sigma.to_evar_map sigma
+
   let pf_apply f gl =
-    f (Proofview.Goal.env gl) (Proofview.Goal.sigma gl)
+    f (Proofview.Goal.env gl) (project gl)
 
   let of_old f gl =
-    f { Evd.it = Proofview.Goal.goal gl ; sigma = Proofview.Goal.sigma gl }
+    f { Evd.it = Proofview.Goal.goal gl ; sigma = project gl; }
 
   let pf_global id gl =
     (** We only check for the existence of an [id] in [hyps] *)
@@ -176,6 +171,9 @@ 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
 
@@ -192,34 +190,35 @@ module New = struct
     next_ident_away id ids
 
   let pf_get_hyp id gl =
-    let hyps = Proofview.Goal.hyps gl in
+    let hyps = Proofview.Goal.env gl in
     let sign =
-      try Context.lookup_named id hyps
+      try Environ.lookup_named id hyps
       with Not_found -> raise (RefinerError (NoSuchHyp id))
     in
     sign
 
   let pf_get_hyp_typ id gl =
-    let (_,_,ty) = pf_get_hyp id gl in
-    ty
+    pf_get_hyp id gl |> get_type
 
   let pf_hyps_types gl =
     let env = Proofview.Goal.env gl in
     let sign = Environ.named_context env in
-    List.map (fun (id,_,x) -> (id, x)) sign
+    List.map (function LocalAssum (id,x)
+                     | LocalDef (id,_,x) -> id, x)
+             sign
 
   let pf_last_hyp gl =
     let hyps = Proofview.Goal.hyps gl in
     List.hd hyps
 
-  let pf_nf_concl (gl : [ `LZ ] Proofview.Goal.t) =
+  let pf_nf_concl (gl : ([ `LZ ], 'r) 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 = Proofview.Goal.sigma gl in
+    let sigma = project gl in
     nf_evar sigma concl
 
-  let pf_whd_betadeltaiota gl t = pf_apply whd_betadeltaiota gl t
+  let pf_whd_all gl t = pf_apply whd_all gl t
 
   let pf_get_type_of gl t = pf_apply Retyping.get_type_of gl t
 
@@ -228,13 +227,13 @@ module New = struct
 
   let pf_hnf_constr gl t = pf_apply hnf_constr gl t
   let pf_hnf_type_of gl t =
-    pf_whd_betadeltaiota gl (pf_get_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_betadeltaiota gl t = pf_apply whd_betadeltaiota gl t
+  let pf_whd_all gl t = pf_apply whd_all gl t
   let pf_compute gl t = pf_apply compute gl t
 
-  let pf_nf_evar gl t = nf_evar (Proofview.Goal.sigma gl) t
+  let pf_nf_evar gl t = nf_evar (project gl) t
 
 end
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 7e943cb1..59f296f6 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -8,7 +8,6 @@
 
 open Names
 open Term
-open Context
 open Environ
 open Evd
 open Proof_type
@@ -34,18 +33,18 @@ val apply_sig_tac :
 
 val pf_concl              : goal sigma -> types
 val pf_env                : goal sigma -> env
-val pf_hyps               : goal sigma -> named_context
+val pf_hyps               : goal sigma -> Context.Named.t
 (*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 -> named_declaration
+val pf_last_hyp           : goal sigma -> Context.Named.Declaration.t
 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 -> named_declaration
+val pf_get_hyp            : goal sigma -> Id.t -> Context.Named.Declaration.t
 val pf_get_hyp_typ        : goal sigma -> Id.t -> types
 
 val pf_get_new_id  : Id.t      -> goal sigma -> Id.t
@@ -64,7 +63,7 @@ val pf_e_reduce :
   (env -> evar_map -> constr -> evar_map * constr) ->
   goal sigma -> constr -> evar_map * constr
 
-val pf_whd_betadeltaiota       : goal sigma -> constr -> constr
+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
@@ -87,18 +86,12 @@ val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool
 val refiner                   : rule -> tactic
 val internal_cut_no_check     : bool -> Id.t -> types -> tactic
 val refine_no_check           : constr -> tactic
-val thin_no_check             : Id.t list -> tactic
-val mutual_fix      :
-  Id.t -> int -> (Id.t * int * constr) list -> int -> tactic
-val mutual_cofix    : Id.t -> (Id.t * constr) list -> int -> 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
-val thin             : Id.t list -> tactic
-val move_hyp         : Id.t -> Id.t move_location -> tactic
 
 (** {6 Pretty-printing functions (debug only). } *)
 val pr_gls    : goal sigma -> Pp.std_ppcmds
@@ -106,36 +99,47 @@ val pr_glls   : goal list sigma -> Pp.std_ppcmds
 
 (* Variants of [Tacmach] functions built with the new proof engine *)
 module New : sig
-  val pf_apply : (env -> evar_map -> 'a) -> 'b Proofview.Goal.t -> 'a
-  val pf_global : identifier -> 'a Proofview.Goal.t -> constr
-  val of_old : (Proof_type.goal Evd.sigma -> 'a) -> [ `NF ] Proofview.Goal.t -> 'a
+  val pf_apply : (env -> evar_map -> 'a) -> ('b, 'r) Proofview.Goal.t -> 'a
+  val pf_global : identifier -> ('a, 'r) Proofview.Goal.t -> constr
+  (** FIXME: encapsulate the level in an existential type. *)
+  val of_old : (Proof_type.goal Evd.sigma -> 'a) -> ([ `NF ], 'r) Proofview.Goal.t -> 'a
 
-  val pf_env : 'a Proofview.Goal.t -> Environ.env
-  val pf_concl : [ `NF ] Proofview.Goal.t -> types
+  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 pf_unsafe_type_of : 'a Proofview.Goal.t -> Term.constr -> Term.types
-  val pf_type_of : 'a Proofview.Goal.t -> Term.constr -> evar_map * Term.types
-  val pf_conv_x : 'a Proofview.Goal.t -> Term.constr -> Term.constr -> bool
+  (** 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_get_new_id  : identifier -> [ `NF ] Proofview.Goal.t -> identifier
-  val pf_ids_of_hyps : 'a Proofview.Goal.t -> identifier list
-  val pf_hyps_types : 'a Proofview.Goal.t -> (identifier * types) list
+  (** 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_hyp : identifier -> [ `NF ] Proofview.Goal.t -> named_declaration
-  val pf_get_hyp_typ        : identifier -> [ `NF ] Proofview.Goal.t -> types
-  val pf_last_hyp           : [ `NF ] Proofview.Goal.t -> named_declaration
+  (** 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_nf_concl : [ `LZ ] Proofview.Goal.t -> types
-  val pf_reduce_to_quantified_ind : 'a Proofview.Goal.t -> types -> pinductive * types
+  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_hnf_constr : 'a Proofview.Goal.t -> constr -> types
-  val pf_hnf_type_of : 'a Proofview.Goal.t -> constr -> types
+  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_whd_betadeltaiota : 'a Proofview.Goal.t -> constr -> constr
-  val pf_compute : 'a Proofview.Goal.t -> constr -> constr
+  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_matches : 'a Proofview.Goal.t -> constr_pattern -> constr -> patvar_map
+  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_evar : 'a Proofview.Goal.t -> constr -> constr
+  val pf_whd_all : ('a, 'r) Proofview.Goal.t -> constr -> constr
+  val pf_compute : ('a, 'r) Proofview.Goal.t -> constr -> constr
+
+  val pf_matches : ('a, 'r) Proofview.Goal.t -> constr_pattern -> constr -> patvar_map
+
+  val pf_nf_evar : ('a, 'r) Proofview.Goal.t -> constr -> constr
 
 end
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
deleted file mode 100644
index a4a447e8..00000000
--- a/proofs/tactic_debug.ml
+++ /dev/null
@@ -1,318 +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 Util
-open Names
-open Pp
-open Tacexpr
-open Termops
-open Nameops
-
-let (prtac, tactic_printer) = Hook.make ()
-let (prmatchpatt, match_pattern_printer) = Hook.make ()
-let (prmatchrl, match_rule_printer) = Hook.make ()
-
-
-(* This module intends to be a beginning of debugger for tactic expressions.
-   Currently, it is quite simple and we can hope to have, in the future, a more
-   complete panel of commands dedicated to a proof assistant framework *)
-
-(* Debug information *)
-type debug_info =
-  | DebugOn of int
-  | DebugOff
-
-(* An exception handler *)
-let explain_logic_error = ref (fun e -> mt())
-
-let explain_logic_error_no_anomaly = ref (fun e -> mt())
-
-let msg_tac_debug s = Proofview.NonLogical.print_debug (s++fnl())
-let msg_tac_notice s = Proofview.NonLogical.print_notice (s++fnl())
-
-(* Prints the goal *)
-
-let db_pr_goal gl =
-  let env = Proofview.Goal.env gl in
-  let concl = Proofview.Goal.concl gl in
-  let penv = print_named_context env in
-  let pc = print_constr_env env concl in
-    str"  " ++ hv 0 (penv ++ fnl () ++
-                   str "============================" ++ fnl ()  ++
-                   str" "  ++ pc) ++ fnl ()
-
-let db_pr_goal =
-  Proofview.Goal.nf_enter begin fun gl ->
-  let pg = db_pr_goal gl in
-  Proofview.tclLIFT (msg_tac_notice (str "Goal:" ++ fnl () ++ pg))
-  end
-
-
-(* Prints the commands *)
-let help () =
-  msg_tac_debug (str "Commands: <Enter> = Continue" ++ fnl() ++
-         str "          h/? = Help" ++ fnl() ++
-         str "          r <num> = Run <num> times" ++ fnl() ++
-         str "          r <string> = Run up to next idtac <string>" ++ fnl() ++
-         str "          s = Skip" ++ fnl() ++
-         str "          x = Exit")
-
-(* Prints the goal and the command to be executed *)
-let goal_com tac =
-  Proofview.tclTHEN
-    db_pr_goal
-    (Proofview.tclLIFT (msg_tac_debug (str "Going to execute:" ++ fnl () ++ Hook.get prtac tac)))
-
-(* [run (new_ref _)] gives us a ref shared among [NonLogical.t]
-   expressions. It avoids parametrizing everything over a
-   reference. *)
-let skipped = Proofview.NonLogical.run (Proofview.NonLogical.ref 0)
-let skip = Proofview.NonLogical.run (Proofview.NonLogical.ref 0)
-let breakpoint = Proofview.NonLogical.run (Proofview.NonLogical.ref None)
-
-let rec drop_spaces inst i =
-  if String.length inst > i && inst.[i] == ' ' then drop_spaces inst (i+1)
-  else i
-
-let possibly_unquote s =
-  if String.length s >= 2 && s.[0] == '"' && s.[String.length s - 1] == '"' then
-    String.sub s 1 (String.length s - 2)
-  else
-    s
-
-(* (Re-)initialize debugger *)
-let db_initialize =
-  let open Proofview.NonLogical in
-  (skip:=0) >> (skipped:=0) >> (breakpoint:=None)
-
-let int_of_string s =
-  try Proofview.NonLogical.return (int_of_string s)
-  with e -> Proofview.NonLogical.raise e
-
-let string_get s i =
-  try Proofview.NonLogical.return (String.get s i)
-  with e -> Proofview.NonLogical.raise e
-
-(* Gives the number of steps or next breakpoint of a run command *)
-let run_com inst =
-  let open Proofview.NonLogical in
-  string_get inst 0 >>= fun first_char ->
-  if first_char ='r' then
-    let i = drop_spaces inst 1 in
-    if String.length inst > i then
-      let s = String.sub inst i (String.length inst - i) in
-      if inst.[0] >= '0' && inst.[0] <= '9' then
-        int_of_string s >>= fun num ->
-        (if num<0 then invalid_arg "run_com" else return ()) >>
-        (skip:=num) >> (skipped:=0)
-      else
-        breakpoint:=Some (possibly_unquote s)
-    else
-      invalid_arg "run_com"
-  else
-    invalid_arg "run_com"
-
-(* Prints the run counter *)
-let run ini =
-  let open Proofview.NonLogical in
-  if not ini then
-    begin
-      Proofview.NonLogical.print_notice (str"\b\r\b\r") >>
-      !skipped >>= fun skipped ->
-      msg_tac_debug (str "Executed expressions: " ++ int skipped ++ fnl())
-    end >>
-    !skipped >>= fun x ->
-    skipped := x+1
-  else
-    return ()
-
-(* Prints the prompt *)
-let rec prompt level =
-  (* spiwack: avoid overriding by the open below *)
-  let runtrue = run true in
-  begin
-    let open Proofview.NonLogical in
-    Proofview.NonLogical.print_notice (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ") >>
-    let exit = (skip:=0) >> (skipped:=0) >> raise Sys.Break in
-    Proofview.NonLogical.catch Proofview.NonLogical.read_line
-      begin function (e, info) -> match e with
-        | End_of_file -> exit
-        | e -> raise ~info e
-      end
-    >>= fun inst ->
-    match inst with
-    | ""  -> return (DebugOn (level+1))
-    | "s" -> return (DebugOff)
-    | "x" -> Proofview.NonLogical.print_char '\b' >> exit
-    | "h"| "?" ->
-      begin
-        help () >>
-        prompt level
-      end
-    | _ ->
-        Proofview.NonLogical.catch (run_com inst >> runtrue >> return (DebugOn (level+1)))
-          begin function (e, info) -> match e with
-            | Failure _ | Invalid_argument _ -> prompt level
-            | e -> raise ~info e
-          end
-  end
-
-(* Prints the state and waits for an instruction *)
-(* spiwack: the only reason why we need to take the continuation [f]
-   as an argument rather than returning the new level directly seems to
-   be that [f] is wrapped in with "explain_logic_error". I don't think
-   it serves any purpose in the current design, so we could just drop
-   that. *)
-let debug_prompt lev tac f =
-  (* spiwack: avoid overriding by the open below *)
-  let runfalse = run false in
-  let open Proofview.NonLogical in
-  let (>=) = Proofview.tclBIND in
-  (* What to print and to do next *)
-  let newlevel =
-    Proofview.tclLIFT !skip >= fun initial_skip ->
-    if Int.equal initial_skip 0 then
-      Proofview.tclLIFT !breakpoint >= fun breakpoint ->
-      if Option.is_empty breakpoint then Proofview.tclTHEN (goal_com tac) (Proofview.tclLIFT (prompt lev))
-      else Proofview.tclLIFT(runfalse >> return (DebugOn (lev+1)))
-    else Proofview.tclLIFT begin
-      (!skip >>= fun s -> skip:=s-1) >>
-      runfalse >>
-      !skip >>= fun new_skip ->
-      (if Int.equal new_skip 0 then skipped:=0 else return ()) >>
-      return (DebugOn (lev+1))
-    end in
-  newlevel >= fun newlevel ->
-  (* What to execute *)
-  Proofview.tclOR
-    (f newlevel)
-    begin fun (reraise, info) ->
-      Proofview.tclTHEN
-        (Proofview.tclLIFT begin
-          (skip:=0) >> (skipped:=0) >>
-            if Logic.catchable_exception reraise then
-              msg_tac_debug (str "Level " ++ int lev ++ str ": " ++ Pervasives.(!) explain_logic_error reraise)
-            else return ()
-        end)
-        (Proofview.tclZERO ~info reraise)
-    end
-
-let is_debug db =
-  let open Proofview.NonLogical in
-  !breakpoint >>= fun breakpoint ->
-  match db, breakpoint with
-  | DebugOff, _ -> return false
-  | _, Some _ -> return false
-  | _ ->
-      !skip >>= fun skip ->
-      return (Int.equal skip 0)
-
-(* Prints a constr *)
-let db_constr debug env c =
-  let open Proofview.NonLogical in
-  is_debug debug >>= fun db ->
-  if db then
-    msg_tac_debug (str "Evaluated term: " ++ print_constr_env env c)
-  else return ()
-
-(* Prints the pattern rule *)
-let db_pattern_rule debug num r =
-  let open Proofview.NonLogical in
-  is_debug debug >>= fun db ->
-  if db then
-  begin
-    msg_tac_debug (str "Pattern rule " ++ int num ++ str ":" ++ fnl () ++
-      str "|" ++ spc () ++ Hook.get prmatchrl r)
-  end
-  else return ()
-
-(* Prints the hypothesis pattern identifier if it exists *)
-let hyp_bound = function
-  | Anonymous -> str " (unbound)"
-  | Name id -> str " (bound to " ++ pr_id id ++ str ")"
-
-(* Prints a matched hypothesis *)
-let db_matched_hyp debug env (id,_,c) ido =
-  let open Proofview.NonLogical in
-  is_debug debug >>= fun db ->
-  if db then
-    msg_tac_debug (str "Hypothesis " ++ pr_id id ++ hyp_bound ido ++
-                str " has been matched: " ++ print_constr_env env c)
-  else return ()
-
-(* Prints the matched conclusion *)
-let db_matched_concl debug env c =
-  let open Proofview.NonLogical in
-  is_debug debug >>= fun db ->
-  if db then
-    msg_tac_debug (str "Conclusion has been matched: " ++ print_constr_env env c)
-  else return ()
-
-(* Prints a success message when the goal has been matched *)
-let db_mc_pattern_success debug =
-  let open Proofview.NonLogical in
-  is_debug debug >>= fun db ->
-  if db then
-    msg_tac_debug (str "The goal has been successfully matched!" ++ fnl() ++
-           str "Let us execute the right-hand side part..." ++ fnl())
-  else return ()
-
-(* Prints a failure message for an hypothesis pattern *)
-let db_hyp_pattern_failure debug env sigma (na,hyp) =
-  let open Proofview.NonLogical in
-  is_debug debug >>= fun db ->
-  if db then
-    msg_tac_debug (str "The pattern hypothesis" ++ hyp_bound na ++
-                str " cannot match: " ++
-           Hook.get prmatchpatt env sigma hyp)
-  else return ()
-
-(* Prints a matching failure message for a rule *)
-let db_matching_failure debug =
-  let open Proofview.NonLogical in
-  is_debug debug >>= fun db ->
-  if db then
-    msg_tac_debug (str "This rule has failed due to matching errors!" ++ fnl() ++
-           str "Let us try the next one...")
-  else return ()
-
-(* Prints an evaluation failure message for a rule *)
-let db_eval_failure debug s =
-  let open Proofview.NonLogical in
-  is_debug debug >>= fun db ->
-  if db then
-    let s = str "message \"" ++ s ++ str "\"" in
-    msg_tac_debug
-      (str "This rule has failed due to \"Fail\" tactic (" ++
-       s ++ str ", level 0)!" ++ fnl() ++ str "Let us try the next one...")
-  else return ()
-
-(* Prints a logic failure message for a rule *)
-let db_logic_failure debug err =
-  let open Proofview.NonLogical in
-  is_debug debug >>= fun db ->
-  if db then
-  begin
-    msg_tac_debug (Pervasives.(!) explain_logic_error err) >>
-    msg_tac_debug (str "This rule has failed due to a logic error!" ++ fnl() ++
-           str "Let us try the next one...")
-  end
-  else return ()
-
-let is_breakpoint brkname s = match brkname, s with
-  | Some s, MsgString s'::_ -> String.equal s s'
-  | _ -> false
-
-let db_breakpoint debug s =
-  let open Proofview.NonLogical in
-  !breakpoint >>= fun opt_breakpoint ->
-  match debug with
-  | DebugOn lev when not (CList.is_empty s) && is_breakpoint opt_breakpoint s ->
-      breakpoint:=None
-  | _ ->
-      return ()
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
deleted file mode 100644
index 215c5b29..00000000
--- a/proofs/tactic_debug.mli
+++ /dev/null
@@ -1,79 +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 Environ
-open Pattern
-open Names
-open Tacexpr
-open Term
-open Evd
-
-(** This module intends to be a beginning of debugger for tactic expressions.
-   Currently, it is quite simple and we can hope to have, in the future, a more
-   complete panel of commands dedicated to a proof assistant framework *)
-
-val tactic_printer : (glob_tactic_expr -> Pp.std_ppcmds) Hook.t
-val match_pattern_printer :
-  (env -> evar_map -> constr_pattern match_pattern -> Pp.std_ppcmds) Hook.t
-val match_rule_printer :
-  ((Tacexpr.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> Pp.std_ppcmds) Hook.t
-
-(** Debug information *)
-type debug_info =
-  | DebugOn of int
-  | DebugOff
-
-(** Prints the state and waits *)
-val debug_prompt :
-  int -> glob_tactic_expr -> (debug_info -> 'a Proofview.tactic) -> 'a Proofview.tactic
-
-(** Initializes debugger *)
-val db_initialize : unit Proofview.NonLogical.t
-
-(** Prints a constr *)
-val db_constr : debug_info -> env -> constr -> unit Proofview.NonLogical.t
-
-(** Prints the pattern rule *)
-val db_pattern_rule :
-  debug_info -> int -> (Tacexpr.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> unit Proofview.NonLogical.t
-
-(** Prints a matched hypothesis *)
-val db_matched_hyp :
-  debug_info -> env -> Id.t * constr option * constr -> Name.t -> unit Proofview.NonLogical.t
-
-(** Prints the matched conclusion *)
-val db_matched_concl : debug_info -> env -> constr -> unit Proofview.NonLogical.t
-
-(** Prints a success message when the goal has been matched *)
-val db_mc_pattern_success : debug_info -> unit Proofview.NonLogical.t
-
-(** Prints a failure message for an hypothesis pattern *)
-val db_hyp_pattern_failure :
-  debug_info -> env -> evar_map -> Name.t * constr_pattern match_pattern -> unit Proofview.NonLogical.t
-
-(** Prints a matching failure message for a rule *)
-val db_matching_failure : debug_info -> unit Proofview.NonLogical.t
-
-(** Prints an evaluation failure message for a rule *)
-val db_eval_failure : debug_info -> Pp.std_ppcmds -> unit Proofview.NonLogical.t
-
-(** An exception handler *)
-val explain_logic_error: (exn -> Pp.std_ppcmds) ref
-
-(** For use in the Ltac debugger: some exception that are usually
-   consider anomalies are acceptable because they are caught later in
-   the process that is being debugged.  One should not require
-   from users that they report these anomalies. *)
-val explain_logic_error_no_anomaly : (exn -> Pp.std_ppcmds) ref
-
-(** Prints a logic failure message for a rule *)
-val db_logic_failure : debug_info -> exn -> unit Proofview.NonLogical.t
-
-(** Prints a logic failure message for a rule *)
-val db_breakpoint : debug_info ->
-  Id.t Loc.located message_token list -> unit Proofview.NonLogical.t