Merge remote-tracking branch 'OFFICIAL/trunk' into morefresh

19 files changed, 4237 insertions, 898 deletions

diff --git a/engine/engine.mllib b/engine/engine.mllib
index dc7ff2a642..70b74edca3 100644
--- a/engine/engine.mllib
+++ b/engine/engine.mllib
@@ -1,5 +1,9 @@
 Logic_monad
 Termops
 Namegen
+UState
 Evd
+Sigma
 Proofview_monad
+Evarutil
+Proofview
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
new file mode 100644
index 0000000000..2bd67dcdc8
--- /dev/null
+++ b/engine/evarutil.ml
@@ -0,0 +1,723 @@
+(************************************************************************)
+(*  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 Errors
+open Util
+open Pp
+open Names
+open Term
+open Vars
+open Termops
+open Namegen
+open Pre_env
+open Environ
+open Evd
+open Sigma.Notations
+
+let safe_evar_value sigma ev =
+  try Some (Evd.existential_value sigma ev)
+  with NotInstantiatedEvar | Not_found -> None
+
+(** Combinators *)
+
+let evd_comb0 f evdref =
+  let (evd',x) = f !evdref in
+    evdref := evd';
+    x
+
+let evd_comb1 f evdref x =
+  let (evd',y) = f !evdref x in
+    evdref := evd';
+    y
+
+let evd_comb2 f evdref x y =
+  let (evd',z) = f !evdref x y in
+    evdref := evd';
+    z
+
+let e_new_global evdref x = 
+  evd_comb1 (Evd.fresh_global (Global.env())) evdref x
+
+let new_global evd x = 
+  Sigma.fresh_global (Global.env()) evd x
+
+(****************************************************)
+(* Expanding/testing/exposing existential variables *)
+(****************************************************)
+
+(* flush_and_check_evars fails if an existential is undefined *)
+
+exception Uninstantiated_evar of existential_key
+
+let rec flush_and_check_evars sigma c =
+  match kind_of_term c with
+  | Evar (evk,_ as ev) ->
+      (match existential_opt_value sigma ev with
+       | None -> raise (Uninstantiated_evar evk)
+       | Some c -> flush_and_check_evars sigma c)
+  | _ -> map_constr (flush_and_check_evars sigma) c
+
+(* let nf_evar_key = Profile.declare_profile "nf_evar"  *)
+(* let nf_evar = Profile.profile2 nf_evar_key Reductionops.nf_evar *)
+
+let rec whd_evar sigma c =
+  match kind_of_term c with
+    | Evar ev ->
+        let (evk, args) = ev in
+        let args = Array.map (fun c -> whd_evar sigma c) args in
+        (match safe_evar_value sigma (evk, args) with
+            Some c -> whd_evar sigma c
+          | None -> c)
+    | Sort (Type u) -> 
+      let u' = Evd.normalize_universe sigma u in
+	if u' == u then c else mkSort (Sorts.sort_of_univ u')
+    | Const (c', u) when not (Univ.Instance.is_empty u) -> 
+      let u' = Evd.normalize_universe_instance sigma u in
+	if u' == u then c else mkConstU (c', u')
+    | Ind (i, u) when not (Univ.Instance.is_empty u) -> 
+      let u' = Evd.normalize_universe_instance sigma u in
+	if u' == u then c else mkIndU (i, u')
+    | Construct (co, u) when not (Univ.Instance.is_empty u) ->
+      let u' = Evd.normalize_universe_instance sigma u in
+	if u' == u then c else mkConstructU (co, u')
+    | _ -> c
+
+let rec nf_evar sigma t = Constr.map (fun t -> nf_evar sigma t) (whd_evar sigma t)
+
+let j_nf_evar sigma j =
+  { uj_val = nf_evar sigma j.uj_val;
+    uj_type = nf_evar sigma j.uj_type }
+let jl_nf_evar sigma jl = List.map (j_nf_evar sigma) jl
+let jv_nf_evar sigma = Array.map (j_nf_evar sigma)
+let tj_nf_evar sigma {utj_val=v;utj_type=t} =
+  {utj_val=nf_evar sigma v;utj_type=t}
+
+let nf_evars_universes evm =
+  Universes.nf_evars_and_universes_opt_subst (safe_evar_value evm) 
+    (Evd.universe_subst evm)
+    
+let nf_evars_and_universes evm =
+  let evm = Evd.nf_constraints evm in
+    evm, nf_evars_universes evm
+
+let e_nf_evars_and_universes evdref =
+  evdref := Evd.nf_constraints !evdref;
+  nf_evars_universes !evdref, Evd.universe_subst !evdref
+
+let nf_evar_map_universes evm =
+  let evm = Evd.nf_constraints evm in
+  let subst = Evd.universe_subst evm in
+    if Univ.LMap.is_empty subst then evm, nf_evar evm
+    else
+      let f = nf_evars_universes evm in
+	Evd.raw_map (fun _ -> map_evar_info f) evm, f
+
+let nf_named_context_evar sigma ctx =
+  Context.Named.map (nf_evar sigma) ctx
+
+let nf_rel_context_evar sigma ctx =
+  Context.Rel.map (nf_evar sigma) ctx
+
+let nf_env_evar sigma env =
+  let nc' = nf_named_context_evar sigma (Environ.named_context env) in
+  let rel' = nf_rel_context_evar sigma (Environ.rel_context env) in
+    push_rel_context rel' (reset_with_named_context (val_of_named_context nc') env)
+
+let nf_evar_info evc info = map_evar_info (nf_evar evc) info
+
+let nf_evar_map evm =
+  Evd.raw_map (fun _ evi -> nf_evar_info evm evi) evm
+
+let nf_evar_map_undefined evm =
+  Evd.raw_map_undefined (fun _ evi -> nf_evar_info evm evi) evm
+
+(*-------------------*)
+(* Auxiliary functions for the conversion algorithms modulo evars
+ *)
+
+(* A probably faster though more approximative variant of
+   [has_undefined (nf_evar c)]: instances are not substituted and
+   maybe an evar occurs in an instance and it would disappear by
+   instantiation *)
+
+let has_undefined_evars evd t =
+  let rec has_ev t =
+    match kind_of_term t with
+    | Evar (ev,args) ->
+        (match evar_body (Evd.find evd ev) with
+        | Evar_defined c ->
+            has_ev c; Array.iter has_ev args
+        | Evar_empty ->
+	    raise NotInstantiatedEvar)
+    | _ -> iter_constr has_ev t in
+  try let _ = has_ev t in false
+  with (Not_found | NotInstantiatedEvar) -> true
+
+let is_ground_term evd t =
+  not (has_undefined_evars evd t)
+
+let is_ground_env evd env =
+  let open Context.Rel.Declaration in
+  let is_ground_rel_decl = function
+    | LocalDef (_,b,_) -> is_ground_term evd b
+    | _ -> true in
+  let open Context.Named.Declaration in
+  let is_ground_named_decl = function
+    | LocalDef (_,b,_) -> is_ground_term evd b
+    | _ -> true in
+  List.for_all is_ground_rel_decl (rel_context env) &&
+  List.for_all is_ground_named_decl (named_context env)
+
+(* Memoization is safe since evar_map and environ are applicative
+   structures *)
+let memo f =
+  let m = ref None in
+  fun x y -> match !m with
+  | Some (x', y', r) when x == x' && y == y' -> r
+  | _ -> let r = f x y in m := Some (x, y, r); r
+
+let is_ground_env = memo is_ground_env
+
+(* Return the head evar if any *)
+
+exception NoHeadEvar
+
+let head_evar =
+  let rec hrec c = match kind_of_term c with
+    | Evar (evk,_)   -> evk
+    | Case (_,_,c,_) -> hrec c
+    | App (c,_)      -> hrec c
+    | Cast (c,_,_)   -> hrec c
+    | _              -> raise NoHeadEvar
+  in
+  hrec
+
+(* Expand head evar if any (currently consider only applications but I
+   guess it should consider Case too) *)
+
+let whd_head_evar_stack sigma c =
+  let rec whrec (c, l as s) =
+    match kind_of_term c with
+      | Evar (evk,args as ev) ->
+        let v =
+          try Some (existential_value sigma ev)
+          with NotInstantiatedEvar | Not_found  -> None in
+        begin match v with
+        | None -> s
+        | Some c -> whrec (c, l)
+        end
+      | Cast (c,_,_) -> whrec (c, l)
+      | App (f,args) -> whrec (f, args :: l)
+      | _ -> s
+  in
+  whrec (c, [])
+
+let whd_head_evar sigma c =
+  let (f, args) = whd_head_evar_stack sigma c in
+  (** optim: don't reallocate if empty/singleton *)
+  match args with
+  | [] -> f
+  | [arg] -> mkApp (f, arg)
+  | _ -> mkApp (f, Array.concat args)
+
+(**********************)
+(* Creating new metas *)
+(**********************)
+
+let meta_counter_summary_name = "meta counter"
+
+(* Generator of metavariables *)
+let new_meta =
+  let meta_ctr = Summary.ref 0 ~name:meta_counter_summary_name in
+  fun () -> incr meta_ctr; !meta_ctr
+
+let mk_new_meta () = mkMeta(new_meta())
+
+(* The list of non-instantiated existential declarations (order is important) *)
+
+let non_instantiated sigma =
+  let listev = Evd.undefined_map sigma in
+  Evar.Map.smartmap (fun evi -> nf_evar_info sigma evi) listev
+
+(************************)
+(* Manipulating filters *)
+(************************)
+
+let make_pure_subst evi args =
+  let open Context.Named.Declaration in
+  snd (List.fold_right
+    (fun decl (args,l) ->
+      match args with
+        | a::rest -> (rest, (get_id decl, a)::l)
+        | _ -> anomaly (Pp.str "Instance does not match its signature"))
+    (evar_filtered_context evi) (Array.rev_to_list args,[]))
+
+(*------------------------------------*
+ * functional operations on evar sets *
+ *------------------------------------*)
+
+(* [push_rel_context_to_named_context] builds the defining context and the
+ * initial instance of an evar. If the evar is to be used in context
+ *
+ * Gamma =  a1     ...    an xp      ...       x1
+ *          \- named part -/ \- de Bruijn part -/
+ *
+ * then the x1...xp are turned into variables so that the evar is declared in
+ * context
+ *
+ *          a1     ...    an xp      ...       x1
+ *          \----------- named part ------------/
+ *
+ * but used applied to the initial instance "a1 ... an Rel(p) ... Rel(1)"
+ * so that ev[a1:=a1 ... an:=an xp:=Rel(p) ... x1:=Rel(1)] is correctly typed
+ * in context Gamma.
+ *
+ * Remark 1: The instance is reverted in practice (i.e. Rel(1) comes first)
+ * Remark 2: If some of the ai or xj are definitions, we keep them in the
+ *   instance. This is necessary so that no unfolding of local definitions
+ *   happens when inferring implicit arguments (consider e.g. the problem
+ *   "x:nat; x':=x; f:forall y, y=y -> Prop |- f _ (refl_equal x')" which
+ *   produces the equation "?y[x,x']=?y[x,x']" =? "x'=x'": we want
+ *   the hole to be instantiated by x', not by x (which would have been
+ *   the case in [invert_definition] if x' had disappeared from the instance).
+ *   Note that at any time, if, in some context env, the instance of
+ *   declaration x:A is t and the instance of definition x':=phi(x) is u, then
+ *   we have the property that u and phi(t) are convertible in env.
+ *)
+
+let subst2 subst vsubst c =
+  substl subst (replace_vars vsubst c)
+
+let push_rel_context_to_named_context env typ =
+  (* compute the instances relative to the named context and rel_context *)
+  let open Context.Named.Declaration in
+  let ids = List.map get_id (named_context env) in
+  let inst_vars = List.map mkVar ids in
+  let inst_rels = List.rev (rel_list 0 (nb_rel env)) in
+  let replace_var_named_declaration id0 id decl =
+    let id' = get_id decl in
+    let id' = if Id.equal id0 id' then id else id' in
+    let vsubst = [id0 , mkVar id] in
+    decl |> set_id id' |> map_constr (replace_vars vsubst)
+  in
+  let replace_var_named_context id0 id  env =
+    let nc = Environ.named_context env in
+    let nc' = List.map (replace_var_named_declaration id0 id) nc in
+    Environ.reset_with_named_context (val_of_named_context nc') env
+  in
+  let extract_if_neq id = function
+    | Anonymous -> None
+    | Name id' when id_ord id id' = 0 -> None
+    | Name id' -> Some id'
+  in
+  (* move the rel context to a named context and extend the named instance *)
+  (* with vars of the rel context *)
+  (* We do keep the instances corresponding to local definition (see above) *)
+  let (subst, vsubst, _, env) =
+    Context.Rel.fold_outside
+      (fun decl (subst, vsubst, avoid, env) ->
+        let open Context.Rel.Declaration in
+        let na = get_name decl in
+	let c = get_value decl in
+	let t = get_type decl in
+        let open Context.Named.Declaration in
+        let id =
+          (* ppedrot: we want to infer nicer names for the refine tactic, but
+             keeping at the same time backward compatibility in other code
+             using this function. For now, we only attempt to preserve the
+             old behaviour of Program, but ultimately, one should do something
+             about this whole name generation problem. *)
+          if Flags.is_program_mode () then next_name_away na avoid
+          else next_ident_away (id_of_name_using_hdchar env t na) avoid
+        in
+        match extract_if_neq id na with
+        | Some id0 when not (is_section_variable id0) ->
+            (* spiwack: if [id<>id0], rather than introducing a new
+               binding named [id], we will keep [id0] (the name given
+               by the user) and rename [id0] into [id] in the named
+               context. Unless [id] is a section variable. *)
+            let subst = List.map (replace_vars [id0,mkVar id]) subst in
+            let vsubst = (id0,mkVar id)::vsubst in
+            let d = match c with
+              | None -> LocalAssum (id0, subst2 subst vsubst t)
+              | Some c -> LocalDef (id0, subst2 subst vsubst c, subst2 subst vsubst t)
+            in
+            let env = replace_var_named_context id0  id env in
+            (mkVar id0 :: subst, vsubst, id::avoid, push_named d env)
+        | _ ->
+            (* spiwack: if [id0] is a section variable renaming it is
+               incorrect. We revert to a less robust behaviour where
+               the new binder has name [id]. Which amounts to the same
+               behaviour than when [id=id0]. *)
+            let d = match c with
+              | None -> LocalAssum (id, subst2 subst vsubst t)
+              | Some c -> LocalDef (id, subst2 subst vsubst c, subst2 subst vsubst t)
+            in
+	    (mkVar id :: subst, vsubst, id::avoid, push_named d env)
+      )
+      (rel_context env) ~init:([], [], ids, env) in
+  (named_context_val env, subst2 subst vsubst typ, inst_rels@inst_vars, subst, vsubst)
+
+(*------------------------------------*
+ * Entry points to define new evars   *
+ *------------------------------------*)
+
+let default_source = (Loc.ghost,Evar_kinds.InternalHole)
+
+let restrict_evar evd evk filter candidates =
+  let evd = Sigma.to_evar_map evd in
+  let evd, evk' = Evd.restrict evk filter ?candidates evd in
+  Sigma.Unsafe.of_pair (evk', Evd.declare_future_goal evk' evd)
+
+let new_pure_evar_full evd evi =
+  let evd = Sigma.to_evar_map evd in
+  let (evd, evk) = Evd.new_evar evd evi in
+  let evd = Evd.declare_future_goal evk evd in
+  Sigma.Unsafe.of_pair (evk, evd)
+
+let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) typ =
+  let evd = Sigma.to_evar_map evd in
+  let default_naming = Misctypes.IntroAnonymous in
+  let naming = Option.default default_naming naming in
+  let evi = {
+    evar_hyps = sign;
+    evar_concl = typ;
+    evar_body = Evar_empty;
+    evar_filter = filter;
+    evar_source = src;
+    evar_candidates = candidates;
+    evar_extra = store; }
+  in
+  let (evd, newevk) = Evd.new_evar evd ~naming evi in
+  let evd =
+    if principal then Evd.declare_principal_goal newevk evd
+    else Evd.declare_future_goal newevk evd
+  in
+  Sigma.Unsafe.of_pair (newevk, evd)
+
+let new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?principal instance =
+  assert (not !Flags.debug ||
+            List.distinct (ids_of_named_context (named_context_of_val sign)));
+  let Sigma (newevk, evd, p) = new_pure_evar sign evd ?src ?filter ?candidates ?store ?naming ?principal typ in
+  Sigma (mkEvar (newevk,Array.of_list instance), evd, p)
+
+(* [new_evar] declares a new existential in an env env with type typ *)
+(* Converting the env into the sign of the evar to define *)
+let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ =
+  let sign,typ',instance,subst,vsubst = push_rel_context_to_named_context env typ in
+  let candidates = Option.map (List.map (subst2 subst vsubst)) candidates in
+  let instance =
+    match filter with
+    | None -> instance
+    | Some filter -> Filter.filter_list filter instance in
+  new_evar_instance sign evd typ' ?src ?filter ?candidates ?store ?naming ?principal instance
+
+let new_evar_unsafe env evd ?src ?filter ?candidates ?store ?naming ?principal typ =
+  let evd = Sigma.Unsafe.of_evar_map evd in
+  let Sigma (evk, evd, _) = new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ in
+  (Sigma.to_evar_map evd, evk)
+
+let new_type_evar env evd ?src ?filter ?naming ?principal rigid =
+  let Sigma (s, evd', p) = Sigma.new_sort_variable rigid evd in
+  let Sigma (e, evd', q) = new_evar env evd' ?src ?filter ?naming ?principal (mkSort s) in
+  Sigma ((e, s), evd', p +> q)
+
+let e_new_type_evar env evdref ?src ?filter ?naming ?principal rigid =
+  let sigma = Sigma.Unsafe.of_evar_map !evdref in
+  let Sigma (c, sigma, _) = new_type_evar env sigma ?src ?filter ?naming ?principal rigid in
+  let sigma = Sigma.to_evar_map sigma in
+    evdref := sigma;
+    c
+
+let new_Type ?(rigid=Evd.univ_flexible) env evd = 
+  let Sigma (s, sigma, p) = Sigma.new_sort_variable rigid evd in
+  Sigma (mkSort s, sigma, p)
+
+let e_new_Type ?(rigid=Evd.univ_flexible) env evdref =
+  let evd', s = new_sort_variable rigid !evdref in
+    evdref := evd'; mkSort s
+
+  (* The same using side-effect *)
+let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ?naming ?principal ty =
+  let (evd',ev) = new_evar_unsafe env !evdref ~src:src ?filter ?candidates ?store ?naming ?principal ty in
+  evdref := evd';
+  ev
+
+(* This assumes an evar with identity instance and generalizes it over only
+   the De Bruijn part of the context *)
+let generalize_evar_over_rels sigma (ev,args) =
+  let evi = Evd.find sigma ev in
+  let sign = named_context_of_val evi.evar_hyps in
+  List.fold_left2
+    (fun (c,inst as x) a d ->
+      if isRel a then (mkNamedProd_or_LetIn d c,a::inst) else x)
+     (evi.evar_concl,[]) (Array.to_list args) sign
+
+(************************************)
+(* Removing a dependency in an evar *)
+(************************************)
+
+type clear_dependency_error =
+| OccurHypInSimpleClause of Id.t option
+| EvarTypingBreak of existential
+
+exception ClearDependencyError of Id.t * clear_dependency_error
+
+let cleared = Store.field ()
+
+exception Depends of Id.t
+
+let rec check_and_clear_in_constr env evdref err ids c =
+  (* returns a new constr where all the evars have been 'cleaned'
+     (ie the hypotheses ids have been removed from the contexts of
+     evars) *)
+  let check id' =
+    if Id.Set.mem id' ids then
+      raise (ClearDependencyError (id',err))
+  in
+    match kind_of_term c with
+      | Var id' ->
+	  check id'; c
+
+      | ( Const _ | Ind _ | Construct _ ) ->
+          let vars = Environ.vars_of_global env c in
+            Id.Set.iter check vars; c
+
+      | Evar (evk,l as ev) ->
+	  if Evd.is_defined !evdref evk then
+	    (* If evk is already defined we replace it by its definition *)
+	    let nc = whd_evar !evdref c in
+	      (check_and_clear_in_constr env evdref err ids nc)
+	  else
+	    (* We check for dependencies to elements of ids in the
+	       evar_info corresponding to e and in the instance of
+	       arguments. Concurrently, we build a new evar
+	       corresponding to e where hypotheses of ids have been
+	       removed *)
+	    let evi = Evd.find_undefined !evdref evk in
+	    let ctxt = Evd.evar_filtered_context evi in
+	    let (rids,filter) =
+              List.fold_right2
+                (fun h a (ri,filter) ->
+                  try
+                  (* Check if some id to clear occurs in the instance
+                     a of rid in ev and remember the dependency *)
+                    let check id = if Id.Set.mem id ids then raise (Depends id) in
+                    let () = Id.Set.iter check (collect_vars a) in
+                  (* Check if some rid to clear in the context of ev
+                     has dependencies in another hyp of the context of ev
+                     and transitively remember the dependency *)
+                    let check id _ =
+                      if occur_var_in_decl (Global.env ()) id h
+                      then raise (Depends id)
+                    in
+                    let () = Id.Map.iter check ri in
+                  (* No dependency at all, we can keep this ev's context hyp *)
+                    (ri, true::filter)
+                  with Depends id -> let open Context.Named.Declaration in
+                                     (Id.Map.add (get_id h) id ri, false::filter))
+		ctxt (Array.to_list l) (Id.Map.empty,[]) in
+	    (* Check if some rid to clear in the context of ev has dependencies
+	       in the type of ev and adjust the source of the dependency *)
+	    let _nconcl =
+	      try
+                let nids = Id.Map.domain rids in
+                check_and_clear_in_constr env evdref (EvarTypingBreak ev) nids (evar_concl evi)
+	      with ClearDependencyError (rid,err) ->
+		raise (ClearDependencyError (Id.Map.find rid rids,err)) in
+
+            if Id.Map.is_empty rids then c
+            else
+              let origfilter = Evd.evar_filter evi in
+              let filter = Evd.Filter.apply_subfilter origfilter filter in
+              let evd = Sigma.Unsafe.of_evar_map !evdref in
+              let Sigma (_, evd, _) = restrict_evar evd evk filter None in
+              let evd = Sigma.to_evar_map evd in
+              evdref := evd;
+	    (* spiwack: hacking session to mark the old [evk] as having been "cleared" *)
+	      let evi = Evd.find !evdref evk in
+	      let extra = evi.evar_extra in
+	      let extra' = Store.set extra cleared true in
+	      let evi' = { evi with evar_extra = extra' } in
+	      evdref := Evd.add !evdref evk evi' ;
+	    (* spiwack: /hacking session *)
+              whd_evar !evdref c
+
+      | _ -> map_constr (check_and_clear_in_constr env evdref err ids) c
+
+let clear_hyps_in_evi_main env evdref hyps terms ids =
+  (* clear_hyps_in_evi erases hypotheses ids in hyps, checking if some
+     hypothesis does not depend on a element of ids, and erases ids in
+     the contexts of the evars occurring in evi *)
+  let terms =
+    List.map (check_and_clear_in_constr env evdref (OccurHypInSimpleClause None) ids) terms in
+  let nhyps =
+    let open Context.Named.Declaration in
+    let check_context decl =
+      let err = OccurHypInSimpleClause (Some (get_id decl)) in
+      map_constr (check_and_clear_in_constr env evdref err ids) decl
+    in
+    let check_value vk = match force_lazy_val vk with
+    | None -> vk
+    | Some (_, d) ->
+      if (Id.Set.for_all (fun e -> not (Id.Set.mem e d)) ids) then
+        (* v does depend on any of ids, it's ok *)
+        vk
+      else
+        (* v depends on one of the cleared hyps:
+            we forget the computed value *)
+        dummy_lazy_val ()
+    in
+      remove_hyps ids check_context check_value hyps
+  in
+  (nhyps,terms)
+
+let clear_hyps_in_evi env evdref hyps concl ids =
+  match clear_hyps_in_evi_main env evdref hyps [concl] ids with
+  | (nhyps,[nconcl]) -> (nhyps,nconcl)
+  | _ -> assert false
+
+let clear_hyps2_in_evi env evdref hyps t concl ids =
+  match clear_hyps_in_evi_main env evdref hyps [t;concl] ids with
+  | (nhyps,[t;nconcl]) -> (nhyps,t,nconcl)
+  | _ -> assert false
+
+(* spiwack: a few functions to gather evars on which goals depend. *)
+let queue_set q is_dependent set =
+  Evar.Set.iter (fun a -> Queue.push (is_dependent,a) q) set
+let queue_term q is_dependent c =
+  queue_set q is_dependent (evars_of_term c)
+
+let process_dependent_evar q acc evm is_dependent e =
+  let evi = Evd.find evm e in
+  (* Queues evars appearing in the types of the goal (conclusion, then
+     hypotheses), they are all dependent. *)
+  queue_term q true evi.evar_concl;
+  List.iter begin fun decl ->
+    let open Context.Named.Declaration in
+    queue_term q true (get_type decl);
+    match decl with
+    | LocalAssum _ -> ()
+    | LocalDef (_,b,_) -> queue_term q true b
+  end (Environ.named_context_of_val evi.evar_hyps);
+  match evi.evar_body with
+  | Evar_empty ->
+      if is_dependent then Evar.Map.add e None acc else acc
+  | Evar_defined b ->
+      let subevars = evars_of_term b in
+      (* evars appearing in the definition of an evar [e] are marked
+         as dependent when [e] is dependent itself: if [e] is a
+         non-dependent goal, then, unless they are reach from another
+         path, these evars are just other non-dependent goals. *)
+      queue_set q is_dependent subevars;
+      if is_dependent then Evar.Map.add e (Some subevars) acc else acc
+
+let gather_dependent_evars q evm =
+  let acc = ref Evar.Map.empty in
+  while not (Queue.is_empty q) do
+    let (is_dependent,e) = Queue.pop q in
+    (* checks if [e] has already been added to [!acc] *)
+    begin if not (Evar.Map.mem e !acc) then
+        acc := process_dependent_evar q !acc evm is_dependent e  
+    end
+  done;
+  !acc
+
+let gather_dependent_evars evm l =
+  let q = Queue.create () in
+  List.iter (fun a -> Queue.add (false,a) q) l;
+  gather_dependent_evars q evm
+
+(* /spiwack *)
+
+(** The following functions return the set of undefined evars
+    contained in the object, the defined evars being traversed.
+    This is roughly a combination of the previous functions and
+    [nf_evar]. *)
+
+let undefined_evars_of_term evd t =
+  let rec evrec acc c =
+    match kind_of_term c with
+      | Evar (n, l) ->
+	let acc = Array.fold_left evrec acc l in
+	(try match (Evd.find evd n).evar_body with
+	  | Evar_empty -> Evar.Set.add n acc
+	  | Evar_defined c -> evrec acc c
+	 with Not_found -> anomaly ~label:"undefined_evars_of_term" (Pp.str "evar not found"))
+      | _ -> fold_constr evrec acc c
+  in
+  evrec Evar.Set.empty t
+
+let undefined_evars_of_named_context evd nc =
+  let open Context.Named.Declaration in
+  Context.Named.fold_outside
+    (fold (fun c s -> Evar.Set.union s (undefined_evars_of_term evd c)))
+    nc
+    ~init:Evar.Set.empty
+
+let undefined_evars_of_evar_info evd evi =
+  Evar.Set.union (undefined_evars_of_term evd evi.evar_concl)
+    (Evar.Set.union
+       (match evi.evar_body with
+	 | Evar_empty -> Evar.Set.empty
+	 | Evar_defined b -> undefined_evars_of_term evd b)
+       (undefined_evars_of_named_context evd
+	  (named_context_of_val evi.evar_hyps)))
+
+(* spiwack: this is a more complete version of
+   {!Termops.occur_evar}. The latter does not look recursively into an
+   [evar_map]. If unification only need to check superficially, tactics
+   do not have this luxury, and need the more complete version. *)
+let occur_evar_upto sigma n c =
+  let rec occur_rec c = match kind_of_term c with
+    | Evar (sp,_) when Evar.equal sp n -> raise Occur
+    | Evar e -> Option.iter occur_rec (existential_opt_value sigma e)
+    | _ -> iter_constr occur_rec c
+  in
+  try occur_rec c; false with Occur -> true
+
+(* We don't try to guess in which sort the type should be defined, since
+   any type has type Type. May cause some trouble, but not so far... *)
+
+let judge_of_new_Type evd =
+  let Sigma (s, evd', p) = Sigma.new_univ_variable univ_rigid evd in
+  Sigma ({ uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) }, evd', p)
+
+let subterm_source evk (loc,k) =
+  let evk = match k with
+    | Evar_kinds.SubEvar (evk) -> evk
+    | _ -> evk in
+  (loc,Evar_kinds.SubEvar evk)
+
+
+(** Term exploration up to instantiation. *)
+let kind_of_term_upto sigma t =
+  Constr.kind (whd_evar sigma t)
+
+(** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and
+    [u] up to existential variable instantiation and equalisable
+    universes. The term [t] is interpreted in [sigma1] while [u] is
+    interpreted in [sigma2]. The universe constraints in [sigma2] are
+    assumed to be an extention of those in [sigma1]. *)
+let eq_constr_univs_test sigma1 sigma2 t u =
+  (* spiwack: mild code duplication with {!Evd.eq_constr_univs}. *)
+  let open Evd in
+  let fold cstr sigma =
+    try Some (add_universe_constraints sigma cstr)
+    with Univ.UniverseInconsistency _ | UniversesDiffer -> None
+  in
+  let ans =
+    Universes.eq_constr_univs_infer_with
+      (fun t -> kind_of_term_upto sigma1 t)
+      (fun u -> kind_of_term_upto sigma2 u)
+      (universes sigma2) fold t u sigma2
+  in
+  match ans with None -> false | Some _ -> true
+
+type type_constraint = types option
+type val_constraint = constr option
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
new file mode 100644
index 0000000000..ffff2c5dd9
--- /dev/null
+++ b/engine/evarutil.mli
@@ -0,0 +1,221 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Names
+open Term
+open Evd
+open Environ
+
+(** {5 This modules provides useful functions for unification modulo evars } *)
+
+(** {6 Metas} *)
+
+(** [new_meta] is a generator of unique meta variables *)
+val new_meta : unit -> metavariable
+val mk_new_meta : unit -> constr
+
+(** {6 Creating a fresh evar given their type and context} *)
+val new_evar :
+  env -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
+  ?candidates:constr list -> ?store:Store.t ->
+  ?naming:Misctypes.intro_pattern_naming_expr ->
+  ?principal:bool -> types -> (constr, 'r) Sigma.sigma
+
+val new_pure_evar :
+  named_context_val -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
+  ?candidates:constr list -> ?store:Store.t ->
+  ?naming:Misctypes.intro_pattern_naming_expr ->
+  ?principal:bool -> types -> (evar, 'r) Sigma.sigma
+
+val new_pure_evar_full : 'r Sigma.t -> evar_info -> (evar, 'r) Sigma.sigma
+
+(** the same with side-effects *)
+val e_new_evar :
+  env -> evar_map ref -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
+  ?candidates:constr list -> ?store:Store.t ->
+  ?naming:Misctypes.intro_pattern_naming_expr ->
+  ?principal:bool -> types -> constr
+
+(** Create a new Type existential variable, as we keep track of 
+    them during type-checking and unification. *)
+val new_type_evar :
+  env -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
+  ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid ->
+  (constr * sorts, 'r) Sigma.sigma
+
+val e_new_type_evar : env -> evar_map ref ->
+  ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
+  ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> constr * sorts
+
+val new_Type : ?rigid:rigid -> env -> 'r Sigma.t -> (constr, 'r) Sigma.sigma
+val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr
+
+val restrict_evar : 'r Sigma.t -> existential_key -> Filter.t ->
+  constr list option -> (existential_key, 'r) Sigma.sigma
+
+(** Polymorphic constants *)
+
+val new_global : 'r Sigma.t -> Globnames.global_reference -> (constr, 'r) Sigma.sigma
+val e_new_global : evar_map ref -> Globnames.global_reference -> constr
+
+(** Create a fresh evar in a context different from its definition context:
+   [new_evar_instance sign evd ty inst] creates a new evar of context
+   [sign] and type [ty], [inst] is a mapping of the evar context to
+   the context where the evar should occur. This means that the terms
+   of [inst] are typed in the occurrence context and their type (seen
+   as a telescope) is [sign] *)
+val new_evar_instance :
+ named_context_val -> 'r Sigma.t -> types -> 
+  ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:constr list ->
+  ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr ->
+  ?principal:bool ->
+  constr list -> (constr, 'r) Sigma.sigma
+
+val make_pure_subst : evar_info -> constr array -> (Id.t * constr) list
+
+val safe_evar_value : evar_map -> existential -> constr option
+
+(** {6 Evars/Metas switching...} *)
+
+val non_instantiated : evar_map -> evar_info Evar.Map.t
+
+(** {6 Unification utils} *)
+
+(** [head_evar c] returns the head evar of [c] if any *)
+exception NoHeadEvar
+val head_evar : constr -> existential_key (** may raise NoHeadEvar *)
+
+(* Expand head evar if any *)
+val whd_head_evar :  evar_map -> constr -> constr
+
+(* An over-approximation of [has_undefined (nf_evars evd c)] *)
+val has_undefined_evars : evar_map -> constr -> bool
+
+val is_ground_term :  evar_map -> constr -> bool
+val is_ground_env  :  evar_map -> env -> bool
+
+(** [gather_dependent_evars evm seeds] classifies the evars in [evm]
+    as dependent_evars and goals (these may overlap). A goal is an
+    evar in [seeds] or an evar appearing in the (partial) definition
+    of a goal. A dependent evar is an evar appearing in the type
+    (hypotheses and conclusion) of a goal, or in the type or (partial)
+    definition of a dependent evar.  The value return is a map
+    associating to each dependent evar [None] if it has no (partial)
+    definition or [Some s] if [s] is the list of evars appearing in
+    its (partial) definition. *)
+val gather_dependent_evars : evar_map -> evar list -> (Evar.Set.t option) Evar.Map.t
+
+(** The following functions return the set of undefined evars
+    contained in the object, the defined evars being traversed.
+    This is roughly a combination of the previous functions and
+    [nf_evar]. *)
+
+val undefined_evars_of_term : evar_map -> constr -> Evar.Set.t
+val undefined_evars_of_named_context : evar_map -> Context.Named.t -> Evar.Set.t
+val undefined_evars_of_evar_info : evar_map -> evar_info -> Evar.Set.t
+
+(** [occur_evar_upto sigma k c] returns [true] if [k] appears in
+    [c]. It looks up recursively in [sigma] for the value of existential
+    variables. *)
+val occur_evar_upto : evar_map -> Evar.t -> Constr.t -> bool
+
+(** {6 Value/Type constraints} *)
+
+val judge_of_new_Type : 'r Sigma.t -> (unsafe_judgment, 'r) Sigma.sigma
+
+(***********************************************************)
+
+(** [flush_and_check_evars] raise [Uninstantiated_evar] if an evar remains
+    uninstantiated; [nf_evar] leaves uninstantiated evars as is *)
+
+val whd_evar :  evar_map -> constr -> constr
+val nf_evar :  evar_map -> constr -> constr
+val j_nf_evar :  evar_map -> unsafe_judgment -> unsafe_judgment
+val jl_nf_evar :
+   evar_map -> unsafe_judgment list -> unsafe_judgment list
+val jv_nf_evar :
+   evar_map -> unsafe_judgment array -> unsafe_judgment array
+val tj_nf_evar :
+   evar_map -> unsafe_type_judgment -> unsafe_type_judgment
+
+val nf_named_context_evar : evar_map -> Context.Named.t -> Context.Named.t
+val nf_rel_context_evar : evar_map -> Context.Rel.t -> Context.Rel.t
+val nf_env_evar : evar_map -> env -> env
+
+val nf_evar_info : evar_map -> evar_info -> evar_info
+val nf_evar_map : evar_map -> evar_map
+val nf_evar_map_undefined : evar_map -> evar_map
+
+(** Presenting terms without solved evars *)
+
+val nf_evars_universes : evar_map -> constr -> constr
+
+val nf_evars_and_universes : evar_map -> evar_map * (constr -> constr)
+val e_nf_evars_and_universes : evar_map ref -> (constr -> constr) * Universes.universe_opt_subst
+
+(** Normalize the evar map w.r.t. universes, after simplification of constraints.
+    Return the substitution function for constrs as well. *)
+val nf_evar_map_universes : evar_map -> evar_map * (constr -> constr)
+
+(** Replacing all evars, possibly raising [Uninstantiated_evar] *)
+exception Uninstantiated_evar of existential_key
+val flush_and_check_evars :  evar_map -> constr -> constr
+
+(** {6 Term manipulation up to instantiation} *)
+
+(** Like {!Constr.kind} except that [kind_of_term sigma t] exposes [t]
+    as an evar [e] only if [e] is uninstantiated in [sigma]. Otherwise the
+    value of [e] in [sigma] is (recursively) used. *)
+val kind_of_term_upto : evar_map -> constr -> (constr,types) kind_of_term
+
+(** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and
+    [u] up to existential variable instantiation and equalisable
+    universes. The term [t] is interpreted in [sigma1] while [u] is
+    interpreted in [sigma2]. The universe constraints in [sigma2] are
+    assumed to be an extention of those in [sigma1]. *)
+val eq_constr_univs_test : evar_map -> evar_map -> constr -> constr -> bool
+
+(** {6 Removing hyps in evars'context}
+raise OccurHypInSimpleClause if the removal breaks dependencies *)
+
+type clear_dependency_error =
+| OccurHypInSimpleClause of Id.t option
+| EvarTypingBreak of existential
+
+exception ClearDependencyError of Id.t * clear_dependency_error
+
+(* spiwack: marks an evar that has been "defined" by clear.
+    used by [Goal] and (indirectly) [Proofview] to handle the clear tactic gracefully*)
+val cleared : bool Store.field
+
+val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> types ->
+  Id.Set.t -> named_context_val * types
+
+val clear_hyps2_in_evi : env -> evar_map ref -> named_context_val -> types -> types ->
+  Id.Set.t -> named_context_val * types * types
+
+val push_rel_context_to_named_context : Environ.env -> types ->
+  named_context_val * types * constr list * constr list * (identifier*constr) list
+
+val generalize_evar_over_rels : evar_map -> existential -> types * constr list
+
+(** Evar combinators *)
+
+val evd_comb0 : (evar_map -> evar_map * 'a) -> evar_map ref -> 'a
+val evd_comb1 : (evar_map -> 'b -> evar_map * 'a) -> evar_map ref -> 'b -> 'a
+val evd_comb2 : (evar_map -> 'b -> 'c -> evar_map * 'a) -> evar_map ref -> 'b -> 'c -> 'a
+
+val subterm_source : existential_key -> Evar_kinds.t Loc.located ->
+  Evar_kinds.t Loc.located
+
+val meta_counter_summary_name : string
+
+(** Deprecater *)
+
+type type_constraint = types option
+type val_constraint = constr option
diff --git a/engine/evd.ml b/engine/evd.ml
index 168a10df93..b6849f7ffb 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
@@ -16,6 +16,7 @@ open Vars
 open Termops
 open Environ
 open Globnames
+open Context.Named.Declaration
 
 (** Generic filters *)
 module Filter :
@@ -208,15 +209,6 @@ let map_evar_info f evi =
     evar_concl = f evi.evar_concl;
     evar_candidates = Option.map (List.map f) evi.evar_candidates }
 
-let evar_ident_info evi =
-  match evi.evar_source with
-  | _,Evar_kinds.ImplicitArg (c,(n,Some id),b) -> id
-  | _,Evar_kinds.VarInstance id -> id
-  | _,Evar_kinds.GoalEvar -> Id.of_string "Goal"
-  | _ ->
-      let env = reset_with_named_context evi.evar_hyps (Global.env()) in
-      Namegen.id_of_name_using_hdchar env evi.evar_concl Anonymous
-
 (* This exception is raised by *.existential_value *)
 exception NotInstantiatedEvar
 
@@ -230,20 +222,20 @@ let evar_instance_array test_id info args =
     else instance_mismatch ()
   | false :: filter, _ :: ctxt ->
     instrec filter ctxt i
-  | true :: filter, (id,_,_ as d) :: ctxt ->
+  | true :: filter, d :: ctxt ->
     if i < len then
       let c = Array.unsafe_get args i in
       if test_id d c then instrec filter ctxt (succ i)
-      else (id, c) :: instrec filter ctxt (succ i)
+      else (get_id d, c) :: instrec filter ctxt (succ i)
     else instance_mismatch ()
   | _ -> instance_mismatch ()
   in
   match Filter.repr (evar_filter info) with
   | None ->
-    let map i (id,_,_ as d) =
+     let map i d =
       if (i < len) then
         let c = Array.unsafe_get args i in
-        if test_id d c then None else Some (id,c)
+        if test_id d c then None else Some (get_id d, c)
       else instance_mismatch ()
     in
     List.map_filter_i map (evar_context info)
@@ -251,7 +243,7 @@ let evar_instance_array test_id info args =
     instrec filter (evar_context info) 0
 
 let make_evar_instance_array info args =
-  evar_instance_array (fun (id,_,_) -> isVarId id) info args
+  evar_instance_array (isVarId % get_id) info args
 
 let instantiate_evar_array info c args =
   let inst = make_evar_instance_array info args in
@@ -259,219 +251,22 @@ let instantiate_evar_array info c args =
   | [] -> c
   | _ -> replace_vars inst c
 
-module StringOrd = struct type t = string let compare = String.compare end
-module UNameMap = struct
-    
-  include Map.Make(StringOrd)
-    
-  let union s t = 
-    if s == t then s
-    else
-      merge (fun k l r -> 
-	match l, r with
-	| Some _, _ -> l
-	| _, _ -> r) s t
-end
-
-(* 2nd part used to check consistency on the fly. *)
-type evar_universe_context = 
- { uctx_names : Univ.Level.t UNameMap.t * string Univ.LMap.t;
-   uctx_local : Univ.universe_context_set; (** The local context of variables *)
-    uctx_univ_variables : Universes.universe_opt_subst;
-      (** The local universes that are unification variables *)
-    uctx_univ_algebraic : Univ.universe_set; 
-    (** The subset of unification variables that
-	can be instantiated with algebraic universes as they appear in types 
-	and universe instances only. *)
-    uctx_universes : Univ.universes; (** The current graph extended with the local constraints *)
-    uctx_initial_universes : Univ.universes; (** The graph at the creation of the evar_map *)
-  }
-  
-let empty_evar_universe_context = 
-  { uctx_names = UNameMap.empty, Univ.LMap.empty;
-    uctx_local = Univ.ContextSet.empty;
-    uctx_univ_variables = Univ.LMap.empty;
-    uctx_univ_algebraic = Univ.LSet.empty;
-    uctx_universes = Univ.initial_universes;
-    uctx_initial_universes = Univ.initial_universes }
-
-let evar_universe_context_from e = 
-  let u = universes e in
-    {empty_evar_universe_context with 
-      uctx_universes = u; uctx_initial_universes = u}
-
-let is_empty_evar_universe_context ctx =
-  Univ.ContextSet.is_empty ctx.uctx_local && 
-    Univ.LMap.is_empty ctx.uctx_univ_variables
-
-let union_evar_universe_context ctx ctx' =
-  if ctx == ctx' then ctx
-  else if is_empty_evar_universe_context ctx' then ctx
-  else
-    let local = Univ.ContextSet.union ctx.uctx_local ctx'.uctx_local in
-    let names = UNameMap.union (fst ctx.uctx_names) (fst ctx'.uctx_names) in
-    let names_rev = Univ.LMap.union (snd ctx.uctx_names) (snd ctx'.uctx_names) in
-      { uctx_names = (names, names_rev);
-	uctx_local = local;
-	uctx_univ_variables = 
-	  Univ.LMap.subst_union ctx.uctx_univ_variables ctx'.uctx_univ_variables;
-	uctx_univ_algebraic = 
-	  Univ.LSet.union ctx.uctx_univ_algebraic ctx'.uctx_univ_algebraic;
-	uctx_initial_universes = ctx.uctx_initial_universes;
-	uctx_universes = 
-	  if local == ctx.uctx_local then ctx.uctx_universes
-	  else
-	    let cstrsr = Univ.ContextSet.constraints ctx'.uctx_local in
-	      Univ.merge_constraints cstrsr ctx.uctx_universes }
-
-(* let union_evar_universe_context_key = Profile.declare_profile "union_evar_universe_context";; *)
-(* let union_evar_universe_context =  *)
-(*   Profile.profile2 union_evar_universe_context_key union_evar_universe_context;; *)
-
+type evar_universe_context = UState.t
 type 'a in_evar_universe_context = 'a * evar_universe_context
 
-let evar_universe_context_set diff ctx =
-  let initctx = ctx.uctx_local in
-  let cstrs =
-    Univ.LSet.fold
-      (fun l cstrs ->
-       try
-	 match Univ.LMap.find l ctx.uctx_univ_variables with
-	 | Some u -> Univ.Constraint.add (l, Univ.Eq, Option.get (Univ.Universe.level u)) cstrs
-	 | None -> cstrs
-       with Not_found | Option.IsNone -> cstrs)
-      (Univ.Instance.levels (Univ.UContext.instance diff)) Univ.Constraint.empty
-  in
-    Univ.ContextSet.add_constraints cstrs initctx 
-		      
-let evar_universe_context_constraints ctx = snd ctx.uctx_local
-let evar_context_universe_context ctx = Univ.ContextSet.to_context ctx.uctx_local
-    
-let evar_universe_context_of ctx = { empty_evar_universe_context with uctx_local = ctx }
-let evar_universe_context_subst ctx = ctx.uctx_univ_variables
-
-let instantiate_variable l b v =
-  v := Univ.LMap.add l (Some b) !v
-
-exception UniversesDiffer
-
-let process_universe_constraints univs vars alg cstrs =
-  let vars = ref vars in
-  let normalize = Universes.normalize_universe_opt_subst vars in
-  let rec unify_universes fo l d r local =
-    let l = normalize l and r = normalize r in
-      if Univ.Universe.equal l r then local
-      else 
-	let varinfo x = 
-	  match Univ.Universe.level x with
-	  | None -> Inl x
-	  | Some l -> Inr (l, Univ.LMap.mem l !vars, Univ.LSet.mem l alg)
-	in
-	  if d == Universes.ULe then
-	    if Univ.check_leq univs l r then
-	      (** Keep Prop/Set <= var around if var might be instantiated by prop or set
-		  later. *)
-	      if Univ.Universe.is_level l then 
-		match Univ.Universe.level r with
-		| Some r ->
-		  Univ.Constraint.add (Option.get (Univ.Universe.level l),Univ.Le,r) local
-		| _ -> local
-	      else local
-	    else
-	      match Univ.Universe.level r with
-	      | None -> error ("Algebraic universe on the right")
-	      | Some rl ->
-		if Univ.Level.is_small rl then
-		  let levels = Univ.Universe.levels l in
-		    Univ.LSet.fold (fun l local ->
-		      if Univ.Level.is_small l || Univ.LMap.mem l !vars then
-			Univ.enforce_eq (Univ.Universe.make l) r local
-		      else raise (Univ.UniverseInconsistency (Univ.Le, Univ.Universe.make l, r, None)))
-		      levels local
-		else
-		  Univ.enforce_leq l r local
-	  else if d == Universes.ULub then
-	    match varinfo l, varinfo r with
-	    | (Inr (l, true, _), Inr (r, _, _)) 
-	    | (Inr (r, _, _), Inr (l, true, _)) -> 
-	      instantiate_variable l (Univ.Universe.make r) vars; 
-	      Univ.enforce_eq_level l r local
-	    | Inr (_, _, _), Inr (_, _, _) ->
-	      unify_universes true l Universes.UEq r local
-	    | _, _ -> assert false
-	  else (* d = Universes.UEq *)
-	    match varinfo l, varinfo r with
-	    | Inr (l', lloc, _), Inr (r', rloc, _) ->
-	      let () = 
-		if lloc then
-		  instantiate_variable l' r vars
-		else if rloc then 
-		  instantiate_variable r' l vars
-		else if not (Univ.check_eq univs l r) then
-		  (* Two rigid/global levels, none of them being local,
-		     one of them being Prop/Set, disallow *)
-		  if Univ.Level.is_small l' || Univ.Level.is_small r' then
-		    raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None))
-		  else
-		    if fo then 
-		      raise UniversesDiffer
-	      in
-	        Univ.enforce_eq_level l' r' local
-	    | Inr (l, loc, alg), Inl r
-	    | Inl r, Inr (l, loc, alg) ->
-	       let inst = Univ.univ_level_rem l r r in
-		 if alg then (instantiate_variable l inst vars; local)
-		 else
-		   let lu = Univ.Universe.make l in
-		   if Univ.univ_level_mem l r then
-		     Univ.enforce_leq inst lu local
-		   else raise (Univ.UniverseInconsistency (Univ.Eq, lu, r, None))
-            | _, _ (* One of the two is algebraic or global *) -> 
-	     if Univ.check_eq univs l r then local
-	     else raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None))
-  in
-  let local = 
-    Universes.Constraints.fold (fun (l,d,r) local -> unify_universes false l d r local)
-      cstrs Univ.Constraint.empty
-  in
-    !vars, local
-
-let add_constraints_context ctx cstrs =
-  let univs, local = ctx.uctx_local in
-  let cstrs' = Univ.Constraint.fold (fun (l,d,r) acc -> 
-    let l = Univ.Universe.make l and r = Univ.Universe.make r in
-    let cstr' = 
-      if d == Univ.Lt then (Univ.Universe.super l, Universes.ULe, r)
-      else (l, (if d == Univ.Le then Universes.ULe else Universes.UEq), r)
-    in Universes.Constraints.add cstr' acc)
-    cstrs Universes.Constraints.empty
-  in
-  let vars, local' =
-    process_universe_constraints ctx.uctx_universes
-      ctx.uctx_univ_variables ctx.uctx_univ_algebraic
-      cstrs'
-  in
-    { ctx with uctx_local = (univs, Univ.Constraint.union local local');
-      uctx_univ_variables = vars;
-      uctx_universes = Univ.merge_constraints cstrs ctx.uctx_universes }
-
-(* let addconstrkey = Profile.declare_profile "add_constraints_context";; *)
-(* let add_constraints_context = Profile.profile2 addconstrkey add_constraints_context;; *)
-
-let add_universe_constraints_context ctx cstrs =
-  let univs, local = ctx.uctx_local in
-  let vars, local' = 
-    process_universe_constraints ctx.uctx_universes 
-      ctx.uctx_univ_variables ctx.uctx_univ_algebraic 
-      cstrs 
-  in
-    { ctx with uctx_local = (univs, Univ.Constraint.union local local');
-      uctx_univ_variables = vars;
-      uctx_universes = Univ.merge_constraints local' ctx.uctx_universes }
+let empty_evar_universe_context = UState.empty
+let is_empty_evar_universe_context = UState.is_empty
+let union_evar_universe_context = UState.union
+let evar_universe_context_set = UState.context_set
+let evar_universe_context_constraints = UState.constraints
+let evar_context_universe_context = UState.context
+let evar_universe_context_of = UState.of_context_set
+let evar_universe_context_subst = UState.subst
+let add_constraints_context = UState.add_constraints
+let add_universe_constraints_context = UState.add_universe_constraints
+let constrain_variables = UState.constrain_variables 
+let evar_universe_context_of_binders = UState.of_binders
 
-(* let addunivconstrkey = Profile.declare_profile "add_universe_constraints_context";; *)
-(* let add_universe_constraints_context =  *)
-(*   Profile.profile2 addunivconstrkey add_universe_constraints_context;; *)
 (*******************************************************************)
 (* Metamaps *)
 
@@ -560,11 +355,86 @@ type evar_constraint = conv_pb * Environ.env * constr * constr
 
 module EvMap = Evar.Map
 
+module EvNames :
+sig
+
+open Misctypes
+
+type t
+
+val empty : t
+val add_name_newly_undefined : intro_pattern_naming_expr -> Evar.t -> evar_info -> t -> t
+val add_name_undefined : intro_pattern_naming_expr -> Evar.t -> evar_info -> t -> t
+val remove_name_defined : Evar.t -> t -> t
+val rename : Evar.t -> Id.t -> t -> t
+val reassign_name_defined : Evar.t -> Evar.t -> t -> t
+val ident : Evar.t -> t -> Id.t option
+val key : Id.t -> t -> Evar.t
+
+end =
+struct
+
+type t = Id.t EvMap.t * existential_key Idmap.t
+
+let empty = (EvMap.empty, Idmap.empty)
+
+let add_name_newly_undefined naming evk evi (evtoid, idtoev as names) =
+  let id = match naming with
+  | Misctypes.IntroAnonymous -> None
+  | Misctypes.IntroIdentifier id ->
+    if Idmap.mem id idtoev then
+    user_err_loc
+      (Loc.ghost,"",str "Already an existential evar of name " ++ pr_id id);
+    Some id
+  | Misctypes.IntroFresh id ->
+    let id = Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev) in
+    Some id
+  in
+  match id with
+  | None -> names
+  | Some id -> (EvMap.add evk id evtoid, Idmap.add id evk idtoev)
+
+let add_name_undefined naming evk evi (evtoid,idtoev as evar_names) =
+  if EvMap.mem evk evtoid then
+    evar_names
+  else
+    add_name_newly_undefined naming evk evi evar_names
+
+let remove_name_defined evk (evtoid, idtoev as names) =
+  let id = try Some (EvMap.find evk evtoid) with Not_found -> None in
+  match id with
+  | None -> names
+  | Some id -> (EvMap.remove evk evtoid, Idmap.remove id idtoev)
+
+let rename evk id (evtoid, idtoev) =
+  let id' = try Some (EvMap.find evk evtoid) with Not_found -> None in
+  match id' with
+  | None -> (EvMap.add evk id evtoid, Idmap.add id evk idtoev)
+  | Some id' ->
+    if Idmap.mem id idtoev then anomaly (str "Evar name already in use");
+    (EvMap.update evk id evtoid (* overwrite old name *), Idmap.add id evk (Idmap.remove id' idtoev))
+
+let reassign_name_defined evk evk' (evtoid, idtoev as names) =
+  let id = try Some (EvMap.find evk evtoid) with Not_found -> None in
+  match id with
+  | None -> names (** evk' must not be defined *)
+  | Some id ->
+    (EvMap.add evk' id (EvMap.remove evk evtoid),
+    Idmap.add id evk' (Idmap.remove id idtoev))
+
+let ident evk (evtoid, _) =
+  try Some (EvMap.find evk evtoid) with Not_found -> None
+
+let key id (_, idtoev) =
+  Idmap.find id idtoev
+
+end
+
 type evar_map = {
   (** Existential variables *)
   defn_evars : evar_info EvMap.t;
   undf_evars : evar_info EvMap.t;
-  evar_names : Id.t EvMap.t * existential_key Idmap.t;
+  evar_names : EvNames.t;
   (** Universes *)
   universes  : evar_universe_context;
   (** Conversion problems *)
@@ -573,7 +443,7 @@ type evar_map = {
   (** Metas *)
   metas      : clbinding Metamap.t;
   (** Interactive proofs *)
-  effects    : Declareops.side_effects;
+  effects    : Safe_typing.private_constants;
   future_goals : Evar.t list; (** list of newly created evars, to be
                                   eventually turned into goals if not solved.*)
   principal_future_goal : Evar.t option; (** if [Some e], [e] must be
@@ -589,61 +459,42 @@ type evar_map = {
 
 (*** Lifting primitive from Evar.Map. ***)
 
-let add_name_newly_undefined naming evk evi (evtoid,idtoev) =
-  let id = match naming with
-  | Misctypes.IntroAnonymous ->
-      let id = evar_ident_info evi in
-      Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev)
-  | Misctypes.IntroIdentifier id ->
-      let id' =
-        Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev) in
-      if not (Names.Id.equal id id') then
-        user_err_loc
-          (Loc.ghost,"",str "Already an existential evar of name " ++ pr_id id);
-      id'
-  | Misctypes.IntroFresh id ->
-      Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev) in
-  (EvMap.add evk id evtoid, Idmap.add id evk idtoev)
-
-let add_name_undefined naming evk evi (evtoid,idtoev as evar_names) =
-  if EvMap.mem evk evtoid then
-    evar_names
-  else
-    add_name_newly_undefined naming evk evi evar_names
-
-let remove_name_defined evk (evtoid,idtoev) =
-  let id = EvMap.find evk evtoid in
-  (EvMap.remove evk evtoid, Idmap.remove id idtoev)
-
-let remove_name_possibly_already_defined evk evar_names =
-  try remove_name_defined evk evar_names
-  with Not_found -> evar_names
-
 let rename evk id evd =
-  let (evtoid,idtoev) = evd.evar_names in
-  let id' = EvMap.find evk evtoid in
-  if Idmap.mem id idtoev then anomaly (str "Evar name already in use");
-  { evd with evar_names =
-      (EvMap.add evk id evtoid (* overwrite old name *),
-       Idmap.add id evk (Idmap.remove id' idtoev)) }
-
-let reassign_name_defined evk evk' (evtoid,idtoev) =
-  let id = EvMap.find evk evtoid in
-  (EvMap.add evk' id (EvMap.remove evk evtoid),
-   Idmap.add id evk' (Idmap.remove id idtoev))
-
-let add d e i = match i.evar_body with
+  { evd with evar_names = EvNames.rename evk id evd.evar_names }
+
+let add_with_name ?(naming = Misctypes.IntroAnonymous) d e i = match i.evar_body with
 | Evar_empty ->
-  let evar_names = add_name_undefined Misctypes.IntroAnonymous e i d.evar_names in
+  let evar_names = EvNames.add_name_undefined naming e i d.evar_names in
   { d with undf_evars = EvMap.add e i d.undf_evars; evar_names }
 | Evar_defined _ ->
-  let evar_names = remove_name_possibly_already_defined e d.evar_names in
+  let evar_names = EvNames.remove_name_defined e d.evar_names in
   { d with defn_evars = EvMap.add e i d.defn_evars; evar_names }
 
+let add d e i = add_with_name d e i
+
+(** New evars *)
+
+let evar_counter_summary_name = "evar counter"
+
+(* Generator of existential names *)
+let new_untyped_evar =
+  let evar_ctr = Summary.ref 0 ~name:evar_counter_summary_name in
+  fun () -> incr evar_ctr; Evar.unsafe_of_int !evar_ctr
+
+let new_evar evd ?naming evi =
+  let evk = new_untyped_evar () in
+  let evd = add_with_name evd ?naming evk evi in
+  (evd, evk)
+
 let remove d e =
   let undf_evars = EvMap.remove e d.undf_evars in
   let defn_evars = EvMap.remove e d.defn_evars in
-  { d with undf_evars; defn_evars; }
+  let principal_future_goal = match d.principal_future_goal with
+  | None -> None
+  | Some e' -> if Evar.equal e e' then None else d.principal_future_goal
+  in
+  let future_goals = List.filter (fun e' -> not (Evar.equal e e')) d.future_goals in
+  { d with undf_evars; defn_evars; principal_future_goal; future_goals }
 
 let find d e =
   try EvMap.find e d.undf_evars
@@ -744,16 +595,12 @@ let cmap f evd =
   { evd with
       metas = Metamap.map (map_clb f) evd.metas;
       defn_evars = EvMap.map (map_evar_info f) evd.defn_evars;
-      undf_evars = EvMap.map (map_evar_info f) evd.defn_evars
+      undf_evars = EvMap.map (map_evar_info f) evd.undf_evars
   }
 
 (* spiwack: deprecated *)
 let create_evar_defs sigma = { sigma with
   conv_pbs=[]; last_mods=Evar.Set.empty; metas=Metamap.empty }
-(* spiwack: tentatively deprecated *)
-let create_goal_evar_defs sigma = { sigma with
-   (* conv_pbs=[]; last_mods=Evar.Set.empty; metas=Metamap.empty } *)
-  metas=Metamap.empty } 
 
 let empty = {
   defn_evars = EvMap.empty;
@@ -762,17 +609,17 @@ let empty = {
   conv_pbs   = [];
   last_mods  = Evar.Set.empty;
   metas      = Metamap.empty;
-  effects    = Declareops.no_seff;
-  evar_names = (EvMap.empty,Idmap.empty); (* id<->key for undefined evars *)
+  effects    = Safe_typing.empty_private_constants;
+  evar_names = EvNames.empty; (* id<->key for undefined evars *)
   future_goals = [];
   principal_future_goal = None;
   extras = Store.empty;
 }
 
-let from_env ?ctx e = 
-  match ctx with
-  | None -> { empty with universes = evar_universe_context_from e }
-  | Some ctx -> { empty with universes = ctx }
+let from_env e = 
+  { empty with universes = UState.make (Environ.universes e) }
+
+let from_ctx ctx = { empty with universes = ctx }
 
 let has_undefined evd = not (EvMap.is_empty evd.undf_evars)
 
@@ -799,14 +646,8 @@ let add_conv_pb ?(tail=false) pb d =
 
 let evar_source evk d = (find d evk).evar_source
 
-let evar_ident evk evd =
-  try EvMap.find evk (fst evd.evar_names)
-  with Not_found ->
-    (* Unnamed (non-dependent) evar *)
-    add_suffix (Id.of_string "X") (string_of_int (Evar.repr evk))
-
-let evar_key id evd =
-  Idmap.find id (snd evd.evar_names)
+let evar_ident evk evd = EvNames.ident evk evd.evar_names
+let evar_key id evd = EvNames.key id evd.evar_names
 
 let define_aux def undef evk body =
   let oldinfo =
@@ -828,42 +669,23 @@ let define evk body evd =
   | [] ->  evd.last_mods
   | _ -> Evar.Set.add evk evd.last_mods
   in
-  let evar_names = remove_name_defined evk evd.evar_names in
+  let evar_names = EvNames.remove_name_defined evk evd.evar_names in
   { evd with defn_evars; undf_evars; last_mods; evar_names }
 
-let evar_declare hyps evk ty ?(src=(Loc.ghost,Evar_kinds.InternalHole)) 
-    ?(filter=Filter.identity) ?candidates ?(store=Store.empty)
-    ?(naming=Misctypes.IntroAnonymous) evd =
-  let () = match Filter.repr filter with
-  | None -> ()
-  | Some filter ->
-    assert (Int.equal (List.length filter) (List.length (named_context_of_val hyps)))
-  in
-  let evar_info = {
-    evar_hyps = hyps;
-    evar_concl = ty;
-    evar_body = Evar_empty;
-    evar_filter = filter;
-    evar_source = src;
-    evar_candidates = candidates;
-    evar_extra = store; }
-  in
-  let evar_names = add_name_newly_undefined naming evk evar_info evd.evar_names in
-  { evd with undf_evars = EvMap.add evk evar_info evd.undf_evars; evar_names }
-
-let restrict evk evk' filter ?candidates evd =
+let restrict evk filter ?candidates evd =
+  let evk' = new_untyped_evar () in
   let evar_info = EvMap.find evk evd.undf_evars in
   let evar_info' =
     { evar_info with evar_filter = filter;
       evar_candidates = candidates;
       evar_extra = Store.empty } in
-  let evar_names = reassign_name_defined evk evk' evd.evar_names in
+  let evar_names = EvNames.reassign_name_defined evk evk' evd.evar_names in
   let ctxt = Filter.filter_list filter (evar_context evar_info) in
-  let id_inst = Array.map_of_list (fun (id,_,_) -> mkVar id) ctxt in
+  let id_inst = Array.map_of_list (mkVar % get_id) ctxt in
   let body = mkEvar(evk',id_inst) in
   let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
   { evd with undf_evars = EvMap.add evk' evar_info' undf_evars;
-    defn_evars; evar_names }
+    defn_evars; evar_names }, evk'
 
 let downcast evk ccl evd =
   let evar_info = EvMap.find evk evd.undf_evars in
@@ -921,10 +743,10 @@ let evars_of_term c =
   evrec Evar.Set.empty c
 
 let evars_of_named_context nc =
-  List.fold_right (fun (_, b, t) s ->
+  List.fold_right (fun decl s ->
     Option.fold_left (fun s t ->
       Evar.Set.union s (evars_of_term t))
-      (Evar.Set.union s (evars_of_term t)) b)
+      (Evar.Set.union s (evars_of_term (get_type decl))) (get_value decl))
     nc Evar.Set.empty
 
 let evars_of_filtered_evar_info evi =
@@ -936,41 +758,9 @@ let evars_of_filtered_evar_info evi =
 	(evars_of_named_context (evar_filtered_context evi)))
 
 (**********************************************************)
-(* Side effects *)
-
-let emit_side_effects eff evd =
-  { evd with effects = Declareops.union_side_effects eff evd.effects; }
-
-let drop_side_effects evd =
-  { evd with effects = Declareops.no_seff; }
-
-let eval_side_effects evd = evd.effects
-
-(* Future goals *)
-let declare_future_goal evk evd =
-  { evd with future_goals = evk::evd.future_goals }
-
-let declare_principal_goal evk evd =
-  match evd.principal_future_goal with
-  | None -> { evd with
-    future_goals = evk::evd.future_goals;
-    principal_future_goal=Some evk; }
-  | Some _ -> Errors.error "Only one main subgoal per instantiation."
-
-let future_goals evd = evd.future_goals
-
-let principal_future_goal evd = evd.principal_future_goal
-
-let reset_future_goals evd =
-  { evd with future_goals = [] ; principal_future_goal=None }
-
-let restore_future_goals evd gls pgl =
-  { evd with future_goals = gls ; principal_future_goal = pgl }
-
-(**********************************************************)
 (* Sort variables *)
 
-type rigid = 
+type rigid = UState.rigid =
   | UnivRigid
   | UnivFlexible of bool (** Is substitution by an algebraic ok? *)
 
@@ -980,133 +770,80 @@ let univ_flexible_alg = UnivFlexible true
 
 let evar_universe_context d = d.universes
 
-let universe_context_set d = d.universes.uctx_local
+let universe_context_set d = UState.context_set d.universes
 
-let universe_context evd =
-  Univ.ContextSet.to_context evd.universes.uctx_local
+let pr_uctx_level = UState.pr_uctx_level
+let universe_context ?names evd = UState.universe_context ?names evd.universes
+
+let restrict_universe_context evd vars =
+  { evd with universes = UState.restrict evd.universes vars }
 
 let universe_subst evd =
-  evd.universes.uctx_univ_variables
-
-let merge_uctx rigid uctx ctx' =
-  let open Univ in
-  let uctx = 
-    match rigid with
-    | UnivRigid -> uctx
-    | UnivFlexible b ->
-      let levels = ContextSet.levels ctx' in
-      let fold u accu =
-        if LMap.mem u accu then accu
-        else LMap.add u None accu
-      in
-      let uvars' = LSet.fold fold levels uctx.uctx_univ_variables in
-	if b then
-	  { uctx with uctx_univ_variables = uvars';
-	  uctx_univ_algebraic = LSet.union uctx.uctx_univ_algebraic levels }
-	else { uctx with uctx_univ_variables = uvars' }
-  in
-  let uctx_local = ContextSet.append ctx' uctx.uctx_local in
-  let uctx_universes = merge_constraints (ContextSet.constraints ctx') uctx.uctx_universes in
-  { uctx with uctx_local; uctx_universes }
+  UState.subst evd.universes
 
-let merge_context_set rigid evd ctx' = 
-  {evd with universes = merge_uctx rigid evd.universes ctx'}
+let merge_context_set ?loc ?(sideff=false) rigid evd ctx' =
+  {evd with universes = UState.merge ?loc sideff rigid evd.universes ctx'}
 
-let merge_uctx_subst uctx s =
-  { uctx with uctx_univ_variables = Univ.LMap.subst_union uctx.uctx_univ_variables s }
-      
 let merge_universe_subst evd subst = 
-  {evd with universes = merge_uctx_subst evd.universes subst }
-
-let with_context_set rigid d (a, ctx) = 
-  (merge_context_set rigid d ctx, a)
-
-let add_uctx_names s l (names, names_rev) =
-    (UNameMap.add s l names, Univ.LMap.add l s names_rev)
-
-let uctx_new_univ_variable rigid name
-  ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) =
-  let u = Universes.new_univ_level (Global.current_dirpath ()) in
-  let ctx' = Univ.ContextSet.add_universe u ctx in
-  let uctx' = 
-    match rigid with
-    | UnivRigid -> uctx
-    | UnivFlexible b -> 
-      let uvars' = Univ.LMap.add u None uvars in
-	if b then {uctx with uctx_univ_variables = uvars';
-	  uctx_univ_algebraic = Univ.LSet.add u avars}
-	else {uctx with uctx_univ_variables = Univ.LMap.add u None uvars} in
-  let names = 
-    match name with
-    | Some n -> add_uctx_names n u uctx.uctx_names
-    | None -> uctx.uctx_names
-  in
-    {uctx' with uctx_names = names; uctx_local = ctx';
-      uctx_universes = Univ.add_universe u uctx.uctx_universes}, u
+  {evd with universes = UState.merge_subst evd.universes subst }
+
+let with_context_set ?loc rigid d (a, ctx) =
+  (merge_context_set ?loc rigid d ctx, a)
 
-let new_univ_level_variable ?name rigid evd =
-  let uctx', u = uctx_new_univ_variable rigid name evd.universes in
+let new_univ_level_variable ?loc ?name ?(predicative=true) rigid evd =
+  let uctx', u = UState.new_univ_variable ?loc rigid name evd.universes in
     ({evd with universes = uctx'}, u)
 
-let new_univ_variable ?name rigid evd =
-  let uctx', u = uctx_new_univ_variable rigid name evd.universes in
+let new_univ_variable ?loc ?name ?(predicative=true) rigid evd =
+  let uctx', u = UState.new_univ_variable ?loc rigid name evd.universes in
     ({evd with universes = uctx'}, Univ.Universe.make u)
 
-let new_sort_variable ?name rigid d =
-  let (d', u) = new_univ_variable rigid ?name d in
+let new_sort_variable ?loc ?name ?(predicative=true) rigid d =
+  let (d', u) = new_univ_variable ?loc rigid ?name ~predicative d in
     (d', Type u)
 
+let add_global_univ d u =
+  { d with universes = UState.add_global_univ d.universes u }
+
 let make_flexible_variable evd b u =
-  let {uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as ctx = evd.universes in
-  let uvars' = Univ.LMap.add u None uvars in
-  let avars' = 
-    if b then
-      let uu = Univ.Universe.make u in
-      let substu_not_alg u' v =
-	Option.cata (fun vu -> Univ.Universe.equal uu vu && not (Univ.LSet.mem u' avars)) false v
-      in
-	if not (Univ.LMap.exists substu_not_alg uvars)
-	then Univ.LSet.add u avars else avars 
-    else avars 
-  in
-    {evd with universes = {ctx with uctx_univ_variables = uvars'; 
-      uctx_univ_algebraic = avars'}}
+  { evd with universes = UState.make_flexible_variable evd.universes b u }
+
+let make_evar_universe_context e l =
+  let uctx = UState.make (Environ.universes e) in
+  match l with
+  | None -> uctx
+  | Some us ->
+      List.fold_left
+        (fun uctx (loc,id) ->
+        fst (UState.new_univ_variable ~loc univ_rigid (Some (Id.to_string id)) uctx))
+        uctx us
 
 (****************************************)
 (* Operations on constants              *)
 (****************************************)
 
-let fresh_sort_in_family ?(rigid=univ_flexible) env evd s = 
-  with_context_set rigid evd (Universes.fresh_sort_in_family env s)
+let fresh_sort_in_family ?loc ?(rigid=univ_flexible) env evd s = 
+  with_context_set ?loc rigid evd (Universes.fresh_sort_in_family env s)
 
-let fresh_constant_instance env evd c =
-  with_context_set univ_flexible evd (Universes.fresh_constant_instance env c)
+let fresh_constant_instance ?loc env evd c =
+  with_context_set ?loc univ_flexible evd (Universes.fresh_constant_instance env c)
 
-let fresh_inductive_instance env evd i =
-  with_context_set univ_flexible evd (Universes.fresh_inductive_instance env i)
+let fresh_inductive_instance ?loc env evd i =
+  with_context_set ?loc univ_flexible evd (Universes.fresh_inductive_instance env i)
 
-let fresh_constructor_instance env evd c =
-  with_context_set univ_flexible evd (Universes.fresh_constructor_instance env c)
+let fresh_constructor_instance ?loc env evd c =
+  with_context_set ?loc univ_flexible evd (Universes.fresh_constructor_instance env c)
 
-let fresh_global ?(rigid=univ_flexible) ?names env evd gr =
-  with_context_set rigid evd (Universes.fresh_global_instance ?names env gr)
+let fresh_global ?loc ?(rigid=univ_flexible) ?names env evd gr =
+  with_context_set ?loc rigid evd (Universes.fresh_global_instance ?names env gr)
 
 let whd_sort_variable evd t = t
 
-let is_sort_variable evd s = 
-  match s with 
-  | Type u -> 
-    (match Univ.universe_level u with
-    | Some l as x -> 
-      let uctx = evd.universes in
-	if Univ.LSet.mem l (Univ.ContextSet.levels uctx.uctx_local) then x
-	else None
-    | None -> None)
-  | _ -> None
+let is_sort_variable evd s = UState.is_sort_variable evd.universes s
 
 let is_flexible_level evd l = 
   let uctx = evd.universes in
-    Univ.LMap.mem l uctx.uctx_univ_variables
+    Univ.LMap.mem l (UState.subst uctx)
 
 let is_eq_sort s1 s2 =
   if Sorts.equal s1 s2 then None
@@ -1117,12 +854,12 @@ let is_eq_sort s1 s2 =
       else Some (u1, u2)
 
 let normalize_universe evd =
-  let vars = ref evd.universes.uctx_univ_variables in
+  let vars = ref (UState.subst evd.universes) in
   let normalize = Universes.normalize_universe_opt_subst vars in
     normalize
 
 let normalize_universe_instance evd l =
-  let vars = ref evd.universes.uctx_univ_variables in
+  let vars = ref (UState.subst evd.universes) in
   let normalize = Univ.level_subst_of (Universes.normalize_univ_variable_opt_subst vars) in
     Univ.Instance.subst_fn normalize l
 
@@ -1146,12 +883,9 @@ let set_eq_sort env d s1 s2 =
       d
 
 let has_lub evd u1 u2 =
-  (* let normalize = Universes.normalize_universe_opt_subst (ref univs.uctx_univ_variables) in *)
-  (* (\* let dref, norm = memo_normalize_universe d in *\) *)
-  (* let u1 = normalize u1 and u2 = normalize u2 in *)
-    if Univ.Universe.equal u1 u2 then evd
-    else add_universe_constraints evd
-      (Universes.Constraints.singleton (u1,Universes.ULub,u2))
+  if Univ.Universe.equal u1 u2 then evd
+  else add_universe_constraints evd
+    (Universes.Constraints.singleton (u1,Universes.ULub,u2))
 
 let set_eq_level d u1 u2 =
   add_constraints d (Univ.enforce_eq_level u1 u2 Univ.Constraint.empty)
@@ -1169,104 +903,29 @@ let set_leq_sort env evd s1 s2 =
   match is_eq_sort s1 s2 with
   | None -> evd
   | Some (u1, u2) ->
-    (* if Univ.is_type0_univ u2 then *)
-    (*   if Univ.is_small_univ u1 then evd *)
-    (*   else raise (Univ.UniverseInconsistency (Univ.Le, u1, u2, [])) *)
-    (* else if Univ.is_type0m_univ u2 then  *)
-    (*   raise (Univ.UniverseInconsistency (Univ.Le, u1, u2, [])) *)
-    (* else  *)
-      if not (type_in_type env) then
-      add_universe_constraints evd (Universes.Constraints.singleton (u1,Universes.ULe,u2))
-      else evd
+     if not (type_in_type env) then
+       add_universe_constraints evd (Universes.Constraints.singleton (u1,Universes.ULe,u2))
+     else evd
 	    
 let check_eq evd s s' =
-  Univ.check_eq evd.universes.uctx_universes s s'
+  UGraph.check_eq (UState.ugraph evd.universes) s s'
 
 let check_leq evd s s' =
-  Univ.check_leq evd.universes.uctx_universes s s'
+  UGraph.check_leq (UState.ugraph evd.universes) s s'
 
-let subst_univs_context_with_def def usubst (ctx, cst) =
-  (Univ.LSet.diff ctx def, Univ.subst_univs_constraints usubst cst)
+let normalize_evar_universe_context_variables = UState.normalize_variables
 
-let normalize_evar_universe_context_variables uctx =
-  let normalized_variables, undef, def, subst = 
-    Universes.normalize_univ_variables uctx.uctx_univ_variables 
-  in
-  let ctx_local = subst_univs_context_with_def def (Univ.make_subst subst) uctx.uctx_local in
-  let ctx_local', univs = Universes.refresh_constraints uctx.uctx_initial_universes ctx_local in
-    subst, { uctx with uctx_local = ctx_local';
-      uctx_univ_variables = normalized_variables;
-      uctx_universes = univs }
-
-(* let normvarsconstrkey = Profile.declare_profile "normalize_evar_universe_context_variables";; *)
-(* let normalize_evar_universe_context_variables = *)
-(*   Profile.profile1 normvarsconstrkey normalize_evar_universe_context_variables;; *)
-    
-let abstract_undefined_variables uctx =
-  let vars' = 
-    Univ.LMap.fold (fun u v acc ->
-      if v == None then Univ.LSet.remove u acc
-      else acc)
-    uctx.uctx_univ_variables uctx.uctx_univ_algebraic
-  in { uctx with uctx_local = Univ.ContextSet.empty;
-      uctx_univ_algebraic = vars' }
-
-let fix_undefined_variables ({ universes = uctx } as evm) =
-  let algs', vars' = 
-    Univ.LMap.fold (fun u v (algs, vars as acc) ->
-      if v == None then (Univ.LSet.remove u algs, Univ.LMap.remove u vars)
-      else acc)
-      uctx.uctx_univ_variables 
-      (uctx.uctx_univ_algebraic, uctx.uctx_univ_variables)
-  in
-    {evm with universes = 
-	{ uctx with uctx_univ_variables = vars';
-	  uctx_univ_algebraic = algs' } }
+let abstract_undefined_variables = UState.abstract_undefined_variables
 
-
-let refresh_undefined_univ_variables uctx =
-  let subst, ctx' = Universes.fresh_universe_context_set_instance uctx.uctx_local in
-  let alg = Univ.LSet.fold (fun u acc -> Univ.LSet.add (Univ.subst_univs_level_level subst u) acc) 
-    uctx.uctx_univ_algebraic Univ.LSet.empty 
-  in
-  let vars = 
-    Univ.LMap.fold
-      (fun u v acc ->
-	Univ.LMap.add (Univ.subst_univs_level_level subst u) 
-          (Option.map (Univ.subst_univs_level_universe subst) v) acc)
-      uctx.uctx_univ_variables Univ.LMap.empty
-  in 
-  let uctx' = {uctx_names = uctx.uctx_names;
-	       uctx_local = ctx'; 
-	       uctx_univ_variables = vars; uctx_univ_algebraic = alg;
-	       uctx_universes = Univ.initial_universes;
-	       uctx_initial_universes = uctx.uctx_initial_universes } in
-    uctx', subst
+let fix_undefined_variables evd =
+  { evd with universes = UState.fix_undefined_variables evd.universes }
 
 let refresh_undefined_universes evd =
-  let uctx', subst = refresh_undefined_univ_variables evd.universes in
+  let uctx', subst = UState.refresh_undefined_univ_variables evd.universes in
   let evd' = cmap (subst_univs_level_constr subst) {evd with universes = uctx'} in
     evd', subst
 
-let normalize_evar_universe_context uctx = 
-  let rec fixpoint uctx = 
-    let ((vars',algs'), us') = 
-      Universes.normalize_context_set uctx.uctx_local uctx.uctx_univ_variables
-        uctx.uctx_univ_algebraic
-    in
-      if Univ.LSet.equal (fst us') (fst uctx.uctx_local) then 
-        uctx
-      else
-	let us', universes = Universes.refresh_constraints uctx.uctx_initial_universes us' in
-	let uctx' = 
-	  { uctx_names = uctx.uctx_names;
-	    uctx_local = us'; 
-	    uctx_univ_variables = vars'; 
-	    uctx_univ_algebraic = algs';
-	    uctx_universes = universes;
-	    uctx_initial_universes = uctx.uctx_initial_universes }
-	in fixpoint uctx'
-  in fixpoint uctx
+let normalize_evar_universe_context = UState.normalize
 
 let nf_univ_variables evd = 
   let subst, uctx' = normalize_evar_universe_context_variables evd.universes in
@@ -1278,55 +937,81 @@ let nf_constraints evd =
   let uctx' = normalize_evar_universe_context uctx' in
     {evd with universes = uctx'}
 
-let nf_constraints = 
-  if Flags.profile then
-    let nfconstrkey = Profile.declare_profile "nf_constraints" in
-      Profile.profile1 nfconstrkey nf_constraints
-  else nf_constraints
-
-let universe_of_name evd s = 
-  UNameMap.find s (fst evd.universes.uctx_names)
+let universe_of_name evd s = UState.universe_of_name evd.universes s
 
 let add_universe_name evd s l =
-  let names' = add_uctx_names s l evd.universes.uctx_names in
-    {evd with universes = {evd.universes with uctx_names = names'}}
+  { evd with universes = UState.add_universe_name evd.universes s l }
 
-let universes evd = evd.universes.uctx_universes
+let universes evd = UState.ugraph evd.universes
+
+let update_sigma_env evd env =
+  { evd with universes = UState.update_sigma_env evd.universes env }
 
 (* Conversion w.r.t. an evar map and its local universes. *)
 
-let conversion_gen env evd pb t u =
+let test_conversion_gen env evd pb t u =
   match pb with 
   | Reduction.CONV -> 
-    Reduction.trans_conv_universes 
-      full_transparent_state ~evars:(existential_opt_value evd) env 
-      evd.universes.uctx_universes t u
-  | Reduction.CUMUL -> Reduction.trans_conv_leq_universes
-     full_transparent_state ~evars:(existential_opt_value evd) env 
-    evd.universes.uctx_universes t u
-
-(* let conversion_gen_key = Profile.declare_profile "conversion_gen" *)
-(* let conversion_gen = Profile.profile5 conversion_gen_key conversion_gen *)
-
-let conversion env d pb t u =
-  conversion_gen env d pb t u; d
+    Reduction.conv env
+      ~evars:((existential_opt_value evd), (UState.ugraph evd.universes))
+      t u
+  | Reduction.CUMUL -> Reduction.conv_leq env
+      ~evars:((existential_opt_value evd), (UState.ugraph evd.universes))
+      t u
 
 let test_conversion env d pb t u =
-  try conversion_gen env d pb t u; true
+  try test_conversion_gen env d pb t u; true
   with _ -> false
 
+exception UniversesDiffer = UState.UniversesDiffer
+
 let eq_constr_univs evd t u =
-  let b, c = Universes.eq_constr_univs_infer evd.universes.uctx_universes t u in
-    if b then 
-      try let evd' = add_universe_constraints evd c in evd', b
-      with Univ.UniverseInconsistency _ | UniversesDiffer -> evd, false
-    else evd, b
+  let fold cstr sigma =
+    try Some (add_universe_constraints sigma cstr)
+    with Univ.UniverseInconsistency _ | UniversesDiffer -> None
+  in
+  match Universes.eq_constr_univs_infer (UState.ugraph evd.universes) fold t u evd with
+  | None -> evd, false
+  | Some evd -> evd, true
 
 let e_eq_constr_univs evdref t u =
   let evd, b = eq_constr_univs !evdref t u in
     evdref := evd; b
 
 (**********************************************************)
+(* Side effects *)
+
+let emit_side_effects eff evd =
+  { evd with effects = Safe_typing.concat_private eff evd.effects;
+	     universes = UState.emit_side_effects eff evd.universes }
+
+let drop_side_effects evd =
+  { evd with effects = Safe_typing.empty_private_constants; }
+
+let eval_side_effects evd = evd.effects
+
+(* Future goals *)
+let declare_future_goal evk evd =
+  { evd with future_goals = evk::evd.future_goals }
+
+let declare_principal_goal evk evd =
+  match evd.principal_future_goal with
+  | None -> { evd with
+    future_goals = evk::evd.future_goals;
+    principal_future_goal=Some evk; }
+  | Some _ -> Errors.error "Only one main subgoal per instantiation."
+
+let future_goals evd = evd.future_goals
+
+let principal_future_goal evd = evd.principal_future_goal
+
+let reset_future_goals evd =
+  { evd with future_goals = [] ; principal_future_goal=None }
+
+let restore_future_goals evd gls pgl =
+  { evd with future_goals = gls ; principal_future_goal = pgl }
+
+(**********************************************************)
 (* Accessing metas *)
 
 (** We use this function to overcome OCaml compiler limitations and to prevent
@@ -1342,7 +1027,7 @@ let set_metas evd metas = {
   evar_names = evd.evar_names;
   future_goals = evd.future_goals;
   principal_future_goal = evd.principal_future_goal;
-  extras = Store.empty;
+  extras = evd.extras;
 }
 
 let meta_list evd = metamap_to_list evd.metas
@@ -1362,6 +1047,10 @@ let map_metas_fvalue f evd =
   in
   set_metas evd (Metamap.smartmap map evd.metas)
 
+let map_metas f evd =
+  let map cl = map_clb f cl in
+  set_metas evd (Metamap.smartmap map evd.metas)
+
 let meta_opt_fvalue evd mv =
   match Metamap.find mv evd.metas with
     | Clval(_,b,_) -> Some b
@@ -1415,44 +1104,14 @@ let meta_reassign mv (v, pb) evd =
 let meta_name evd mv =
   try fst (clb_name (Metamap.find mv evd.metas)) with Not_found -> Anonymous
 
-let explain_no_such_bound_variable evd id =
-  let mvl =
-    List.rev (Metamap.fold (fun n clb l ->
-      let na = fst (clb_name clb) in
-      if na != Anonymous then out_name na :: l else l)
-    evd.metas []) 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 (mvl,mvnodef) =
-    Metamap.fold
-      (fun n clb (l1,l2 as l) ->
-        let (na',def) = clb_name clb in
-        if Name.equal na na' then if def then (n::l1,l2) else (n::l1,n::l2)
-        else l)
-      evd.metas ([],[]) 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 clear_metas evd = {evd with metas = Metamap.empty}
 
-let meta_merge evd1 evd2 =
+let meta_merge ?(with_univs = true) evd1 evd2 =
   let metas = Metamap.fold Metamap.add evd1.metas evd2.metas in
-  let universes = union_evar_universe_context evd2.universes evd1.universes in
+  let universes =
+    if with_univs then union_evar_universe_context evd2.universes evd1.universes
+    else evd2.universes
+  in
   {evd2 with universes; metas; }
 
 type metabinding = metavariable * constr * instance_status
@@ -1468,18 +1127,6 @@ let retract_coercible_metas evd =
   let metas = Metamap.smartmapi map evd.metas in
   !mc, set_metas evd metas
 
-let subst_defined_metas_evars (bl,el) c =
-  let rec substrec c = match kind_of_term c with
-    | Meta i ->
-      let select (j,_,_) = Int.equal i j in
-      substrec (pi2 (List.find select bl))
-    | Evar (evk,args) ->
-      let select (_,(evk',args'),_) = Evar.equal evk evk' && Array.equal Constr.equal args args' in
-      (try substrec (pi3 (List.find select el))
-       with Not_found -> map_constr substrec c)
-    | _ -> map_constr substrec c
-  in try Some (substrec c) with Not_found -> None
-
 let evar_source_of_meta mv evd =
   match meta_name evd mv with
   | Anonymous -> (Loc.ghost,Evar_kinds.GoalEvar)
@@ -1570,7 +1217,34 @@ type unsolvability_explanation = SeveralInstancesFound of int
 (**********************************************************)
 (* Pretty-printing *)
 
-let pr_existential_key sigma evk = str "?" ++ pr_id (evar_ident evk sigma)
+let pr_evar_suggested_name evk sigma =
+  let base_id evk' evi =
+  match evar_ident evk' sigma with
+  | Some id -> id
+  | None -> match evi.evar_source with
+  | _,Evar_kinds.ImplicitArg (c,(n,Some id),b) -> id
+  | _,Evar_kinds.VarInstance id -> id
+  | _,Evar_kinds.GoalEvar -> Id.of_string "Goal"
+  | _ ->
+      let env = reset_with_named_context evi.evar_hyps (Global.env()) in
+      Namegen.id_of_name_using_hdchar env evi.evar_concl Anonymous
+  in
+  let names = EvMap.mapi base_id sigma.undf_evars in
+  let id = EvMap.find evk names in
+  let fold evk' id' (seen, n) =
+    if seen then (seen, n)
+    else if Evar.equal evk evk' then (true, n)
+    else if Id.equal id id' then (seen, succ n)
+    else (seen, n)
+  in
+  let (_, n) = EvMap.fold fold names (false, 0) in
+  if n = 0 then id else Nameops.add_suffix id (string_of_int (pred n))
+
+let pr_existential_key sigma evk = match evar_ident evk sigma with
+| None ->
+  str "?" ++ pr_id (pr_evar_suggested_name evk sigma)
+| Some id ->
+  str "?" ++ pr_id id
 
 let pr_instance_status (sc,typ) =
   begin match sc with
@@ -1602,13 +1276,14 @@ let pr_meta_map mmap =
   in
   prlist pr_meta_binding (metamap_to_list mmap)
 
-let pr_decl ((id,b,_),ok) =
-  match b with
+let pr_decl (decl,ok) =
+  let id = get_id decl in
+  match get_value decl with
   | None -> if ok then pr_id id else (str "{" ++ pr_id id ++ str "}")
   | Some c -> str (if ok then "(" else "{") ++ pr_id id ++ str ":=" ++
       print_constr c ++ str (if ok then ")" else "}")
 
-let rec pr_evar_source = function
+let pr_evar_source = function
   | Evar_kinds.QuestionMark _ -> str "underscore"
   | Evar_kinds.CasesType false -> str "pattern-matching return predicate"
   | Evar_kinds.CasesType true ->
@@ -1703,13 +1378,6 @@ let evar_dependency_closure n sigma =
 let has_no_evar sigma =
   EvMap.is_empty sigma.defn_evars && EvMap.is_empty sigma.undf_evars
 
-let pr_uctx_level uctx = 
-  let map, map_rev = uctx.uctx_names in 
-    fun l ->
-      try str(Univ.LMap.find l map_rev)
-      with Not_found -> 
-	Universes.pr_with_global_universes l
-
 let pr_evd_level evd = pr_uctx_level evd.universes
 
 let pr_evar_universe_context ctx =
@@ -1717,18 +1385,19 @@ let pr_evar_universe_context ctx =
   if is_empty_evar_universe_context ctx then mt ()
   else
     (str"UNIVERSES:"++brk(0,1)++ 
-       h 0 (Univ.pr_universe_context_set prl ctx.uctx_local) ++ fnl () ++
+       h 0 (Univ.pr_universe_context_set prl (evar_universe_context_set ctx)) ++ fnl () ++
      str"ALGEBRAIC UNIVERSES:"++brk(0,1)++
-     h 0 (Univ.LSet.pr prl ctx.uctx_univ_algebraic) ++ fnl() ++
+     h 0 (Univ.LSet.pr prl (UState.algebraics ctx)) ++ fnl() ++
      str"UNDEFINED UNIVERSES:"++brk(0,1)++
-       h 0 (Universes.pr_universe_opt_subst ctx.uctx_univ_variables) ++ fnl())
+       h 0 (Universes.pr_universe_opt_subst (UState.subst ctx)) ++ fnl())
 
 let print_env_short env =
   let pr_body n = function
   | None -> pr_name n
   | Some b -> str "(" ++ pr_name n ++ str " := " ++ print_constr b ++ str ")" in
-  let pr_named_decl (n, b, _) = pr_body (Name n) b in
-  let pr_rel_decl (n, b, _) = pr_body n b in
+  let pr_named_decl decl = pr_body (Name (get_id decl)) (get_value decl) in
+  let pr_rel_decl decl = let open Context.Rel.Declaration in
+                         pr_body (get_name decl) (get_value decl) in
   let nc = List.rev (named_context env) in
   let rc = List.rev (rel_context env) in
     str "[" ++ pr_sequence pr_named_decl nc ++ str "]" ++ spc () ++
@@ -1766,7 +1435,7 @@ let pr_evar_list sigma l =
     h 0 (str (string_of_existential ev) ++
       str "==" ++ pr_evar_info evi ++
       (if evi.evar_body == Evar_empty
-       then str " {" ++ pr_id (evar_ident ev sigma) ++ str "}"
+       then str " {" ++  pr_existential_key sigma ev ++ str "}"
        else mt ()))
   in
   h 0 (prlist_with_sep fnl pr l)
diff --git a/engine/evd.mli b/engine/evd.mli
index f2d8a83350..3ae6e586c1 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
@@ -10,7 +10,6 @@ open Util
 open Loc
 open Names
 open Term
-open Context
 open Environ
 
 (** {5 Existential variables and unification states}
@@ -105,8 +104,8 @@ type evar_info = {
 
 val make_evar : named_context_val -> types -> evar_info
 val evar_concl : evar_info -> constr
-val evar_context : evar_info -> named_context
-val evar_filtered_context : evar_info -> named_context
+val evar_context : evar_info -> Context.Named.t
+val evar_filtered_context : evar_info -> Context.Named.t
 val evar_hyps : evar_info -> named_context_val
 val evar_filtered_hyps : evar_info -> named_context_val
 val evar_body : evar_info -> evar_body
@@ -119,7 +118,7 @@ val map_evar_info : (constr -> constr) -> evar_info -> evar_info
 
 (** {6 Unification state} **)
 
-type evar_universe_context
+type evar_universe_context = UState.t
 (** The universe context associated to an evar map *)
 
 type evar_map
@@ -129,10 +128,13 @@ type evar_map
 val empty : evar_map
 (** The empty evar map. *)
 
-val from_env : ?ctx:evar_universe_context -> env -> evar_map
+val from_env : env -> evar_map
 (** The empty evar map with given universe context, taking its initial 
     universes from env. *)
 
+val from_ctx : evar_universe_context -> evar_map
+(** The empty evar map with given universe context *)
+
 val is_empty : evar_map -> bool
 (** Whether an evarmap is empty. *)
 
@@ -140,6 +142,10 @@ val has_undefined : evar_map -> bool
 (** [has_undefined sigma] is [true] if and only if
     there are uninstantiated evars in [sigma]. *)
 
+val new_evar : evar_map ->
+  ?naming:Misctypes.intro_pattern_naming_expr -> evar_info -> evar_map * evar
+(** Creates a fresh evar mapping to the given information. *)
+
 val add : evar_map -> evar -> evar_info -> evar_map
 (** [add sigma ev info] adds [ev] with evar info [info] in sigma.
     Precondition: ev must not preexist in [sigma]. *)
@@ -216,7 +222,7 @@ val existential_opt_value : evar_map -> existential -> constr option
 (** Same as {!existential_value} but returns an option instead of raising an
     exception. *)
 
-val evar_instance_array : (named_declaration -> 'a -> bool) -> evar_info ->
+val evar_instance_array : (Context.Named.Declaration.t -> 'a -> bool) -> evar_info ->
   'a array -> (Id.t * 'a) list
 
 val instantiate_evar_array : evar_info -> constr -> constr array -> constr
@@ -227,14 +233,8 @@ val evars_reset_evd  : ?with_conv_pbs:bool -> ?with_univs:bool ->
 
 (** {6 Misc} *)
 
-val evar_declare :
-  named_context_val -> evar -> types -> ?src:Loc.t * Evar_kinds.t ->
-      ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t ->
-      ?naming:Misctypes.intro_pattern_naming_expr -> evar_map -> evar_map
-(** Convenience function. Just a wrapper around {!add}. *)
-
-val restrict : evar -> evar -> Filter.t -> ?candidates:constr list ->
-  evar_map -> evar_map
+val restrict : evar -> Filter.t -> ?candidates:constr list ->
+  evar_map -> evar_map * evar
 (** Restrict an undefined evar into a new evar by filtering context and
     possibly limiting the instances to a set of candidates *)
 
@@ -246,7 +246,7 @@ val evar_source : existential_key -> evar_map -> Evar_kinds.t located
 (** Convenience function. Wrapper around {!find} to recover the source of an
     evar in a given evar map. *)
 
-val evar_ident : existential_key -> evar_map -> Id.t
+val evar_ident : existential_key -> evar_map -> Id.t option
 
 val rename : existential_key -> Id.t -> evar_map -> evar_map
 
@@ -258,10 +258,10 @@ val dependent_evar_ident : existential_key -> evar_map -> Id.t
 
 (** {5 Side-effects} *)
 
-val emit_side_effects : Declareops.side_effects -> evar_map -> evar_map
+val emit_side_effects : Safe_typing.private_constants -> evar_map -> evar_map
 (** Push a side-effect into the evar map. *)
 
-val eval_side_effects : evar_map -> Declareops.side_effects
+val eval_side_effects : evar_map -> Safe_typing.private_constants
 (** Return the effects contained in the evar map. *)
 
 val drop_side_effects : evar_map -> evar_map
@@ -422,7 +422,7 @@ val evar_list : constr -> existential list
 val evars_of_term : constr -> Evar.Set.t
   (** including evars in instances of evars *)
 
-val evars_of_named_context : named_context -> Evar.Set.t
+val evars_of_named_context : Context.Named.t -> Evar.Set.t
 
 val evars_of_filtered_evar_info : evar_info -> Evar.Set.t
 
@@ -439,7 +439,6 @@ val meta_opt_fvalue : evar_map -> metavariable -> (constr freelisted * instance_
 val meta_type      : evar_map -> metavariable -> types
 val meta_ftype     : evar_map -> metavariable -> types freelisted
 val meta_name      : evar_map -> metavariable -> Name.t
-val meta_with_name : evar_map -> Id.t -> metavariable
 val meta_declare   :
   metavariable -> types -> ?name:Name.t -> evar_map -> evar_map
 val meta_assign    : metavariable -> constr * instance_status -> evar_map -> evar_map
@@ -448,15 +447,15 @@ val meta_reassign  : metavariable -> constr * instance_status -> evar_map -> eva
 val clear_metas : evar_map -> evar_map
 
 (** [meta_merge evd1 evd2] returns [evd2] extended with the metas of [evd1] *)
-val meta_merge : evar_map -> evar_map -> evar_map
+val meta_merge : ?with_univs:bool -> evar_map -> evar_map -> evar_map
 
 val undefined_metas : evar_map -> metavariable list
 val map_metas_fvalue : (constr -> constr) -> evar_map -> evar_map
+val map_metas : (constr -> constr) -> evar_map -> evar_map
 
 type metabinding = metavariable * constr * instance_status
 
 val retract_coercible_metas : evar_map -> metabinding list * evar_map
-val subst_defined_metas_evars : metabinding list * ('a * existential * constr) list -> constr -> constr option
 
 (** {5 FIXME: Nothing to do here} *)
 
@@ -465,7 +464,7 @@ val subst_defined_metas_evars : metabinding list * ('a * existential * constr) l
 
 (** Rigid or flexible universe variables *)
 
-type rigid = 
+type rigid = UState.rigid =
   | UnivRigid
   | UnivFlexible of bool (** Is substitution by an algebraic ok? *)
 
@@ -475,7 +474,7 @@ val univ_flexible_alg : rigid
 
 type 'a in_evar_universe_context = 'a * evar_universe_context
 
-val evar_universe_context_set : Univ.universe_context -> evar_universe_context -> Univ.universe_context_set
+val evar_universe_context_set : evar_universe_context -> Univ.universe_context_set
 val evar_universe_context_constraints : evar_universe_context -> Univ.constraints
 val evar_context_universe_context : evar_universe_context -> Univ.universe_context
 val evar_universe_context_of : Univ.universe_context_set -> evar_universe_context
@@ -483,13 +482,18 @@ val empty_evar_universe_context : evar_universe_context
 val union_evar_universe_context : evar_universe_context -> evar_universe_context ->
   evar_universe_context
 val evar_universe_context_subst : evar_universe_context -> Universes.universe_opt_subst
+val constrain_variables : Univ.LSet.t -> evar_universe_context -> Univ.constraints
 
+
+val evar_universe_context_of_binders :
+  Universes.universe_binders -> evar_universe_context
+							    
+val make_evar_universe_context : env -> (Id.t located) list option -> evar_universe_context
+val restrict_universe_context : evar_map -> Univ.universe_set -> evar_map							   
 (** Raises Not_found if not a name for a universe in this map. *)
 val universe_of_name : evar_map -> string -> Univ.universe_level
 val add_universe_name : evar_map -> string -> Univ.universe_level -> evar_map
 
-val universes : evar_map -> Univ.universes
-
 val add_constraints_context : evar_universe_context -> 
   Univ.constraints -> evar_universe_context
 
@@ -500,16 +504,17 @@ val normalize_evar_universe_context_variables : evar_universe_context ->
 val normalize_evar_universe_context : evar_universe_context -> 
   evar_universe_context
 
-val new_univ_level_variable : ?name:string -> rigid -> evar_map -> evar_map * Univ.universe_level
-val new_univ_variable : ?name:string -> rigid -> evar_map -> evar_map * Univ.universe
-val new_sort_variable : ?name:string -> rigid -> evar_map -> evar_map * sorts
+val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe_level
+val new_univ_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe
+val new_sort_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * sorts
+val add_global_univ : evar_map -> Univ.Level.t -> evar_map
+											   
 val make_flexible_variable : evar_map -> bool -> Univ.universe_level -> evar_map
 val is_sort_variable : evar_map -> sorts -> Univ.universe_level option 
 (** [is_sort_variable evm s] returns [Some u] or [None] if [s] is 
     not a local sort variable declared in [evm] *)
 val is_flexible_level : evar_map -> Univ.Level.t -> bool
 
-val whd_sort_variable : evar_map -> constr -> constr
 (* val normalize_universe_level : evar_map -> Univ.universe_level -> Univ.universe_level *)
 val normalize_universe : evar_map -> Univ.universe -> Univ.universe
 val normalize_universe_instance : evar_map -> Univ.universe_instance -> Univ.universe_instance
@@ -527,18 +532,19 @@ val check_leq : evar_map -> Univ.universe -> Univ.universe -> bool
 
 val evar_universe_context : evar_map -> evar_universe_context
 val universe_context_set : evar_map -> Univ.universe_context_set
-val universe_context : evar_map -> Univ.universe_context
+val universe_context : ?names:(Id.t located) list -> evar_map ->
+		       (Id.t * Univ.Level.t) list * Univ.universe_context
 val universe_subst : evar_map -> Universes.universe_opt_subst
-val universes : evar_map -> Univ.universes
+val universes : evar_map -> UGraph.t
 
 
 val merge_universe_context : evar_map -> evar_universe_context -> evar_map
 val set_universe_context : evar_map -> evar_universe_context -> evar_map
 
-val merge_context_set : rigid -> evar_map -> Univ.universe_context_set -> evar_map
+val merge_context_set : ?loc:Loc.t -> ?sideff:bool -> rigid -> evar_map -> Univ.universe_context_set -> evar_map
 val merge_universe_subst : evar_map -> Universes.universe_opt_subst -> evar_map
 
-val with_context_set : rigid -> evar_map -> 'a Univ.in_universe_context_set -> evar_map * 'a
+val with_context_set : ?loc:Loc.t -> rigid -> evar_map -> 'a Univ.in_universe_context_set -> evar_map * 'a
 
 val nf_univ_variables : evar_map -> evar_map * Univ.universe_subst
 val abstract_undefined_variables : evar_universe_context -> evar_universe_context
@@ -549,25 +555,24 @@ val refresh_undefined_universes : evar_map -> evar_map * Univ.universe_level_sub
 
 val nf_constraints : evar_map -> evar_map
 
+val update_sigma_env : evar_map -> env -> evar_map
+
 (** Polymorphic universes *)
 
-val fresh_sort_in_family : ?rigid:rigid -> env -> evar_map -> sorts_family -> evar_map * sorts
-val fresh_constant_instance : env -> evar_map -> constant -> evar_map * pconstant
-val fresh_inductive_instance : env -> evar_map -> inductive -> evar_map * pinductive
-val fresh_constructor_instance : env -> evar_map -> constructor -> evar_map * pconstructor
+val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid -> env -> evar_map -> sorts_family -> evar_map * sorts
+val fresh_constant_instance : ?loc:Loc.t -> env -> evar_map -> constant -> evar_map * pconstant
+val fresh_inductive_instance : ?loc:Loc.t -> env -> evar_map -> inductive -> evar_map * pinductive
+val fresh_constructor_instance : ?loc:Loc.t -> env -> evar_map -> constructor -> evar_map * pconstructor
 
-val fresh_global : ?rigid:rigid -> ?names:Univ.Instance.t -> env -> evar_map -> 
+val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> env -> evar_map -> 
   Globnames.global_reference -> evar_map * constr
 
 (********************************************************************
-  Conversion w.r.t. an evar map: might generate universe unifications 
-  that are kept in the evarmap.
-  Raises [NotConvertible]. *)
-
-val conversion : env -> evar_map -> conv_pb -> constr -> constr -> evar_map
+  Conversion w.r.t. an evar map, not unifying universes. See 
+  [Reductionops.infer_conv] for conversion up-to universes. *)
 
 val test_conversion : env -> evar_map -> conv_pb -> constr -> constr -> bool
-(** This one forgets about the assignemts of universes. *)
+(** WARNING: This does not allow unification of universes *)
 
 val eq_constr_univs : evar_map -> constr -> constr -> evar_map * bool
 (** Syntactic equality up to universes, recording the associated constraints *)
@@ -592,6 +597,8 @@ type unsolvability_explanation = SeveralInstancesFound of int
 
 val pr_existential_key : evar_map -> evar -> Pp.std_ppcmds
 
+val pr_evar_suggested_name : existential_key -> evar_map -> Id.t
+
 (** {5 Debug pretty-printers} *)
 
 val pr_evar_info : evar_info -> Pp.std_ppcmds
@@ -608,4 +615,6 @@ val pr_evd_level : evar_map -> Univ.Level.t -> Pp.std_ppcmds
 val create_evar_defs      : evar_map -> evar_map
 (** Create an [evar_map] with empty meta map: *)
 
-val create_goal_evar_defs : evar_map -> evar_map
+(** {5 Summary names} *)
+
+val evar_counter_summary_name : string
diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml
index c88de133d4..4b78bc05d5 100644
--- a/engine/logic_monad.ml
+++ b/engine/logic_monad.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
@@ -94,10 +94,6 @@ struct
 
   let print_char = fun c -> (); fun () -> print_char c
 
-  (** {!Pp.pp}. The buffer is also flushed. *)
-  let print = fun s -> (); fun () -> try Pp.msg_info s; Pp.pp_flush () with e ->
-    let (e, info) = Errors.push e in raise ~info e ()
-
   let timeout = fun n t -> (); fun () ->
     Control.timeout n t (Exception Timeout)
 
@@ -107,6 +103,13 @@ struct
       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
@@ -151,7 +154,7 @@ struct
       shape of the monadic type is reminiscent of that of the
       continuation monad transformer.
 
-      The paper also contains the rational for the [split] abstraction.
+      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
diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli
index 1869f32633..c5160443b1 100644
--- a/engine/logic_monad.mli
+++ b/engine/logic_monad.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
@@ -55,8 +55,13 @@ module NonLogical : sig
 
   val read_line : string t
   val print_char : char -> unit t
-  (** {!Pp.pp}. The buffer is also flushed. *)
-  val print : Pp.std_ppcmds -> 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}. *)
diff --git a/engine/namegen.ml b/engine/namegen.ml
index a88c2e20e3..6b2b585316 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
@@ -22,6 +22,7 @@ open Libnames
 open Globnames
 open Environ
 open Termops
+open Context.Rel.Declaration
 
 (**********************************************************************)
 (* Conventional names *)
@@ -113,7 +114,7 @@ let hdchar env c =
     | Rel n ->
 	(if n<=k then "p" (* the initial term is flexible product/function *)
 	 else
-	   try match Environ.lookup_rel (n-k) env with
+	   try match Environ.lookup_rel (n-k) env |> to_tuple with
 	     | (Name id,_,_)   -> lowercase_first_char id
 	     | (Anonymous,_,t) -> hdrec 0 (lift (n-k) t)
 	   with Not_found -> "y")
@@ -142,10 +143,9 @@ let prod_name = mkProd_name
 let prod_create   env (a,b) = mkProd (named_hd env a Anonymous, a, b)
 let lambda_create env (a,b) =  mkLambda (named_hd env a Anonymous, a, b)
 
-let name_assumption env (na,c,t) =
-  match c with
-    | None      -> (named_hd env t na, None, t)
-    | Some body -> (named_hd env body na, c, t)
+let name_assumption env = function
+    | LocalAssum (na,t) -> LocalAssum (named_hd env t na, t)
+    | LocalDef (na,c,t) -> LocalDef (named_hd env c na, c, t)
 
 let name_context env hyps =
   snd
@@ -277,11 +277,12 @@ let next_name_away = next_name_away_with_default default_non_dependent_string
 let make_all_name_different env =
   let avoid = ref (ids_of_named_context (named_context env)) in
   process_rel_context
-    (fun (na,c,t) newenv ->
+    (fun decl newenv ->
+       let (na,_,t) = to_tuple decl in
        let na = named_hd newenv t na in
        let id = next_name_away na !avoid in
        avoid := id::!avoid;
-       push_rel (Name id,c,t) newenv)
+       push_rel (set_name (Name id) decl) newenv)
     env
 
 (* 5- Looks for next fresh name outside a list; avoids also to use names that
diff --git a/engine/namegen.mli b/engine/namegen.mli
index f66bc6d88c..a2923fee99 100644
--- a/engine/namegen.mli
+++ b/engine/namegen.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
@@ -8,7 +8,6 @@
 
 open Names
 open Term
-open Context
 open Environ
 
 (*********************************************************************
@@ -39,13 +38,13 @@ val lambda_name : env -> Name.t * types * constr -> constr
 
 val prod_create : env -> types * types -> constr
 val lambda_create : env -> types * constr -> constr
-val name_assumption : env -> rel_declaration -> rel_declaration
-val name_context : env -> rel_context -> rel_context
+val name_assumption : env -> Context.Rel.Declaration.t -> Context.Rel.Declaration.t
+val name_context : env -> Context.Rel.t -> Context.Rel.t
 
-val mkProd_or_LetIn_name : env -> types -> rel_declaration -> types
-val mkLambda_or_LetIn_name : env -> constr -> rel_declaration -> constr
-val it_mkProd_or_LetIn_name   : env -> types -> rel_context -> types
-val it_mkLambda_or_LetIn_name : env -> constr -> rel_context -> constr
+val mkProd_or_LetIn_name : env -> types -> Context.Rel.Declaration.t -> types
+val mkLambda_or_LetIn_name : env -> constr -> Context.Rel.Declaration.t -> constr
+val it_mkProd_or_LetIn_name   : env -> types -> Context.Rel.t -> types
+val it_mkLambda_or_LetIn_name : env -> constr -> Context.Rel.t -> constr
 
 (*********************************************************************
    Fresh names *)
diff --git a/engine/proofview.ml b/engine/proofview.ml
new file mode 100644
index 0000000000..ba664cafaf
--- /dev/null
+++ b/engine/proofview.ml
@@ -0,0 +1,1211 @@
+(************************************************************************)
+(*  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
+open Sigma.Notations
+open Context.Named.Declaration
+
+(** 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 typeclass_resolvable = Evd.Store.field ()
+
+let dependent_init =
+  (* Goals are created with a store which marks them as unresolvable
+     for type classes. *)
+  let store = Evd.Store.set Evd.Store.empty typeclass_resolvable () 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 = Sigma.Unsafe.of_evar_map sigma in
+    let Sigma (econstr, sigma, _) = Evarutil.new_evar env sigma ~src ~store typ in
+    let sigma = Sigma.to_evar_map sigma 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 -> std_ppcmds) ref = ref (fun n -> mt ())
+let set_nosuchgoals_hook f = nosuchgoals_hook := f
+
+
+
+(* This uses the hook above *)
+let _ = Errors.register_handler begin function
+  | NoSuchGoals n ->
+    let suffix = !nosuchgoals_hook n in
+    Errors.errorlabstrm ""
+      (str "No such " ++ str (String.plural n "goal") ++ 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] returns the list of unifiable goals 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 None
+  | 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
+      tclUNIT (Some 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 d1 d2 =
+      match d1, d2 with
+      | LocalAssum (i1,t1), LocalAssum (i2,t2) ->
+         Names.Id.equal i1 i2 && eq_constr sigma1 sigma2 t1 t2
+      | LocalDef (i1,c1,t1), LocalDef (i2,c2,t2) ->
+         Names.Id.equal i1 i2 && eq_constr sigma1 sigma2 c1 c2
+         && eq_constr sigma1 sigma2 t1 t2
+      | _ ->
+         false
+    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 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 = match Evd.Store.get info.Evd.evar_extra typeclass_resolvable with
+    | None -> { info with Evd.evar_extra = Evd.Store.set info.Evd.evar_extra typeclass_resolvable () }
+    | Some () -> info
+    in
+    Evd.add evd content info
+
+  let advance = advance
+
+  let typeclass_resolvable = typeclass_resolvable
+
+end
+
+module UnsafeRepr = Proof.Unsafe
+
+let (>>=) = tclBIND
+let (<*>) = tclTHEN
+let (<+>) t1 t2 = tclOR t1 (fun _ -> t2)
+
+(** {6 Goal-dependent tactics} *)
+
+let goal_env evars gl =
+  let evi = Evd.find evars gl in
+  Evd.evar_filtered_env evi
+
+let goal_nf_evar sigma gl =
+  let evi = Evd.find sigma gl in
+  let evi = Evarutil.nf_evar_info sigma evi in
+  let sigma = Evd.add sigma gl evi in
+  (gl, sigma)
+
+let goal_extra evars gl =
+  let evi = Evd.find evars gl in
+  evi.Evd.evar_extra
+
+
+let catchable_exception = function
+  | Logic_monad.Exception _ -> false
+  | e -> Errors.noncritical e
+
+
+module Goal = struct
+
+  type ('a, 'r) t = {
+    env : Environ.env;
+    sigma : Evd.evar_map;
+    concl : Term.constr ;
+    self : Evar.t ; (* for compatibility with old-style definitions *)
+  }
+
+  type ('a, 'b) enter =
+    { enter : 'r. ('a, 'r) t -> 'b }
+
+  let assume (gl : ('a, 'r) t) = (gl :> ([ `NF ], 'r) t)
+
+  let env { env=env } = env
+  let sigma { sigma=sigma } = Sigma.Unsafe.of_evar_map sigma
+  let hyps { env=env } = Environ.named_context env
+  let concl { concl=concl } = concl
+  let extra { sigma=sigma; self=self } = goal_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.enter 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.enter 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
+
+  type ('a, 'b) s_enter =
+    { s_enter : 'r. ('a, 'r) t -> ('b, 'r) Sigma.sigma }
+
+  let s_enter f =
+    InfoL.tag (Info.Dispatch) begin
+    iter_goal begin fun goal ->
+      Env.get >>= fun env ->
+      tclEVARMAP >>= fun sigma ->
+      try
+        let gl = gmake env sigma goal in
+        let Sigma (tac, sigma, _) = f.s_enter gl in
+        let sigma = Sigma.to_evar_map sigma in
+        tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) tac)
+      with e when catchable_exception e ->
+        let (e, info) = Errors.push e in
+        tclZERO ~info e
+    end
+    end
+
+  let nf_s_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
+        let Sigma (tac, sigma, _) = f.s_enter gl in
+        let sigma = Sigma.to_evar_map sigma in
+        tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) tac)
+      with e when catchable_exception e ->
+        let (e, info) = Errors.push e in
+        tclZERO ~info e
+    end
+    end
+
+  let goals =
+    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 =
+          Env.get >>= fun env ->
+          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
+
+  let lift (gl : ('a, 'r) t) _ = (gl :> ('a, 's) t)
+
+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 -> goal_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 = goal_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 of_tactic t gls =
+    try
+      let init = { shelf = []; solution = gls.Evd.sigma ; comb = [gls.Evd.it] } in
+      let (_,final,_,_) = apply (goal_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
+
+(** {7 Notations} *)
+
+module Notations = struct
+  let (>>=) = tclBIND
+  let (<*>) = tclTHEN
+  let (<+>) t1 t2 = tclOR t1 (fun _ -> t2)
+  type ('a, 'b) enter = ('a, 'b) Goal.enter =
+    { enter : 'r. ('a, 'r) Goal.t -> 'b }
+  type ('a, 'b) s_enter = ('a, 'b) Goal.s_enter =
+    { s_enter : 'r. ('a, 'r) Goal.t -> ('b, 'r) Sigma.sigma }
+end
diff --git a/engine/proofview.mli b/engine/proofview.mli
new file mode 100644
index 0000000000..7996b7969c
--- /dev/null
+++ b/engine/proofview.mli
@@ -0,0 +1,589 @@
+(************************************************************************)
+(*  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 -> Pp.std_ppcmds) -> 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] returns the list of unifiable goals if some
+    goals are unifiable (see {!shelve_unifiable}) in the current focus. *)
+val guard_no_unifiable : Names.Name.t list option 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 : Evd.evar_map -> Evar.t -> Evd.evar_map
+
+  (** [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. *)
+  val advance : Evd.evar_map -> Evar.t -> Evar.t option
+
+  val typeclass_resolvable : unit Evd.Store.field
+
+end
+
+(** This module gives access to the innards of the monad. Its use is
+    restricted to very specific cases. *)
+module UnsafeRepr :
+sig
+  type state = Proofview_monad.Logical.Unsafe.state
+  val repr : 'a tactic -> ('a, state, state, iexn) Logic_monad.BackState.t
+  val make : ('a, state, state, iexn) Logic_monad.BackState.t -> 'a tactic
+end
+
+(** {6 Goal-dependent tactics} *)
+
+module Goal : sig
+
+  (** Type of goals.
+
+      The first 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.
+
+      The second parameter is a stage indicating where the goal belongs. See
+      module {!Sigma}.
+  *)
+  type ('a, 'r) t
+
+  (** Assume that you do not need the goal to be normalized. *)
+  val assume : ('a, 'r) t -> ([ `NF ], 'r) t
+
+  (** Normalises the argument goal. *)
+  val normalize : ('a, 'r) t -> ([ `NF ], 'r) 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 ], 'r) t -> Term.constr
+  val hyps : ([ `NF ], 'r) t -> Context.Named.t
+  val env : ('a, 'r) t -> Environ.env
+  val sigma : ('a, 'r) t -> 'r Sigma.t
+  val extra : ('a, 'r) t -> Evd.Store.t
+
+  (** Returns the goal's conclusion even if the goal is not
+      normalised. *)
+  val raw_concl : ('a, 'r) t -> Term.constr
+
+  type ('a, 'b) enter =
+    { enter : 'r. ('a, 'r) t -> 'b }
+
+  (** [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 ], unit tactic) enter -> unit tactic
+
+  (** Like {!nf_enter}, but does not normalize the goal beforehand. *)
+  val enter : ([ `LZ ], unit tactic) enter -> unit tactic
+
+  type ('a, 'b) s_enter =
+    { s_enter : 'r. ('a, 'r) t -> ('b, 'r) Sigma.sigma }
+
+  (** A variant of {!enter} allows to work with a monotonic state. The evarmap
+      returned by the argument is put back into the current state before firing
+      the returned tactic. *)
+  val s_enter : ([ `LZ ], unit tactic) s_enter -> unit tactic
+
+  (** Like {!s_enter}, but normalizes the goal beforehand. *)
+  val nf_s_enter : ([ `NF ], unit tactic) s_enter -> unit tactic
+
+  (** Recover the list of current goals under focus, without evar-normalization.
+      FIXME: encapsulate the level in an existential type. *)
+  val goals : ([ `LZ ], 'r) t tactic list tactic
+
+  (** Compatibility: avoid if possible *)
+  val goal : ([ `NF ], 'r) t -> Evar.t
+
+  (** Every goal is valid at a later stage. FIXME: take a later evarmap *)
+  val lift : ('a, 'r) t -> ('r, 's) Sigma.le -> ('a, 's) t
+
+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
+
+  (* 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
+
+(** {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
+
+  type ('a, 'b) enter = ('a, 'b) Goal.enter =
+    { enter : 'r. ('a, 'r) Goal.t -> 'b }
+  type ('a, 'b) s_enter = ('a, 'b) Goal.s_enter =
+    { s_enter : 'r. ('a, 'r) Goal.t -> ('b, 'r) Sigma.sigma }
+end
diff --git a/engine/proofview_monad.ml b/engine/proofview_monad.ml
index 6e68cd2e45..6f52b3ee90 100644
--- a/engine/proofview_monad.ml
+++ b/engine/proofview_monad.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
@@ -108,11 +108,6 @@ module Info = struct
   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
@@ -157,8 +152,11 @@ 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 }
-
+type proofview = {
+  solution : Evd.evar_map;
+  comb : Evar.t list;
+  shelf : Evar.t list;
+}
 
 (** {6 Instantiation of the logic monad} *)
 
@@ -171,10 +169,10 @@ module P = struct
   type e = bool
 
   (** Status (safe/unsafe) * shelved goals * given up *)
-  type w = bool * Evar.t list * Evar.t list
+  type w = bool * Evar.t list
 
-  let wunit = true , [] , []
-  let wprod (b1,s1,g1) (b2,s2,g2) = b1 && b2 , s1@s2 , g1@g2
+  let wunit = true , []
+  let wprod (b1, g1) (b2, g2) = b1 && b2 , g1@g2
 
   type u = Info.state
 
@@ -226,19 +224,21 @@ module Env : State with type t := Environ.env = struct
 end
 
 module Status : Writer with type t := bool = struct
-  let put s = Logical.put (s,[],[])
+  let put s = Logical.put (s, [])
 end
 
-module Shelf : Writer with type t = Evar.t list = struct
+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 put sh = Logical.put (true,sh,[])
+  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)
+  let put gs = Logical.put (true, gs)
 end
 
 (** Lens and utilies pertaining to the info trace *)
diff --git a/engine/proofview_monad.mli b/engine/proofview_monad.mli
index d2a2e55fb1..0aff0a7207 100644
--- a/engine/proofview_monad.mli
+++ b/engine/proofview_monad.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
@@ -68,15 +68,19 @@ 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 }
+type proofview = {
+  solution : Evd.evar_map;
+  comb : Evar.t list;
+  shelf : Evar.t list;
+}
 
 (** {6 Instantiation of the logic monad} *)
 
 module P : sig
   type s = proofview * Environ.env
 
-  (** Status (safe/unsafe) * shelved goals * given up *)
-  type w = bool * Evar.t list * Evar.t list
+  (** Status (safe/unsafe) * given up *)
+  type w = bool * Evar.t list
 
   val wunit : w
   val wprod : w -> w -> w
@@ -123,7 +127,7 @@ 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 : Writer with type t = Evar.t list
+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. *)
diff --git a/engine/sigma.ml b/engine/sigma.ml
new file mode 100644
index 0000000000..c7b0bb5a50
--- /dev/null
+++ b/engine/sigma.ml
@@ -0,0 +1,117 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+type 'a t = Evd.evar_map
+
+type ('a, 'b) le = unit
+
+let refl = ()
+let cons _ _  = ()
+let (+>) = fun _ _ -> ()
+
+type ('a, 'r) sigma = Sigma : 'a * 's t * ('r, 's) le -> ('a, 'r) sigma
+
+type 'a evar = Evar.t
+
+let lift_evar evk () = evk
+
+let to_evar_map evd = evd
+let to_evar evk = evk
+
+let here x s = Sigma (x, s, ())
+
+(** API *)
+
+type 'r fresh = Fresh : 's evar * 's t * ('r, 's) le -> 'r fresh
+
+let new_evar sigma ?naming info =
+  let (sigma, evk) = Evd.new_evar sigma ?naming info in
+  Fresh (evk, sigma, ())
+
+let define evk c sigma =
+  Sigma ((), Evd.define evk c sigma, ())
+
+let new_univ_level_variable ?loc ?name ?predicative rigid sigma =
+  let (sigma, u) = Evd.new_univ_level_variable ?loc ?name ?predicative rigid sigma in
+  Sigma (u, sigma, ())
+
+let new_univ_variable ?loc ?name ?predicative rigid sigma =
+  let (sigma, u) = Evd.new_univ_variable ?loc ?name ?predicative rigid sigma in
+  Sigma (u, sigma, ())
+
+let new_sort_variable ?loc ?name ?predicative rigid sigma =
+  let (sigma, u) = Evd.new_sort_variable ?loc ?name ?predicative rigid sigma in
+  Sigma (u, sigma, ())
+
+let fresh_sort_in_family ?loc ?rigid env sigma s =
+  let (sigma, s) = Evd.fresh_sort_in_family ?loc ?rigid env sigma s in
+  Sigma (s, sigma, ())
+
+let fresh_constant_instance ?loc env sigma cst =
+  let (sigma, cst) = Evd.fresh_constant_instance ?loc env sigma cst in
+  Sigma (cst, sigma, ())
+
+let fresh_inductive_instance ?loc env sigma ind =
+  let (sigma, ind) = Evd.fresh_inductive_instance ?loc env sigma ind in
+  Sigma (ind, sigma, ())
+
+let fresh_constructor_instance ?loc env sigma pc =
+  let (sigma, c) = Evd.fresh_constructor_instance ?loc env sigma pc in
+  Sigma (c, sigma, ())
+
+let fresh_global ?loc ?rigid ?names env sigma r =
+  let (sigma, c) = Evd.fresh_global ?loc ?rigid ?names env sigma r in
+  Sigma (c, sigma, ())
+
+(** Run *)
+
+type 'a run = { run : 'r. 'r t -> ('a, 'r) sigma }
+
+let run sigma f : 'a * Evd.evar_map =
+  let Sigma (x, sigma, ()) = f.run sigma in
+  (x, sigma)
+
+(** Monotonic references *)
+
+type evdref = Evd.evar_map ref
+
+let apply evdref f =
+  let Sigma (x, sigma, ()) = f.run !evdref in
+  evdref := sigma;
+  x
+
+let purify f =
+  let f (sigma : Evd.evar_map) =
+    let evdref = ref sigma in
+    let ans = f evdref in
+    Sigma (ans, !evdref, ())
+  in
+  { run = f }
+
+(** Unsafe primitives *)
+
+module Unsafe =
+struct
+
+let le = ()
+let of_evar_map sigma = sigma
+let of_evar evk = evk
+let of_ref ref = ref
+let of_pair (x, sigma) = Sigma (x, sigma, ())
+
+end
+
+module Notations =
+struct
+  type ('a, 'r) sigma_ = ('a, 'r) sigma =
+    Sigma : 'a * 's t * ('r, 's) le -> ('a, 'r) sigma_
+
+  let (+>) = fun _ _ -> ()
+
+  type 'a run_ = 'a run = { run : 'r. 'r t -> ('a, 'r) sigma }
+end
diff --git a/engine/sigma.mli b/engine/sigma.mli
new file mode 100644
index 0000000000..643bea4036
--- /dev/null
+++ b/engine/sigma.mli
@@ -0,0 +1,129 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Names
+open Constr
+
+(** Monotonous state enforced by typing.
+
+    This module allows to constrain uses of evarmaps in a monotonous fashion,
+    and in particular statically suppress evar leaks and the like.
+*)
+
+(** {5 Stages} *)
+
+type ('a, 'b) le
+(** Relationship stating that stage ['a] is anterior to stage ['b] *)
+
+val refl : ('a, 'a) le
+(** Reflexivity of anteriority *)
+
+val cons : ('a, 'b) le -> ('b, 'c) le -> ('a, 'c) le
+(** Transitivity of anteriority *)
+
+val (+>) : ('a, 'b) le -> ('b, 'c) le -> ('a, 'c) le
+(** Alias for {!cons} *)
+
+(** {5 Monotonous evarmaps} *)
+
+type 'r t
+(** Stage-indexed evarmaps.  *)
+
+type ('a, 'r) sigma = Sigma : 'a * 's t * ('r, 's) le -> ('a, 'r) sigma
+(** Return values at a later stage *)
+
+type 'r evar
+(** Stage-indexed evars *)
+
+(** {5 Constructors} *)
+
+val here : 'a -> 'r t -> ('a, 'r) sigma
+(** [here x s] is a shorthand for [Sigma (x, s, refl)] *)
+
+(** {5 Postponing} *)
+
+val lift_evar : 'r evar -> ('r, 's) le -> 's evar
+(** Any evar existing at stage ['r] is also valid at any later stage. *)
+
+(** {5 Downcasting} *)
+
+val to_evar_map : 'r t -> Evd.evar_map
+val to_evar : 'r evar -> Evar.t
+
+(** {5 Monotonous API} *)
+
+type 'r fresh = Fresh : 's evar * 's t * ('r, 's) le -> 'r fresh
+
+val new_evar : 'r t -> ?naming:Misctypes.intro_pattern_naming_expr ->
+  Evd.evar_info -> 'r fresh
+
+val define : 'r evar -> Constr.t -> 'r t -> (unit, 'r) sigma
+
+(** Polymorphic universes *)
+
+val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool ->
+  Evd.rigid -> 'r t -> (Univ.universe_level, 'r) sigma
+val new_univ_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool ->
+  Evd.rigid -> 'r t -> (Univ.universe, 'r) sigma
+val new_sort_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool ->
+  Evd.rigid -> 'r t -> (Sorts.t, 'r) sigma
+
+val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:Evd.rigid -> Environ.env ->
+  'r t -> Term.sorts_family -> (Term.sorts, 'r) sigma
+val fresh_constant_instance :
+  ?loc:Loc.t -> Environ.env -> 'r t -> constant -> (pconstant, 'r) sigma
+val fresh_inductive_instance :
+  ?loc:Loc.t -> Environ.env -> 'r t -> inductive -> (pinductive, 'r) sigma
+val fresh_constructor_instance : ?loc:Loc.t -> Environ.env -> 'r t -> constructor ->
+  (pconstructor, 'r) sigma
+
+val fresh_global : ?loc:Loc.t -> ?rigid:Evd.rigid -> ?names:Univ.Instance.t -> Environ.env ->
+  'r t -> Globnames.global_reference -> (constr, 'r) sigma
+
+(** FILLME *)
+
+(** {5 Run} *)
+
+type 'a run = { run : 'r. 'r t -> ('a, 'r) sigma }
+
+val run : Evd.evar_map -> 'a run -> 'a * Evd.evar_map
+
+(** {5 Imperative monotonic functions} *)
+
+type evdref
+(** Monotonic references over evarmaps *)
+
+val apply : evdref -> 'a run -> 'a
+(** Apply a monotonic function on a reference. *)
+
+val purify : (evdref -> 'a) -> 'a run
+(** Converse of {!apply}. *)
+
+(** {5 Unsafe primitives} *)
+
+module Unsafe :
+sig
+  val le : ('a, 'b) le
+  val of_evar_map : Evd.evar_map -> 'r t
+  val of_evar : Evd.evar -> 'r evar
+  val of_ref : Evd.evar_map ref -> evdref
+  val of_pair : ('a * Evd.evar_map) -> ('a, 'r) sigma
+end
+
+(** {5 Notations} *)
+
+module Notations :
+sig
+  type ('a, 'r) sigma_ = ('a, 'r) sigma =
+    Sigma : 'a * 's t * ('r, 's) le -> ('a, 'r) sigma_
+
+  type 'a run_ = 'a run = { run : 'r. 'r t -> ('a, 'r) sigma }
+
+  val (+>) : ('a, 'b) le -> ('b, 'c) le -> ('a, 'c) le
+  (** Alias for {!cons} *)
+end
diff --git a/engine/termops.ml b/engine/termops.ml
index 937471cf76..f698f81513 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
@@ -13,9 +13,11 @@ open Names
 open Nameops
 open Term
 open Vars
-open Context
 open Environ
 
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
+
 (* Sorts and sort family *)
 
 let print_sort = function
@@ -99,26 +101,28 @@ let print_constr_env t = !term_printer t
 let print_constr t = !term_printer (Global.env()) t
 let set_print_constr f = term_printer := f
 
-let pr_var_decl env (id,c,typ) =
-  let pbody = match c with
-    | None ->  (mt ())
-    | Some c ->
+let pr_var_decl env decl =
+  let open NamedDecl in
+  let pbody = match decl with
+    | LocalAssum _ ->  mt ()
+    | LocalDef (_,c,_) ->
 	(* Force evaluation *)
 	let pb = print_constr_env env c in
 	  (str" := " ++ pb ++ cut () ) in
-  let pt = print_constr_env env typ in
+  let pt = print_constr_env env (get_type decl) in
   let ptyp = (str" : " ++ pt) in
-    (pr_id id ++ hov 0 (pbody ++ ptyp))
+    (pr_id (get_id decl) ++ hov 0 (pbody ++ ptyp))
 
-let pr_rel_decl env (na,c,typ) =
-  let pbody = match c with
-    | None -> mt ()
-    | Some c ->
+let pr_rel_decl env decl =
+  let open RelDecl in
+  let pbody = match decl with
+    | LocalAssum _ -> mt ()
+    | LocalDef (_,c,_) ->
 	(* Force evaluation *)
 	let pb = print_constr_env env c in
 	  (str":=" ++ spc () ++ pb ++ spc ()) in
-  let ptyp = print_constr_env env typ in
-    match na with
+  let ptyp = print_constr_env env (get_type decl) in
+    match get_name decl with
       | Anonymous -> hov 0 (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
       | Name id -> hov 0 (pr_id id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
 
@@ -158,55 +162,53 @@ let rel_list n m =
   in
   reln [] 1
 
-(* Same as [rel_list] but takes a context as argument and skips let-ins *)
-let extended_rel_list n hyps =
-  let rec reln l p = function
-    | (_,None,_) :: hyps -> reln (mkRel (n+p) :: l) (p+1) hyps
-    | (_,Some _,_) :: hyps -> reln l (p+1) hyps
-    | [] -> l
-  in
-  reln [] 1 hyps
-
-let extended_rel_vect n hyps = Array.of_list (extended_rel_list n hyps)
-
-
-
-let push_rel_assum (x,t) env = push_rel (x,None,t) env
+let push_rel_assum (x,t) env =
+  let open RelDecl in
+  push_rel (LocalAssum (x,t)) env
 
 let push_rels_assum assums =
-  push_rel_context (List.map (fun (x,t) -> (x,None,t)) assums)
+  let open RelDecl in
+  push_rel_context (List.map (fun (x,t) -> LocalAssum (x,t)) assums)
 
 let push_named_rec_types (lna,typarray,_) env =
+  let open NamedDecl in
   let ctxt =
     Array.map2_i
       (fun i na t ->
 	 match na with
-	   | Name id -> (id, None, lift i t)
+	   | Name id -> LocalAssum (id, lift i t)
 	   | Anonymous -> anomaly (Pp.str "Fix declarations must be named"))
       lna typarray in
   Array.fold_left
     (fun e assum -> push_named assum e) env ctxt
 
 let lookup_rel_id id sign =
+  let open RelDecl in
   let rec lookrec n = function
-    | []                     -> raise Not_found
-    | (Anonymous, _, _) :: l -> lookrec (n + 1) l
-    | (Name id', b, t) :: l  ->
-      if Names.Id.equal id' id then (n, b, t) else lookrec (n + 1) l
+    | [] ->
+        raise Not_found
+    | (LocalAssum (Anonymous, _) | LocalDef (Anonymous,_,_)) :: l ->
+        lookrec (n + 1) l
+    | LocalAssum (Name id', t) :: l  ->
+        if Names.Id.equal id' id then (n,None,t)  else lookrec (n + 1) l
+    | LocalDef (Name id', b, t) :: l  ->
+        if Names.Id.equal id' id then (n,Some b,t) else lookrec (n + 1) l
   in
   lookrec 1 sign
 
 (* Constructs either [forall x:t, c] or [let x:=b:t in c] *)
-let mkProd_or_LetIn (na,body,t) c =
-  match body with
-    | None -> mkProd (na, t, c)
-    | Some b -> mkLetIn (na, b, t, c)
+let mkProd_or_LetIn decl c =
+  let open RelDecl in
+  match decl with
+    | LocalAssum (na,t) -> mkProd (na, t, c)
+    | LocalDef (na,b,t) -> mkLetIn (na, b, t, c)
 
 (* Constructs either [forall x:t, c] or [c] in which [x] is replaced by [b] *)
-let mkProd_wo_LetIn (na,body,t) c =
-  match body with
-    | None -> mkProd (na,  t, c)
-    | Some b -> subst1 b c
+let mkProd_wo_LetIn decl c =
+  let open RelDecl in
+  match decl with
+    | LocalAssum (na,t) -> mkProd (na, t, c)
+    | LocalDef (_,b,_) -> subst1 b c
 
 let it_mkProd init = List.fold_left (fun c (n,t)  -> mkProd (n, t, c)) init
 let it_mkLambda init = List.fold_left (fun c (n,t)  -> mkLambda (n, t, c)) init
@@ -222,10 +224,11 @@ let it_mkNamedProd_wo_LetIn init = it_named_context_quantifier mkNamedProd_wo_Le
 let it_mkNamedLambda_or_LetIn init = it_named_context_quantifier mkNamedLambda_or_LetIn ~init
 
 let it_mkLambda_or_LetIn_from_no_LetIn c decls =
+  let open RelDecl in
   let rec aux k decls c = match decls with
   | [] -> c
-  | (na,Some b,t)::decls -> mkLetIn (na,b,t,aux (k-1) decls (liftn 1 k c))
-  | (na,None,t)::decls -> mkLambda (na,t,aux (k-1) decls c)
+  | LocalDef (na,b,t) :: decls -> mkLetIn (na,b,t,aux (k-1) decls (liftn 1 k c))
+  | LocalAssum (na,t) :: decls -> mkLambda (na,t,aux (k-1) decls c)
   in aux (List.length decls) (List.rev decls) c
 
 (* *)
@@ -316,7 +319,7 @@ let map_constr_with_named_binders g f l c = match kind_of_term c with
    (co-)fixpoint) *)
 
 let fold_rec_types g (lna,typarray,_) e =
-  let ctxt = Array.map2_i (fun i na t -> (na, None, lift i t)) lna typarray in
+  let ctxt = Array.map2_i (fun i na t -> RelDecl.LocalAssum (na, lift i t)) lna typarray in
   Array.fold_left (fun e assum -> g assum e) e ctxt
 
 let map_left2 f a g b =
@@ -331,7 +334,9 @@ let map_left2 f a g b =
     r, s
   end
 
-let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with
+let map_constr_with_binders_left_to_right g f l c =
+  let open RelDecl in
+  match kind_of_term c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _) -> c
   | Cast (b,k,t) -> 
@@ -341,18 +346,18 @@ let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with
       else mkCast (b',k,t')
   | Prod (na,t,b) ->
       let t' = f l t in
-      let b' = f (g (na,None,t) l) b in
+      let b' = f (g (LocalAssum (na,t)) l) b in
 	if t' == t && b' == b then c
 	else mkProd (na, t', b')
   | Lambda (na,t,b) ->
       let t' = f l t in
-      let b' = f (g (na,None,t) l) b in
+      let b' = f (g (LocalAssum (na,t)) l) b in
 	if t' == t && b' == b then c
 	else mkLambda (na, t', b')
   | LetIn (na,bo,t,b) ->
       let bo' = f l bo in
       let t' = f l t in
-      let b' = f (g (na,Some bo,t) l) b in
+      let b' = f (g (LocalDef (na,bo,t)) l) b in
 	if bo' == bo && t' == t && b' == b then c
 	else mkLetIn (na, bo', t', b')	    
   | App (c,[||]) -> assert false
@@ -393,7 +398,9 @@ let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with
 	else mkCoFix (ln,(lna,tl',bl'))
 
 (* strong *)
-let map_constr_with_full_binders g f l cstr = match kind_of_term cstr with
+let map_constr_with_full_binders g f l cstr =
+  let open RelDecl in
+  match kind_of_term cstr with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _) -> cstr
   | Cast (c,k, t) ->
@@ -402,16 +409,16 @@ let map_constr_with_full_binders g f l cstr = match kind_of_term cstr with
       if c==c' && t==t' then cstr else mkCast (c', k, t')
   | Prod (na,t,c) ->
       let t' = f l t in
-      let c' = f (g (na,None,t) l) c in
+      let c' = f (g (LocalAssum (na,t)) l) c in
       if t==t' && c==c' then cstr else mkProd (na, t', c')
   | Lambda (na,t,c) ->
       let t' = f l t in
-      let c' = f (g (na,None,t) l) c in
+      let c' = f (g (LocalAssum (na,t)) l) c in
       if t==t' && c==c' then cstr else  mkLambda (na, t', c')
   | LetIn (na,b,t,c) ->
       let b' = f l b in
       let t' = f l t in
-      let c' = f (g (na,Some b,t) l) c in
+      let c' = f (g (LocalDef (na,b,t)) l) c in
       if b==b' && t==t' && c==c' then cstr else mkLetIn (na, b', t', c')
   | App (c,al) ->
       let c' = f l c in
@@ -432,7 +439,7 @@ let map_constr_with_full_binders g f l cstr = match kind_of_term cstr with
   | Fix (ln,(lna,tl,bl)) ->
       let tl' = Array.map (f l) tl in
       let l' =
-        Array.fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in
+        Array.fold_left2 (fun l na t -> g (LocalAssum (na,t)) l) l lna tl in
       let bl' = Array.map (f l') bl in
       if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl'
       then cstr
@@ -440,7 +447,7 @@ let map_constr_with_full_binders g f l cstr = match kind_of_term cstr with
   | CoFix(ln,(lna,tl,bl)) ->
       let tl' = Array.map (f l) tl in
       let l' =
-        Array.fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in
+        Array.fold_left2 (fun l na t -> g (LocalAssum (na,t)) l) l lna tl in
       let bl' = Array.map (f l') bl in
       if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl'
       then cstr
@@ -453,23 +460,25 @@ let map_constr_with_full_binders g f l cstr = match kind_of_term cstr with
    index) which is processed by [g] (which typically add 1 to [n]) at
    each binder traversal; it is not recursive *)
 
-let fold_constr_with_full_binders g f n acc c = match kind_of_term c with
+let fold_constr_with_full_binders g f n acc c =
+  let open RelDecl in
+  match kind_of_term c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _) -> acc
   | Cast (c,_, t) -> f n (f n acc c) t
-  | Prod (na,t,c) -> f (g (na,None,t) n) (f n acc t) c
-  | Lambda (na,t,c) -> f (g (na,None,t) n) (f n acc t) c
-  | LetIn (na,b,t,c) -> f (g (na,Some b,t) n) (f n (f n acc b) t) c
+  | Prod (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
+  | Lambda (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
+  | LetIn (na,b,t,c) -> f (g (LocalDef (na,b,t)) n) (f n (f n acc b) t) c
   | App (c,l) -> Array.fold_left (f n) (f n acc c) l
   | Proj (p,c) -> f n acc c
   | Evar (_,l) -> Array.fold_left (f n) acc l
   | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
   | Fix (_,(lna,tl,bl)) ->
-      let n' = CArray.fold_left2 (fun c n t -> g (n,None,t) c) n lna tl in
+      let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n,t)) c) n lna tl in
       let fd = Array.map2 (fun t b -> (t,b)) tl bl in
       Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
   | CoFix (_,(lna,tl,bl)) ->
-      let n' = CArray.fold_left2 (fun c n t -> g (n,None,t) c) n lna tl in
+      let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n,t)) c) n lna tl in
       let fd = Array.map2 (fun t b -> (t,b)) tl bl in
       Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
 
@@ -481,23 +490,25 @@ let fold_constr_with_binders g f n acc c =
    each binder traversal; it is not recursive and the order with which
    subterms are processed is not specified *)
 
-let iter_constr_with_full_binders g f l c = match kind_of_term c with
+let iter_constr_with_full_binders g f l c =
+  let open RelDecl in
+  match kind_of_term c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _) -> ()
   | Cast (c,_, t) -> f l c; f l t
-  | Prod (na,t,c) -> f l t; f (g (na,None,t) l) c
-  | Lambda (na,t,c) -> f l t; f (g (na,None,t) l) c
-  | LetIn (na,b,t,c) -> f l b; f l t; f (g (na,Some b,t) l) c
+  | Prod (na,t,c) -> f l t; f (g (LocalAssum (na,t)) l) c
+  | Lambda (na,t,c) -> f l t; f (g (LocalAssum (na,t)) l) c
+  | LetIn (na,b,t,c) -> f l b; f l t; f (g (LocalDef (na,b,t)) l) c
   | App (c,args) -> f l c; Array.iter (f l) args
   | Proj (p,c) -> f l c
   | Evar (_,args) -> Array.iter (f l) args
   | Case (_,p,c,bl) -> f l p; f l c; Array.iter (f l) bl
   | Fix (_,(lna,tl,bl)) ->
-      let l' = Array.fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in
+      let l' = Array.fold_left2 (fun l na t -> g (LocalAssum (na,t)) l) l lna tl in
       Array.iter (f l) tl;
       Array.iter (f l') bl
   | CoFix (_,(lna,tl,bl)) ->
-      let l' = Array.fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in
+      let l' = Array.fold_left2 (fun l na t -> g (LocalAssum (na,t)) l) l lna tl in
       Array.iter (f l) tl;
       Array.iter (f l') bl
 
@@ -545,10 +556,11 @@ let occur_var env id c =
   in
   try occur_rec c; false with Occur -> true
 
-let occur_var_in_decl env hyp (_,c,typ) =
-  match c with
-    | None -> occur_var env hyp typ
-    | Some body ->
+let occur_var_in_decl env hyp decl =
+  let open NamedDecl in
+  match decl with
+    | LocalAssum (_,typ) -> occur_var env hyp typ
+    | LocalDef (_, body, typ) ->
         occur_var env hyp typ ||
         occur_var env hyp body
 
@@ -561,7 +573,7 @@ let free_rels m =
   in
   frec 1 Int.Set.empty m
 
-(* collects all metavar occurences, in left-to-right order, preserving
+(* collects all metavar occurrences, in left-to-right order, preserving
  * repetitions and all. *)
 
 let collect_metas c =
@@ -607,10 +619,11 @@ let dependent_no_evar = dependent_main true false
 let dependent_univs = dependent_main false true
 let dependent_univs_no_evar = dependent_main true true
 
-let dependent_in_decl a (_,c,t) =
-  match c with
-    | None -> dependent a t
-    | Some body -> dependent a body || dependent a t
+let dependent_in_decl a decl =
+  let open NamedDecl in
+  match decl with
+    | LocalAssum (_,t) -> dependent a t
+    | LocalDef (_, body, t) -> dependent a body || dependent a t
 
 let count_occurrences m t =
   let n = ref 0 in
@@ -713,10 +726,10 @@ let replace_term = replace_term_gen eq_constr
 
 let vars_of_env env =
   let s =
-    Context.fold_named_context (fun (id,_,_) s -> Id.Set.add id s)
+    Context.Named.fold_outside (fun decl s -> Id.Set.add (NamedDecl.get_id decl) s)
       (named_context env) ~init:Id.Set.empty in
-  Context.fold_rel_context
-    (fun (na,_,_) s -> match na with Name id -> Id.Set.add id s | _ -> s)
+  Context.Rel.fold_outside
+    (fun decl s -> match RelDecl.get_name decl with Name id -> Id.Set.add id s | _ -> s)
     (rel_context env) ~init:s
 
 let add_vname vars = function
@@ -741,12 +754,12 @@ let lookup_rel_of_name id names =
 let empty_names_context = []
 
 let ids_of_rel_context sign =
-  Context.fold_rel_context
-    (fun (na,_,_) l -> match na with Name id -> id::l | Anonymous -> l)
+  Context.Rel.fold_outside
+    (fun decl l -> match RelDecl.get_name decl with Name id -> id::l | Anonymous -> l)
     sign ~init:[]
 
 let ids_of_named_context sign =
-  Context.fold_named_context (fun (id,_,_) idl -> id::idl) sign ~init:[]
+  Context.Named.fold_outside (fun decl idl -> NamedDecl.get_id decl :: idl) sign ~init:[]
 
 let ids_of_context env =
   (ids_of_rel_context (rel_context env))
@@ -754,7 +767,7 @@ let ids_of_context env =
 
 
 let names_of_rel_context env =
-  List.map (fun (na,_,_) -> na) (rel_context env)
+  List.map RelDecl.get_name (rel_context env)
 
 let is_section_variable id =
   try let _ = Global.lookup_named id in true
@@ -801,7 +814,7 @@ let split_app c = match kind_of_term c with
 	c::(Array.to_list prev), last
   | _ -> assert false
 
-type subst = (rel_context*constr) Evar.Map.t
+type subst = (Context.Rel.t * constr) Evar.Map.t
 
 exception CannotFilter
 
@@ -827,7 +840,7 @@ let filtering env cv_pb c1 c2 =
         end
       | Prod (n,t1,c1), Prod (_,t2,c2) ->
 	  aux env cv_pb t1 t2;
-	  aux ((n,None,t1)::env) cv_pb c1 c2
+	  aux (RelDecl.LocalAssum (n,t1) :: env) cv_pb c1 c2
       | _, Evar (ev,_) -> define cv_pb env ev c1
       | Evar (ev,_), _ -> define cv_pb env ev c2
       | _ ->
@@ -838,15 +851,43 @@ let filtering env cv_pb c1 c2 =
   in
   aux env cv_pb c1 c2; !evm
 
-let decompose_prod_letin : constr -> int * rel_context * constr =
+let decompose_prod_letin : constr -> int * Context.Rel.t * constr =
   let rec prodec_rec i l c = match kind_of_term c with
-    | Prod (n,t,c)    -> prodec_rec (succ i) ((n,None,t)::l) c
-    | LetIn (n,d,t,c) -> prodec_rec (succ i) ((n,Some d,t)::l) c
+    | Prod (n,t,c)    -> prodec_rec (succ i) (RelDecl.LocalAssum (n,t)::l) c
+    | LetIn (n,d,t,c) -> prodec_rec (succ i) (RelDecl.LocalDef (n,d,t)::l) c
     | Cast (c,_,_)    -> prodec_rec i l c
     | _               -> i,l,c in
   prodec_rec 0 []
 
-let align_prod_letin c a : rel_context * constr =
+(* (nb_lam [na1:T1]...[nan:Tan]c) where c is not an abstraction
+ * gives n (casts are ignored) *)
+let nb_lam =
+  let rec nbrec n c = match kind_of_term c with
+    | Lambda (_,_,c) -> nbrec (n+1) c
+    | Cast (c,_,_) -> nbrec n c
+    | _ -> n
+  in
+  nbrec 0
+
+(* similar to nb_lam, but gives the number of products instead *)
+let nb_prod =
+  let rec nbrec n c = match kind_of_term c with
+    | Prod (_,_,c) -> nbrec (n+1) c
+    | Cast (c,_,_) -> nbrec n c
+    | _ -> n
+  in
+  nbrec 0
+
+let nb_prod_modulo_zeta x =
+  let rec count n c =
+    match kind_of_term c with
+        Prod(_,_,t) -> count (n+1) t
+      | LetIn(_,a,_,t) -> count n (subst1 a t)
+      | Cast(c,_,_) -> count n c
+      | _ -> n
+  in count 0 x
+
+let align_prod_letin c a : Context.Rel.t * constr =
   let (lc,_,_) = decompose_prod_letin c in
   let (la,l,a) = decompose_prod_letin a in
   if not (la >= lc) then invalid_arg "align_prod_letin";
@@ -884,20 +925,20 @@ let process_rel_context f env =
   let sign = named_context_val env in
   let rels = rel_context env in
   let env0 = reset_with_named_context sign env in
-  Context.fold_rel_context f rels ~init:env0
+  Context.Rel.fold_outside f rels ~init:env0
 
 let assums_of_rel_context sign =
-  Context.fold_rel_context
-    (fun (na,c,t) l ->
-      match c with
-          Some _ -> l
-        | None -> (na, t)::l)
+  Context.Rel.fold_outside
+    (fun decl l ->
+      match decl with
+      | RelDecl.LocalDef _ -> l
+      | RelDecl.LocalAssum (na,t) -> (na, t)::l)
     sign ~init:[]
 
 let map_rel_context_in_env f env sign =
   let rec aux env acc = function
     | d::sign ->
-	aux (push_rel d env) (map_rel_declaration (f env) d :: acc) sign
+	aux (push_rel d env) (RelDecl.map_constr (f env) d :: acc) sign
     | [] ->
 	acc
   in
@@ -905,10 +946,10 @@ let map_rel_context_in_env f env sign =
 
 let map_rel_context_with_binders f sign =
   let rec aux k = function
-    | d::sign -> map_rel_declaration (f k) d :: aux (k-1) sign
+    | d::sign -> RelDecl.map_constr (f k) d :: aux (k-1) sign
     | [] -> []
   in
-  aux (rel_context_length sign) sign
+  aux (Context.Rel.length sign) sign
 
 let substl_rel_context l =
   map_rel_context_with_binders (fun k -> substnl l (k-1))
@@ -919,60 +960,54 @@ let lift_rel_context n =
 let smash_rel_context sign =
   let rec aux acc = function
   | [] -> acc
-  | (_,None,_ as d) :: l -> aux (d::acc) l
-  | (_,Some b,_) :: l ->
+  | (RelDecl.LocalAssum _ as d) :: l -> aux (d::acc) l
+  | RelDecl.LocalDef (_,b,_) :: l ->
       (* Quadratic in the number of let but there are probably a few of them *)
       aux (List.rev (substl_rel_context [b] (List.rev acc))) l
   in List.rev (aux [] sign)
 
-let adjust_subst_to_rel_context sign l =
-  let rec aux subst sign l =
-    match sign, l with
-    | (_,None,_)::sign', a::args' -> aux (a::subst) sign' args'
-    | (_,Some c,_)::sign', args' ->
-	aux (substl (List.rev subst) c :: subst) sign' args'
-    | [], [] -> List.rev subst
-    | _ -> anomaly (Pp.str "Instance and signature do not match")
-  in aux [] (List.rev sign) l
-
 let fold_named_context_both_sides f l ~init = List.fold_right_and_left f l init
 
-let rec mem_named_context id = function
-  | (id',_,_) :: _ when Id.equal id id' -> true
+let rec mem_named_context id ctxt =
+  match ctxt with
+  | decl :: _ when Id.equal id (NamedDecl.get_id decl) -> true
   | _ :: sign -> mem_named_context id sign
   | [] -> false
 
 let compact_named_context_reverse sign =
-  let compact l (i1,c1,t1) =
+  let compact l decl =
+    let (i1,c1,t1) = NamedDecl.to_tuple decl in
     match l with
     | [] -> [[i1],c1,t1]
     | (l2,c2,t2)::q ->
        if Option.equal Constr.equal c1 c2 && Constr.equal t1 t2
        then (i1::l2,c2,t2)::q
        else ([i1],c1,t1)::l
-  in Context.fold_named_context_reverse compact ~init:[] sign
+  in Context.Named.fold_inside compact ~init:[] sign
 
 let compact_named_context sign = List.rev (compact_named_context_reverse sign)
 
 let clear_named_body id env =
+  let open NamedDecl in
   let aux _ = function
-  | (id',Some c,t) when Id.equal id id' -> push_named (id,None,t)
+  | LocalDef (id',c,t) when Id.equal id id' -> push_named (LocalAssum (id,t))
   | d -> push_named d in
   fold_named_context aux env ~init:(reset_context env)
 
 let global_vars env ids = Id.Set.elements (global_vars_set env ids)
 
 let global_vars_set_of_decl env = function
-  | (_,None,t) -> global_vars_set env t
-  | (_,Some c,t) ->
+  | NamedDecl.LocalAssum (_,t) -> global_vars_set env t
+  | NamedDecl.LocalDef (_,c,t) ->
       Id.Set.union (global_vars_set env t)
         (global_vars_set env c)
 
 let dependency_closure env sign hyps =
   if Id.Set.is_empty hyps then [] else
     let (_,lh) =
-      Context.fold_named_context_reverse
-        (fun (hs,hl) (x,_,_ as d) ->
+      Context.Named.fold_inside
+        (fun (hs,hl) d ->
+          let x = NamedDecl.get_id d in
           if Id.Set.mem x hs then
             (Id.Set.union (global_vars_set_of_decl env d) (Id.Set.remove x hs),
             x::hl)
@@ -987,12 +1022,12 @@ let on_judgment f j = { uj_val = f j.uj_val; uj_type = f j.uj_type }
 let on_judgment_value f j = { j with uj_val = f j.uj_val }
 let on_judgment_type f j = { j with uj_type = f j.uj_type }
 
-(* Cut a context ctx in 2 parts (ctx1,ctx2) with ctx1 containing k
-     variables; skips let-in's *)
+(* Cut a context ctx in 2 parts (ctx1,ctx2) with ctx1 containing k non let-in
+     variables skips let-in's; let-in's in the middle are put in ctx2 *)
 let context_chop k ctx =
   let rec chop_aux acc = function
     | (0, l2) -> (List.rev acc, l2)
-    | (n, ((_,Some _,_ as h)::t)) -> chop_aux (h::acc) (n, t)
+    | (n, (RelDecl.LocalDef _ as h)::t) -> chop_aux (h::acc) (n, t)
     | (n, (h::t)) -> chop_aux (h::acc) (pred n, t)
     | (_, []) -> anomaly (Pp.str "context_chop")
   in chop_aux [] (k,ctx)
diff --git a/engine/termops.mli b/engine/termops.mli
index 6c680005db..c2a4f33235 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
@@ -9,7 +9,6 @@
 open Pp
 open Names
 open Term
-open Context
 open Environ
 
 (** printers *)
@@ -22,7 +21,7 @@ val set_print_constr : (env -> constr -> std_ppcmds) -> unit
 val print_constr     : constr -> std_ppcmds
 val print_constr_env : env -> constr -> std_ppcmds
 val print_named_context : env -> std_ppcmds
-val pr_rel_decl : env -> rel_declaration -> std_ppcmds
+val pr_rel_decl : env -> Context.Rel.Declaration.t -> std_ppcmds
 val print_rel_context : env -> std_ppcmds
 val print_env : env -> std_ppcmds
 
@@ -31,35 +30,31 @@ val push_rel_assum : Name.t * types -> env -> env
 val push_rels_assum : (Name.t * types) list -> env -> env
 val push_named_rec_types : Name.t array * types array * 'a -> env -> env
 
-val lookup_rel_id : Id.t -> rel_context -> int * constr option * types
+val lookup_rel_id : Id.t -> Context.Rel.t -> int * constr option * types
 (** Associates the contents of an identifier in a [rel_context]. Raise
     [Not_found] if there is no such identifier. *)
 
 (** Functions that build argument lists matching a block of binders or a context.
     [rel_vect n m] builds [|Rel (n+m);...;Rel(n+1)|]
-    [extended_rel_vect n ctx] extends the [ctx] context of length [m]
-    with [n] elements.
 *)
 val rel_vect : int -> int -> constr array
 val rel_list : int -> int -> constr list
-val extended_rel_list : int -> rel_context -> constr list
-val extended_rel_vect : int -> rel_context -> constr array
 
 (** iterators/destructors on terms *)
-val mkProd_or_LetIn : rel_declaration -> types -> types
-val mkProd_wo_LetIn : rel_declaration -> types -> types
+val mkProd_or_LetIn : Context.Rel.Declaration.t -> types -> types
+val mkProd_wo_LetIn : Context.Rel.Declaration.t -> types -> types
 val it_mkProd : types -> (Name.t * types) list -> types
 val it_mkLambda : constr -> (Name.t * types) list -> constr
-val it_mkProd_or_LetIn : types -> rel_context -> types
-val it_mkProd_wo_LetIn : types -> rel_context -> types
-val it_mkLambda_or_LetIn : constr -> rel_context -> constr
-val it_mkNamedProd_or_LetIn : types -> named_context -> types
-val it_mkNamedProd_wo_LetIn : types -> named_context -> types
-val it_mkNamedLambda_or_LetIn : constr -> named_context -> constr
+val it_mkProd_or_LetIn : types -> Context.Rel.t -> types
+val it_mkProd_wo_LetIn : types -> Context.Rel.t -> types
+val it_mkLambda_or_LetIn : constr -> Context.Rel.t -> constr
+val it_mkNamedProd_or_LetIn : types -> Context.Named.t -> types
+val it_mkNamedProd_wo_LetIn : types -> Context.Named.t -> types
+val it_mkNamedLambda_or_LetIn : constr -> Context.Named.t -> constr
 
 (* Ad hoc version reinserting letin, assuming the body is defined in
    the context where the letins are expanded *)
-val it_mkLambda_or_LetIn_from_no_LetIn : constr -> rel_context -> constr
+val it_mkLambda_or_LetIn_from_no_LetIn : constr -> Context.Rel.t -> constr
 
 (** {6 Generic iterators on constr} *)
 
@@ -67,11 +62,11 @@ val map_constr_with_named_binders :
   (Name.t -> 'a -> 'a) ->
   ('a -> constr -> constr) -> 'a -> constr -> constr
 val map_constr_with_binders_left_to_right :
-  (rel_declaration -> 'a -> 'a) ->
+  (Context.Rel.Declaration.t -> 'a -> 'a) ->
   ('a -> constr -> constr) ->
     'a -> constr -> constr
 val map_constr_with_full_binders :
-  (rel_declaration -> 'a -> 'a) ->
+  (Context.Rel.Declaration.t -> 'a -> 'a) ->
   ('a -> constr -> constr) -> 'a -> constr -> constr
 
 (** [fold_constr_with_binders g f n acc c] folds [f n] on the immediate
@@ -85,11 +80,11 @@ val fold_constr_with_binders :
   ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b
 
 val fold_constr_with_full_binders :
-  (rel_declaration -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) ->
+  (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) ->
     'a -> 'b -> constr -> 'b
 
 val iter_constr_with_full_binders :
-  (rel_declaration -> 'a -> 'a) -> ('a -> constr -> unit) -> 'a ->
+  (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> constr -> unit) -> 'a ->
     constr -> unit
 
 (**********************************************************************)
@@ -106,7 +101,7 @@ val occur_evar : existential_key -> types -> bool
 val occur_var : env -> Id.t -> types -> bool
 val occur_var_in_decl :
   env ->
-  Id.t -> 'a * types option * types -> bool
+  Id.t -> Context.Named.Declaration.t -> bool
 val free_rels : constr -> Int.Set.t
 
 (** [dependent m t] tests whether [m] is a subterm of [t] *)
@@ -114,7 +109,7 @@ val dependent : constr -> constr -> bool
 val dependent_no_evar : constr -> constr -> bool
 val dependent_univs : constr -> constr -> bool
 val dependent_univs_no_evar : constr -> constr -> bool
-val dependent_in_decl : constr -> named_declaration -> bool
+val dependent_in_decl : constr -> Context.Named.Declaration.t -> bool
 val count_occurrences : constr -> constr -> int
 val collect_metas : constr -> int list
 val collect_vars : constr -> Id.Set.t (** for visible vars only *)
@@ -168,11 +163,21 @@ exception CannotFilter
    (context,term), or raises [CannotFilter].
    Warning: Outer-kernel sort subtyping are taken into account: c1 has
    to be smaller than c2 wrt. sorts. *)
-type subst = (rel_context*constr) Evar.Map.t
-val filtering : rel_context -> Reduction.conv_pb -> constr -> constr -> subst
+type subst = (Context.Rel.t * constr) Evar.Map.t
+val filtering : Context.Rel.t -> Reduction.conv_pb -> constr -> constr -> subst
 
-val decompose_prod_letin : constr -> int * rel_context * constr
-val align_prod_letin : constr -> constr -> rel_context * constr
+val decompose_prod_letin : constr -> int * Context.Rel.t * constr
+val align_prod_letin : constr -> constr -> Context.Rel.t * constr
+
+(** [nb_lam] {% $ %}[x_1:T_1]...[x_n:T_n]c{% $ %} where {% $ %}c{% $ %} is not an abstraction
+   gives {% $ %}n{% $ %} (casts are ignored) *)
+val nb_lam : constr -> int
+
+(** Similar to [nb_lam], but gives the number of products instead *)
+val nb_prod : constr -> int
+
+(** Similar to [nb_prod], but zeta-contracts let-in on the way *)
+val nb_prod_modulo_zeta : constr -> int
 
 (** Get the last arg of a constr intended to be an application *)
 val last_arg : constr -> constr
@@ -191,44 +196,51 @@ val add_name : Name.t -> names_context -> names_context
 val lookup_name_of_rel : int -> names_context -> Name.t
 val lookup_rel_of_name : Id.t -> names_context -> int
 val empty_names_context : names_context
-val ids_of_rel_context : rel_context -> Id.t list
-val ids_of_named_context : named_context -> Id.t list
+val ids_of_rel_context : Context.Rel.t -> Id.t list
+val ids_of_named_context : Context.Named.t -> Id.t list
 val ids_of_context : env -> Id.t list
 val names_of_rel_context : env -> names_context
 
-val context_chop : int -> rel_context -> rel_context * rel_context
-val env_rel_context_chop : int -> env -> env * rel_context
+(* [context_chop n Γ] returns (Γ₁,Γ₂) such that [Γ]=[Γ₂Γ₁], [Γ₁] has
+   [n] hypotheses, excluding local definitions, and [Γ₁], if not empty,
+   starts with an hypothesis (i.e. [Γ₁] has the form empty or [x:A;Γ₁'] *)
+val context_chop : int -> Context.Rel.t -> Context.Rel.t * Context.Rel.t
+
+(* [env_rel_context_chop n env] extracts out the [n] top declarations
+   of the rel_context part of [env], counting both local definitions and
+   hypotheses *)
+val env_rel_context_chop : int -> env -> env * Context.Rel.t
 
 (** Set of local names *)
 val vars_of_env: env -> Id.Set.t
 val add_vname : Id.Set.t -> Name.t -> Id.Set.t
 
 (** other signature iterators *)
-val process_rel_context : (rel_declaration -> env -> env) -> env -> env
-val assums_of_rel_context : rel_context -> (Name.t * constr) list
-val lift_rel_context : int -> rel_context -> rel_context
-val substl_rel_context : constr list -> rel_context -> rel_context
-val smash_rel_context : rel_context -> rel_context (** expand lets in context *)
-val adjust_subst_to_rel_context : rel_context -> constr list -> constr list
+val process_rel_context : (Context.Rel.Declaration.t -> env -> env) -> env -> env
+val assums_of_rel_context : Context.Rel.t -> (Name.t * constr) list
+val lift_rel_context : int -> Context.Rel.t -> Context.Rel.t
+val substl_rel_context : constr list -> Context.Rel.t -> Context.Rel.t
+val smash_rel_context : Context.Rel.t -> Context.Rel.t (** expand lets in context *)
+
 val map_rel_context_in_env :
-  (env -> constr -> constr) -> env -> rel_context -> rel_context
+  (env -> constr -> constr) -> env -> Context.Rel.t -> Context.Rel.t
 val map_rel_context_with_binders :
-  (int -> constr -> constr) -> rel_context -> rel_context
+  (int -> constr -> constr) -> Context.Rel.t -> Context.Rel.t
 val fold_named_context_both_sides :
-  ('a -> named_declaration -> named_declaration list -> 'a) ->
-    named_context -> init:'a -> 'a
-val mem_named_context : Id.t -> named_context -> bool
-val compact_named_context : named_context -> named_list_context
-val compact_named_context_reverse : named_context -> named_list_context
+  ('a -> Context.Named.Declaration.t -> Context.Named.Declaration.t list -> 'a) ->
+    Context.Named.t -> init:'a -> 'a
+val mem_named_context : Id.t -> Context.Named.t -> bool
+val compact_named_context : Context.Named.t -> Context.NamedList.t
+val compact_named_context_reverse : Context.Named.t -> Context.NamedList.t
 
 val clear_named_body : Id.t -> env -> env
 
 val global_vars : env -> constr -> Id.t list
-val global_vars_set_of_decl : env -> named_declaration -> Id.Set.t
+val global_vars_set_of_decl : env -> Context.Named.Declaration.t -> Id.Set.t
 
 (** Gives an ordered list of hypotheses, closed by dependencies,
    containing a given set *)
-val dependency_closure : env -> named_context -> Id.Set.t -> Id.t list
+val dependency_closure : env -> Context.Named.t -> Id.Set.t -> Id.t list
 
 (** Test if an identifier is the basename of a global reference *)
 val is_section_variable : Id.t -> bool
diff --git a/engine/uState.ml b/engine/uState.ml
new file mode 100644
index 0000000000..8aa9a61ab9
--- /dev/null
+++ b/engine/uState.ml
@@ -0,0 +1,491 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Errors
+open Util
+open Names
+
+module StringOrd = struct type t = string let compare = String.compare end
+module UNameMap = struct
+    
+  include Map.Make(StringOrd)
+    
+  let union s t = 
+    if s == t then s
+    else
+      merge (fun k l r -> 
+        match l, r with
+        | Some _, _ -> l
+        | _, _ -> r) s t
+end
+
+type uinfo = {
+  uname : string option;
+  uloc : Loc.t option;
+}
+
+(* 2nd part used to check consistency on the fly. *)
+type t =
+ { uctx_names : Univ.Level.t UNameMap.t * uinfo Univ.LMap.t;
+   uctx_local : Univ.universe_context_set; (** The local context of variables *)
+   uctx_univ_variables : Universes.universe_opt_subst;
+   (** The local universes that are unification variables *)
+   uctx_univ_algebraic : Univ.universe_set; 
+   (** The subset of unification variables that can be instantiated with
+        algebraic universes as they appear in inferred types only. *)
+   uctx_universes : UGraph.t; (** The current graph extended with the local constraints *)
+   uctx_initial_universes : UGraph.t; (** The graph at the creation of the evar_map *)
+ }
+  
+let empty =
+  { uctx_names = UNameMap.empty, Univ.LMap.empty;
+    uctx_local = Univ.ContextSet.empty;
+    uctx_univ_variables = Univ.LMap.empty;
+    uctx_univ_algebraic = Univ.LSet.empty;
+    uctx_universes = UGraph.initial_universes;
+    uctx_initial_universes = UGraph.initial_universes }
+
+let make u =
+    { empty with 
+      uctx_universes = u; uctx_initial_universes = u}
+
+let is_empty ctx =
+  Univ.ContextSet.is_empty ctx.uctx_local && 
+    Univ.LMap.is_empty ctx.uctx_univ_variables
+
+let union ctx ctx' =
+  if ctx == ctx' then ctx
+  else if is_empty ctx' then ctx
+  else
+    let local = Univ.ContextSet.union ctx.uctx_local ctx'.uctx_local in
+    let names = UNameMap.union (fst ctx.uctx_names) (fst ctx'.uctx_names) in
+    let newus = Univ.LSet.diff (Univ.ContextSet.levels ctx'.uctx_local)
+                               (Univ.ContextSet.levels ctx.uctx_local) in
+    let newus = Univ.LSet.diff newus (Univ.LMap.domain ctx.uctx_univ_variables) in
+    let declarenew g =
+      Univ.LSet.fold (fun u g -> UGraph.add_universe u false g) newus g
+    in
+    let names_rev = Univ.LMap.union (snd ctx.uctx_names) (snd ctx'.uctx_names) in
+      { uctx_names = (names, names_rev);
+        uctx_local = local;
+        uctx_univ_variables = 
+          Univ.LMap.subst_union ctx.uctx_univ_variables ctx'.uctx_univ_variables;
+        uctx_univ_algebraic = 
+          Univ.LSet.union ctx.uctx_univ_algebraic ctx'.uctx_univ_algebraic;
+        uctx_initial_universes = declarenew ctx.uctx_initial_universes;
+        uctx_universes = 
+          if local == ctx.uctx_local then ctx.uctx_universes
+          else
+            let cstrsr = Univ.ContextSet.constraints ctx'.uctx_local in
+              UGraph.merge_constraints cstrsr (declarenew ctx.uctx_universes) }
+
+let context_set ctx = ctx.uctx_local
+
+let constraints ctx = snd ctx.uctx_local
+
+let context ctx = Univ.ContextSet.to_context ctx.uctx_local
+
+let of_context_set ctx = { empty with uctx_local = ctx }
+
+let subst ctx = ctx.uctx_univ_variables
+
+let ugraph ctx = ctx.uctx_universes
+
+let algebraics ctx = ctx.uctx_univ_algebraic
+
+let constrain_variables diff ctx =
+  Univ.LSet.fold
+    (fun l cstrs ->
+      try
+        match Univ.LMap.find l ctx.uctx_univ_variables with
+        | Some u -> Univ.Constraint.add (l, Univ.Eq, Option.get (Univ.Universe.level u)) cstrs
+        | None -> cstrs
+      with Not_found | Option.IsNone -> cstrs)
+    diff Univ.Constraint.empty
+
+let add_uctx_names ?loc s l (names, names_rev) =
+  (UNameMap.add s l names, Univ.LMap.add l { uname = Some s; uloc = loc } names_rev)
+
+let add_uctx_loc l loc (names, names_rev) =
+  match loc with
+  | None -> (names, names_rev)
+  | Some _ -> (names, Univ.LMap.add l { uname = None; uloc = loc } names_rev)
+
+let of_binders b =
+  let ctx = empty in
+  let names =
+    List.fold_left (fun acc (id, l) -> add_uctx_names (Id.to_string id) l acc)
+                   ctx.uctx_names b
+  in { ctx with uctx_names = names }
+
+let instantiate_variable l b v =
+  try v := Univ.LMap.update l (Some b) !v
+  with Not_found -> assert false
+
+exception UniversesDiffer
+
+let process_universe_constraints ctx cstrs =
+  let univs = ctx.uctx_universes in
+  let vars = ref ctx.uctx_univ_variables in
+  let normalize = Universes.normalize_universe_opt_subst vars in
+  let rec unify_universes fo l d r local =
+    let l = normalize l and r = normalize r in
+      if Univ.Universe.equal l r then local
+      else 
+        let varinfo x = 
+          match Univ.Universe.level x with
+          | None -> Inl x
+          | Some l -> Inr (l, Univ.LMap.mem l !vars, Univ.LSet.mem l ctx.uctx_univ_algebraic)
+        in
+          if d == Universes.ULe then
+            if UGraph.check_leq univs l r then
+              (** Keep Prop/Set <= var around if var might be instantiated by prop or set
+                  later. *)
+              if Univ.Universe.is_level l then 
+                match Univ.Universe.level r with
+                | Some r ->
+                  Univ.Constraint.add (Option.get (Univ.Universe.level l),Univ.Le,r) local
+                | _ -> local
+              else local
+            else
+              match Univ.Universe.level r with
+              | None -> error ("Algebraic universe on the right")
+              | Some rl ->
+                if Univ.Level.is_small rl then
+                  let levels = Univ.Universe.levels l in
+                    Univ.LSet.fold (fun l local ->
+                      if Univ.Level.is_small l || Univ.LMap.mem l !vars then
+                        unify_universes fo (Univ.Universe.make l) Universes.UEq r local
+                      else raise (Univ.UniverseInconsistency (Univ.Le, Univ.Universe.make l, r, None)))
+                      levels local
+                else
+                  Univ.enforce_leq l r local
+          else if d == Universes.ULub then
+            match varinfo l, varinfo r with
+            | (Inr (l, true, _), Inr (r, _, _)) 
+            | (Inr (r, _, _), Inr (l, true, _)) -> 
+              instantiate_variable l (Univ.Universe.make r) vars; 
+              Univ.enforce_eq_level l r local
+            | Inr (_, _, _), Inr (_, _, _) ->
+              unify_universes true l Universes.UEq r local
+            | _, _ -> assert false
+          else (* d = Universes.UEq *)
+            match varinfo l, varinfo r with
+            | Inr (l', lloc, _), Inr (r', rloc, _) ->
+              let () = 
+                if lloc then
+                  instantiate_variable l' r vars
+                else if rloc then 
+                  instantiate_variable r' l vars
+                else if not (UGraph.check_eq univs l r) then
+                  (* Two rigid/global levels, none of them being local,
+                     one of them being Prop/Set, disallow *)
+                  if Univ.Level.is_small l' || Univ.Level.is_small r' then
+                    raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None))
+                  else
+                    if fo then 
+                      raise UniversesDiffer
+              in
+                Univ.enforce_eq_level l' r' local
+            | Inr (l, loc, alg), Inl r
+            | Inl r, Inr (l, loc, alg) ->
+               let inst = Univ.univ_level_rem l r r in
+                 if alg then (instantiate_variable l inst vars; local)
+                 else
+                   let lu = Univ.Universe.make l in
+                   if Univ.univ_level_mem l r then
+                     Univ.enforce_leq inst lu local
+                   else raise (Univ.UniverseInconsistency (Univ.Eq, lu, r, None))
+            | _, _ (* One of the two is algebraic or global *) -> 
+             if UGraph.check_eq univs l r then local
+             else raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None))
+  in
+  let local = 
+    Universes.Constraints.fold (fun (l,d,r) local -> unify_universes false l d r local)
+      cstrs Univ.Constraint.empty
+  in
+    !vars, local
+
+let add_constraints ctx cstrs =
+  let univs, local = ctx.uctx_local in
+  let cstrs' = Univ.Constraint.fold (fun (l,d,r) acc -> 
+    let l = Univ.Universe.make l and r = Univ.Universe.make r in
+    let cstr' = 
+      if d == Univ.Lt then (Univ.Universe.super l, Universes.ULe, r)
+      else (l, (if d == Univ.Le then Universes.ULe else Universes.UEq), r)
+    in Universes.Constraints.add cstr' acc)
+    cstrs Universes.Constraints.empty
+  in
+  let vars, local' = process_universe_constraints ctx cstrs' in
+    { ctx with uctx_local = (univs, Univ.Constraint.union local local');
+      uctx_univ_variables = vars;
+      uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes }
+
+(* let addconstrkey = Profile.declare_profile "add_constraints_context";; *)
+(* let add_constraints_context = Profile.profile2 addconstrkey add_constraints_context;; *)
+
+let add_universe_constraints ctx cstrs =
+  let univs, local = ctx.uctx_local in
+  let vars, local' = process_universe_constraints ctx cstrs in
+    { ctx with uctx_local = (univs, Univ.Constraint.union local local');
+      uctx_univ_variables = vars;
+      uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes }
+
+let pr_uctx_level uctx = 
+  let map, map_rev = uctx.uctx_names in 
+    fun l ->
+      try str (Option.get (Univ.LMap.find l map_rev).uname)
+      with Not_found | Option.IsNone ->
+        Universes.pr_with_global_universes l
+
+let universe_context ?names ctx =
+  match names with
+  | None -> [], Univ.ContextSet.to_context ctx.uctx_local
+  | Some pl ->
+     let levels = Univ.ContextSet.levels ctx.uctx_local in
+     let newinst, map, left =
+       List.fold_right
+         (fun (loc,id) (newinst, map, acc) ->
+          let l =
+            try UNameMap.find (Id.to_string id) (fst ctx.uctx_names)
+            with Not_found ->
+              user_err_loc (loc, "universe_context",
+                            str"Universe " ++ Nameops.pr_id id ++ str" is not bound anymore.")
+          in (l :: newinst, (id, l) :: map, Univ.LSet.remove l acc))
+         pl ([], [], levels)
+     in
+       if not (Univ.LSet.is_empty left) then
+         let n = Univ.LSet.cardinal left in
+         let loc =
+          let get_loc u = try (Univ.LMap.find u (snd ctx.uctx_names)).uloc with Not_found -> None in
+          try List.find_map get_loc (Univ.LSet.elements left) with Not_found -> Loc.ghost
+         in
+           user_err_loc (loc, "universe_context",
+                        (str(CString.plural n "Universe") ++ spc () ++
+                             Univ.LSet.pr (pr_uctx_level ctx) left ++
+                             spc () ++ str (CString.conjugate_verb_to_be n) ++ str" unbound."))
+      else
+        let inst = Univ.Instance.of_array (Array.of_list newinst) in
+        let ctx = Univ.UContext.make (inst,
+          Univ.ContextSet.constraints ctx.uctx_local)
+        in map, ctx
+
+let restrict ctx vars =
+  let uctx' = Universes.restrict_universe_context ctx.uctx_local vars in
+  { ctx with uctx_local = uctx' }
+
+type rigid = 
+  | UnivRigid
+  | UnivFlexible of bool (** Is substitution by an algebraic ok? *)
+
+let univ_rigid = UnivRigid
+let univ_flexible = UnivFlexible false
+let univ_flexible_alg = UnivFlexible true
+
+let merge ?loc sideff rigid uctx ctx' =
+  let open Univ in
+  let levels = ContextSet.levels ctx' in
+  let uctx = if sideff then uctx else
+    match rigid with
+    | UnivRigid -> uctx
+    | UnivFlexible b ->
+      let fold u accu =
+        if LMap.mem u accu then accu
+        else LMap.add u None accu
+      in
+      let uvars' = LSet.fold fold levels uctx.uctx_univ_variables in
+        if b then
+          { uctx with uctx_univ_variables = uvars';
+          uctx_univ_algebraic = LSet.union uctx.uctx_univ_algebraic levels }
+        else { uctx with uctx_univ_variables = uvars' }
+  in
+  let uctx_local =
+    if sideff then uctx.uctx_local
+    else ContextSet.append ctx' uctx.uctx_local
+  in
+  let declare g =
+    LSet.fold (fun u g ->
+               try UGraph.add_universe u false g
+               with UGraph.AlreadyDeclared when sideff -> g)
+              levels g
+  in
+  let uctx_names =
+    let fold u accu =
+      let modify _ info = match info.uloc with
+      | None -> { info with uloc = loc }
+      | Some _ -> info
+      in
+      try LMap.modify u modify accu
+      with Not_found -> LMap.add u { uname = None; uloc = loc } accu
+    in
+    (fst uctx.uctx_names, LSet.fold fold levels (snd uctx.uctx_names))
+  in
+  let initial = declare uctx.uctx_initial_universes in
+  let univs = declare uctx.uctx_universes in
+  let uctx_universes = UGraph.merge_constraints (ContextSet.constraints ctx') univs in
+    { uctx with uctx_names; uctx_local; uctx_universes; uctx_initial_universes = initial }
+
+let merge_subst uctx s =
+  { uctx with uctx_univ_variables = Univ.LMap.subst_union uctx.uctx_univ_variables s }
+
+let emit_side_effects eff u =
+  let uctxs = Safe_typing.universes_of_private eff in
+  List.fold_left (merge true univ_rigid) u uctxs
+
+let new_univ_variable ?loc rigid name
+  ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) =
+  let u = Universes.new_univ_level (Global.current_dirpath ()) in
+  let ctx' = Univ.ContextSet.add_universe u ctx in
+  let uctx', pred =
+    match rigid with
+    | UnivRigid -> uctx, true
+    | UnivFlexible b -> 
+      let uvars' = Univ.LMap.add u None uvars in
+        if b then {uctx with uctx_univ_variables = uvars';
+          uctx_univ_algebraic = Univ.LSet.add u avars}, false
+        else {uctx with uctx_univ_variables = uvars'}, false
+  in
+  let names = 
+    match name with
+    | Some n -> add_uctx_names ?loc n u uctx.uctx_names
+    | None -> add_uctx_loc u loc uctx.uctx_names
+  in
+  let initial =
+    UGraph.add_universe u false uctx.uctx_initial_universes
+  in                                                 
+  let uctx' =
+    {uctx' with uctx_names = names; uctx_local = ctx';
+                uctx_universes = UGraph.add_universe u false uctx.uctx_universes;
+                uctx_initial_universes = initial}
+  in uctx', u
+
+let add_global_univ uctx u =
+  let initial =
+    UGraph.add_universe u true uctx.uctx_initial_universes
+  in
+  let univs = 
+    UGraph.add_universe u true uctx.uctx_universes
+  in
+  { uctx with uctx_local = Univ.ContextSet.add_universe u uctx.uctx_local;
+                                     uctx_initial_universes = initial;
+                                     uctx_universes = univs }
+
+let make_flexible_variable ctx b u =
+  let {uctx_univ_variables = uvars; uctx_univ_algebraic = avars} = ctx in
+  let uvars' = Univ.LMap.add u None uvars in
+  let avars' = 
+    if b then
+      let uu = Univ.Universe.make u in
+      let substu_not_alg u' v =
+        Option.cata (fun vu -> Univ.Universe.equal uu vu && not (Univ.LSet.mem u' avars)) false v
+      in
+        if not (Univ.LMap.exists substu_not_alg uvars)
+        then Univ.LSet.add u avars else avars 
+    else avars 
+  in
+  {ctx with uctx_univ_variables = uvars'; 
+      uctx_univ_algebraic = avars'}
+
+let is_sort_variable uctx s = 
+  match s with 
+  | Sorts.Type u -> 
+    (match Univ.universe_level u with
+    | Some l as x -> 
+        if Univ.LSet.mem l (Univ.ContextSet.levels uctx.uctx_local) then x
+        else None
+    | None -> None)
+  | _ -> None
+
+let subst_univs_context_with_def def usubst (ctx, cst) =
+  (Univ.LSet.diff ctx def, Univ.subst_univs_constraints usubst cst)
+
+let normalize_variables uctx =
+  let normalized_variables, undef, def, subst = 
+    Universes.normalize_univ_variables uctx.uctx_univ_variables 
+  in
+  let ctx_local = subst_univs_context_with_def def (Univ.make_subst subst) uctx.uctx_local in
+  let ctx_local', univs = Universes.refresh_constraints uctx.uctx_initial_universes ctx_local in
+    subst, { uctx with uctx_local = ctx_local';
+      uctx_univ_variables = normalized_variables;
+      uctx_universes = univs }
+
+let abstract_undefined_variables uctx =
+  let vars' = 
+    Univ.LMap.fold (fun u v acc ->
+      if v == None then Univ.LSet.remove u acc
+      else acc)
+    uctx.uctx_univ_variables uctx.uctx_univ_algebraic
+  in { uctx with uctx_local = Univ.ContextSet.empty;
+      uctx_univ_algebraic = vars' }
+
+let fix_undefined_variables uctx =
+  let algs', vars' = 
+    Univ.LMap.fold (fun u v (algs, vars as acc) ->
+      if v == None then (Univ.LSet.remove u algs, Univ.LMap.remove u vars)
+      else acc)
+      uctx.uctx_univ_variables 
+      (uctx.uctx_univ_algebraic, uctx.uctx_univ_variables)
+  in
+  { uctx with uctx_univ_variables = vars';
+    uctx_univ_algebraic = algs' }
+
+let refresh_undefined_univ_variables uctx =
+  let subst, ctx' = Universes.fresh_universe_context_set_instance uctx.uctx_local in
+  let alg = Univ.LSet.fold (fun u acc -> Univ.LSet.add (Univ.subst_univs_level_level subst u) acc) 
+    uctx.uctx_univ_algebraic Univ.LSet.empty 
+  in
+  let vars = 
+    Univ.LMap.fold
+      (fun u v acc ->
+        Univ.LMap.add (Univ.subst_univs_level_level subst u) 
+          (Option.map (Univ.subst_univs_level_universe subst) v) acc)
+      uctx.uctx_univ_variables Univ.LMap.empty
+  in
+  let declare g = Univ.LSet.fold (fun u g -> UGraph.add_universe u false g)
+                                   (Univ.ContextSet.levels ctx') g in
+  let initial = declare uctx.uctx_initial_universes in
+  let univs = declare UGraph.initial_universes in
+  let uctx' = {uctx_names = uctx.uctx_names;
+               uctx_local = ctx'; 
+               uctx_univ_variables = vars; uctx_univ_algebraic = alg;
+               uctx_universes = univs;
+               uctx_initial_universes = initial } in
+    uctx', subst
+
+let normalize uctx = 
+  let ((vars',algs'), us') = 
+    Universes.normalize_context_set uctx.uctx_local uctx.uctx_univ_variables
+				    uctx.uctx_univ_algebraic
+  in
+  if Univ.ContextSet.equal us' uctx.uctx_local then uctx
+  else
+    let us', universes =
+      Universes.refresh_constraints uctx.uctx_initial_universes us'
+    in
+      { uctx_names = uctx.uctx_names;
+        uctx_local = us'; 
+        uctx_univ_variables = vars'; 
+        uctx_univ_algebraic = algs';
+        uctx_universes = universes;
+        uctx_initial_universes = uctx.uctx_initial_universes }
+
+let universe_of_name uctx s = 
+  UNameMap.find s (fst uctx.uctx_names)
+
+let add_universe_name uctx s l =
+  let names' = add_uctx_names s l uctx.uctx_names in
+  { uctx with uctx_names = names' }
+
+let update_sigma_env uctx env =
+  let univs = Environ.universes env in
+  let eunivs =
+    { uctx with uctx_initial_universes = univs;
+                         uctx_universes = univs }
+  in
+  merge true univ_rigid eunivs eunivs.uctx_local
diff --git a/engine/uState.mli b/engine/uState.mli
new file mode 100644
index 0000000000..c5c454020c
--- /dev/null
+++ b/engine/uState.mli
@@ -0,0 +1,117 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Universe unification states *)
+
+open Names
+
+exception UniversesDiffer
+
+type t
+(** Type of universe unification states. They allow the incremental building of
+    universe constraints during an interactive proof. *)
+
+(** {5 Constructors} *)
+
+val empty : t
+
+val make : UGraph.t -> t
+
+val is_empty : t -> bool
+
+val union : t -> t -> t
+
+val of_context_set : Univ.universe_context_set -> t
+
+val of_binders : Universes.universe_binders -> t
+
+(** {5 Projections} *)
+
+val context_set : t -> Univ.universe_context_set
+(** The local context of the state, i.e. a set of bound variables together
+    with their associated constraints. *)
+
+val subst : t -> Universes.universe_opt_subst
+(** The local universes that are unification variables *)
+
+val ugraph : t -> UGraph.t
+(** The current graph extended with the local constraints *)
+
+val algebraics : t -> Univ.LSet.t
+(** The subset of unification variables that can be instantiated with algebraic
+    universes as they appear in inferred types only. *)
+
+val constraints : t -> Univ.constraints
+(** Shorthand for {!context_set} composed with {!ContextSet.constraints}. *)
+
+val context : t -> Univ.universe_context
+(** Shorthand for {!context_set} with {!Context_set.to_context}. *)
+
+(** {5 Constraints handling} *)
+
+val add_constraints : t -> Univ.constraints -> t
+(**
+  @raise UniversesDiffer when universes differ
+*)
+
+val add_universe_constraints : t -> Universes.universe_constraints -> t
+(**
+  @raise UniversesDiffer when universes differ
+*)
+
+(** {5 Names} *)
+
+val add_universe_name : t -> string -> Univ.Level.t -> t
+(** Associate a human-readable name to a local variable. *)
+
+val universe_of_name : t -> string -> Univ.Level.t
+(** Retrieve the universe associated to the name. *)
+
+(** {5 Unification} *)
+
+val restrict : t -> Univ.universe_set -> t
+
+type rigid = 
+  | UnivRigid
+  | UnivFlexible of bool (** Is substitution by an algebraic ok? *)
+
+val univ_rigid : rigid
+val univ_flexible : rigid
+val univ_flexible_alg : rigid
+
+val merge : ?loc:Loc.t -> bool -> rigid -> t -> Univ.universe_context_set -> t
+val merge_subst : t -> Universes.universe_opt_subst -> t
+val emit_side_effects : Safe_typing.private_constants -> t -> t
+
+val new_univ_variable : ?loc:Loc.t -> rigid -> string option -> t -> t * Univ.Level.t
+val add_global_univ : t -> Univ.Level.t -> t
+val make_flexible_variable : t -> bool -> Univ.Level.t -> t
+
+val is_sort_variable : t -> Sorts.t -> Univ.Level.t option
+
+val normalize_variables : t -> Univ.universe_subst * t
+
+val constrain_variables : Univ.LSet.t -> t -> Univ.constraints
+
+val abstract_undefined_variables : t -> t
+
+val fix_undefined_variables : t -> t
+
+val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst
+
+val normalize : t -> t
+
+(** {5 TODO: Document me} *)
+
+val universe_context : ?names:(Id.t Loc.located) list -> t -> (Id.t * Univ.Level.t) list * Univ.universe_context
+
+val update_sigma_env : t -> Environ.env -> t
+
+(** {5 Pretty-printing} *)
+
+val pr_uctx_level : t -> Univ.Level.t -> Pp.std_ppcmds