[declare] [obligations] Refactor preparation of obligation entry

Preparation of obligation/program entries requires low-level
manipulation that does break the abstraction over `proof_entry`; we
thus introduce `prepare_obligation`, and move the code that prepares
the obligation entry to its own module.

This seems to improve separation of concerns, and helps clarify the
two of three current models in which Coq operates w.r.t. definitions:

- single, ground entries with possibly mutual definitions [regular lemmas]
- single, non-ground entries with possibly mutual definitions [obligations]
- multiple entries [equations]

12 files changed, 396 insertions, 327 deletions

diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
index 2fdca15552..3b906324f4 100644
--- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml
+++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
@@ -1,5 +1,5 @@
 let edeclare ?hook ~name ~poly ~scope ~kind ~opaque ~udecl ~impargs sigma body tyopt  =
-  let sigma, ce = DeclareDef.prepare_definition ~allow_evars:false
+  let sigma, ce = DeclareDef.prepare_definition
       ~opaque ~poly sigma ~udecl ~types:tyopt ~body in
   let uctx = Evd.evar_universe_context sigma in
   let ubind = Evd.universe_binders sigma in
diff --git a/vernac/classes.ml b/vernac/classes.ml
index dafd1cc5e4..e0bf9e777c 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -315,7 +315,7 @@ let instance_hook info global imps ?hook cst =
 let declare_instance_constant info global imps ?hook name udecl poly sigma term termtype =
   let kind = Decls.(IsDefinition Instance) in
   let sigma, entry = DeclareDef.prepare_definition
-      ~allow_evars:false ~poly sigma ~udecl ~types:(Some termtype) ~body:term in
+      ~poly sigma ~udecl ~types:(Some termtype) ~body:term in
   let kn = Declare.declare_constant ~name ~kind (Declare.DefinitionEntry entry) in
   Declare.definition_message name;
   DeclareUniv.declare_univ_binders (GlobRef.ConstRef kn) (Evd.universe_binders sigma);
@@ -343,7 +343,7 @@ let declare_instance_program env sigma ~global ~poly name pri imps udecl term te
     let sigma = Evd.from_env env in
     declare_instance env sigma (Some pri) (not global) (GlobRef.ConstRef cst)
   in
-  let obls, _, term, typ = Obligations.eterm_obligations env name sigma 0 term termtype in
+  let obls, _, term, typ = RetrieveObl.retrieve_obligations env name sigma 0 term termtype in
   let hook = DeclareDef.Hook.make hook in
   let uctx = Evd.evar_universe_context sigma in
   let scope, kind = DeclareDef.Global Declare.ImportDefaultBehavior, Decls.Instance in
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index c1be95fa67..eb70ad0ac0 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -68,49 +68,35 @@ let interp_definition ~program_mode pl bl ~poly red_option c ctypopt =
   (* Declare the definition *)
   let c = EConstr.it_mkLambda_or_LetIn c ctx in
   let tyopt = Option.map (fun ty -> EConstr.it_mkProd_or_LetIn ty ctx) tyopt in
+  (c, tyopt), evd, udecl, imps
 
-  let evd, ce = DeclareDef.prepare_definition ~allow_evars:program_mode
-      ~opaque:false ~poly evd ~udecl ~types:tyopt ~body:c in
-
-  (ce, evd, udecl, imps)
-
-let check_definition ~program_mode (ce, evd, _, imps) =
+let check_definition ~program_mode (ce, evd) =
   let env = Global.env () in
   check_evars_are_solved ~program_mode env evd;
   ce
 
 let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
   let program_mode = false in
-  let (ce, evd, udecl, impargs as def) =
+  let (body, types), evd, udecl, impargs =
     interp_definition ~program_mode udecl bl ~poly red_option c ctypopt
   in
-  let ce = check_definition ~program_mode def in
+  let evd, ce = DeclareDef.prepare_definition ~opaque:false ~poly evd ~udecl ~types ~body in
+  let ce = check_definition ~program_mode (ce, evd) in
   let uctx = Evd.evar_universe_context evd in
   let hook_data = Option.map (fun hook -> hook, uctx, []) hook in
   let kind = Decls.IsDefinition kind in
   let ubind = Evd.universe_binders evd in
   let _ : Names.GlobRef.t =
-    DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ~ubind ce ~impargs
+    DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce
   in ()
 
 let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
   let program_mode = true in
-  let (ce, evd, udecl, impargs as def) =
+  let (body, types), evd, udecl, impargs =
     interp_definition ~program_mode udecl bl ~poly red_option c ctypopt
   in
-  let env = Global.env () in
-  let (c,ctx), sideff = Future.force ce.Declare.proof_entry_body in
-  assert(Safe_typing.empty_private_constants = sideff.Evd.seff_private);
-  assert(Univ.ContextSet.is_empty ctx);
-  Obligations.check_evars env evd;
-  let c = EConstr.of_constr c in
-  let typ = match ce.Declare.proof_entry_type with
-    | Some t -> EConstr.of_constr t
-    | None -> Retyping.get_type_of env evd c
-  in
-  let obls, _, c, cty = Obligations.eterm_obligations env name evd 0 c typ in
-  let uctx = Evd.evar_universe_context evd in
+  let term, ty, uctx, obls = DeclareDef.prepare_obligation ~name ~poly ~body ~types ~udecl evd in
   let _ : DeclareObl.progress =
     Obligations.add_definition
-      ~name ~term:c cty ~uctx ~udecl ~impargs ~scope ~poly ~kind ?hook obls
+      ~name ~term ty ~uctx ~udecl ~impargs ~scope ~poly ~kind ?hook obls
   in ()
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index 7902b0ef09..337da22018 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -39,19 +39,3 @@ val do_definition_program
   -> constr_expr
   -> constr_expr option
   -> unit
-
-(************************************************************************)
-(** Internal API  *)
-(************************************************************************)
-
-(** Not used anywhere. *)
-val interp_definition
-  :  program_mode:bool
-  -> universe_decl_expr option
-  -> local_binder_expr list
-  -> poly:bool
-  -> red_expr option
-  -> constr_expr
-  -> constr_expr option
-  -> Evd.side_effects Declare.proof_entry *
-     Evd.evar_map * UState.universe_decl * Impargs.manual_implicits
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 3bac0419ef..f20b294499 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -254,9 +254,9 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
   in
   (* XXX: Capturing sigma here... bad bad *)
   let hook = DeclareDef.Hook.make (hook sigma) in
-  Obligations.check_evars env sigma;
+  RetrieveObl.check_evars env sigma;
   let evars, _, evars_def, evars_typ =
-    Obligations.eterm_obligations env recname sigma 0 def typ
+    RetrieveObl.retrieve_obligations env recname sigma 0 def typ
   in
   let uctx = Evd.evar_universe_context sigma in
   ignore(Obligations.add_definition ~name:recname ~term:evars_def ~udecl
@@ -287,7 +287,7 @@ let do_program_recursive ~scope ~poly fixkind fixl =
     let typ = nf_evar evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign) in
     let evm = collect_evars_of_term evd def typ in
     let evars, _, def, typ =
-      Obligations.eterm_obligations env id evm
+      RetrieveObl.retrieve_obligations env id evm
         (List.length rec_sign) def typ in
     (id, def, typ, imps, evars)
   in
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index b0c8fe90c4..f283f700b7 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -157,7 +157,8 @@ let check_definition_evars ~allow_evars sigma =
   let env = Global.env () in
   if not allow_evars then Pretyping.check_evars_are_solved ~program_mode:false env sigma
 
-let prepare_definition ~allow_evars ?opaque ?inline ~poly ~udecl ~types ~body sigma =
+let prepare_definition ?opaque ?inline ~poly ~udecl ~types ~body sigma =
+  let allow_evars = false in
   check_definition_evars ~allow_evars sigma;
   let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:(not allow_evars)
       sigma (fun nf -> nf body, Option.map nf types)
@@ -165,6 +166,28 @@ let prepare_definition ~allow_evars ?opaque ?inline ~poly ~udecl ~types ~body si
   let univs = Evd.check_univ_decl ~poly sigma udecl in
   sigma, definition_entry ?opaque ?inline ?types ~univs body
 
+let prepare_obligation ?opaque ?inline ~name ~poly ~udecl ~types ~body sigma =
+  let allow_evars = true in
+  check_definition_evars ~allow_evars sigma;
+  let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:(not allow_evars)
+      sigma (fun nf -> nf body, Option.map nf types)
+  in
+  let univs = Evd.check_univ_decl ~poly sigma udecl in
+  let ce = definition_entry ?opaque ?inline ?types ~univs body in
+  let env = Global.env () in
+  let (c,ctx), sideff = Future.force ce.Declare.proof_entry_body in
+  assert(Safe_typing.empty_private_constants = sideff.Evd.seff_private);
+  assert(Univ.ContextSet.is_empty ctx);
+  RetrieveObl.check_evars env sigma;
+  let c = EConstr.of_constr c in
+  let typ = match ce.Declare.proof_entry_type with
+    | Some t -> EConstr.of_constr t
+    | None -> Retyping.get_type_of env sigma c
+  in
+  let obls, _, c, cty = RetrieveObl.retrieve_obligations env name sigma 0 c typ in
+  let uctx = Evd.evar_universe_context sigma in
+  c, cty, uctx, obls
+
 let prepare_parameter ~allow_evars ~poly ~udecl ~types sigma =
   check_definition_evars ~allow_evars sigma;
   let sigma, typ = Evarutil.finalize ~abort_on_undefined_evars:(not allow_evars)
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index e999027b44..27d9460382 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -89,8 +89,7 @@ val declare_mutually_recursive
   -> Names.GlobRef.t list
 
 val prepare_definition
-  :  allow_evars:bool
-  -> ?opaque:bool
+  :  ?opaque:bool
   -> ?inline:bool
   -> poly:bool
   -> udecl:UState.universe_decl
@@ -99,6 +98,17 @@ val prepare_definition
   -> Evd.evar_map
   -> Evd.evar_map * Evd.side_effects Declare.proof_entry
 
+val prepare_obligation
+  :  ?opaque:bool
+  -> ?inline:bool
+  -> name:Id.t
+  -> poly:bool
+  -> udecl:UState.universe_decl
+  -> types:EConstr.t option
+  -> body:EConstr.t
+  -> Evd.evar_map
+  -> Constr.constr * Constr.types * UState.t * RetrieveObl.obligation_info
+
 val prepare_parameter
   : allow_evars:bool
   -> poly:bool
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index a29ba44907..0ffcea3867 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -10,252 +10,16 @@
 
 open Printf
 
-(**
-   - Get types of existentials ;
-   - Flatten dependency tree (prefix order) ;
-   - Replace existentials by de Bruijn indices in term, applied to the right arguments ;
-   - Apply term prefixed by quantification on "existentials".
-*)
-
-open Constr
 open Names
 open Pp
 open CErrors
 open Util
 
-module NamedDecl = Context.Named.Declaration
-
 (* For the records fields, opens should go away one these types are private *)
 open DeclareObl
 open DeclareObl.Obligation
 open DeclareObl.ProgramDecl
 
-let succfix (depth, fixrels) =
-  (succ depth, List.map succ fixrels)
-
-let check_evars env evm =
-  Evar.Map.iter
-    (fun key evi ->
-       if Evd.is_obligation_evar evm key then ()
-       else
-         let (loc,k) = Evd.evar_source key evm in
-         Pretype_errors.error_unsolvable_implicit ?loc env evm key None)
-  (Evd.undefined_map evm)
-
-type oblinfo =
-  { ev_name: int * Id.t;
-    ev_hyps: EConstr.named_context;
-    ev_status: bool * Evar_kinds.obligation_definition_status;
-    ev_chop: int option;
-    ev_src: Evar_kinds.t Loc.located;
-    ev_typ: types;
-    ev_tac: unit Proofview.tactic option;
-    ev_deps: Int.Set.t }
-
-(** Substitute evar references in t using de Bruijn indices,
-  where n binders were passed through. *)
-
-let subst_evar_constr evm evs n idf t =
-  let seen = ref Int.Set.empty in
-  let transparent = ref Id.Set.empty in
-  let evar_info id = List.assoc_f Evar.equal id evs in
-  let rec substrec (depth, fixrels) c = match EConstr.kind evm c with
-    | Evar (k, args) ->
-        let { ev_name = (id, idstr) ;
-              ev_hyps = hyps ; ev_chop = chop } =
-          try evar_info k
-          with Not_found ->
-            anomaly ~label:"eterm" (Pp.str "existential variable " ++ int (Evar.repr k) ++ str " not found.")
-        in
-        seen := Int.Set.add id !seen;
-          (* Evar arguments are created in inverse order,
-             and we must not apply to defined ones (i.e. LetIn's)
-          *)
-        let args =
-          let n = match chop with None -> 0 | Some c -> c in
-          let (l, r) = List.chop n (List.rev (Array.to_list args)) in
-            List.rev r
-        in
-        let args =
-          let rec aux hyps args acc =
-             let open Context.Named.Declaration in
-             match hyps, args with
-                 (LocalAssum _ :: tlh), (c :: tla) ->
-                   aux tlh tla ((substrec (depth, fixrels) c) :: acc)
-               | (LocalDef _ :: tlh), (_ :: tla) ->
-                   aux tlh tla acc
-               | [], [] -> acc
-               | _, _ -> acc (*failwith "subst_evars: invalid argument"*)
-          in aux hyps args []
-        in
-          if List.exists
-            (fun x -> match EConstr.kind evm x with
-            | Rel n -> Int.List.mem n fixrels
-            | _ -> false) args
-          then
-            transparent := Id.Set.add idstr !transparent;
-          EConstr.mkApp (idf idstr, Array.of_list args)
-    | Fix _ ->
-        EConstr.map_with_binders evm succfix substrec (depth, 1 :: fixrels) c
-    | _ -> EConstr.map_with_binders evm succfix substrec (depth, fixrels) c
-  in
-  let t' = substrec (0, []) t in
-    EConstr.to_constr evm t', !seen, !transparent
-
-
-(** Substitute variable references in t using de Bruijn indices,
-  where n binders were passed through. *)
-let subst_vars acc n t =
-  let var_index id = Util.List.index Id.equal id acc in
-  let rec substrec depth c = match Constr.kind c with
-    | Var v -> (try mkRel (depth + (var_index v)) with Not_found -> c)
-    | _ -> Constr.map_with_binders succ substrec depth c
-  in
-    substrec 0 t
-
-(** Rewrite type of an evar ([ H1 : t1, ... Hn : tn |- concl ])
-    to a product : forall H1 : t1, ..., forall Hn : tn, concl.
-    Changes evars and hypothesis references to variable references.
-*)
-let etype_of_evar evm evs hyps concl =
-  let open Context.Named.Declaration in
-  let rec aux acc n = function
-      decl :: tl ->
-        let t', s, trans = subst_evar_constr evm evs n EConstr.mkVar (NamedDecl.get_type decl) in
-        let t'' = subst_vars acc 0 t' in
-        let rest, s', trans' = aux (NamedDecl.get_id decl :: acc) (succ n) tl in
-        let s' = Int.Set.union s s' in
-        let trans' = Id.Set.union trans trans' in
-          (match decl with
-            | LocalDef (id,c,_) ->
-                let c', s'', trans'' = subst_evar_constr evm evs n EConstr.mkVar c in
-                let c' = subst_vars acc 0 c' in
-                Term.mkNamedProd_or_LetIn (LocalDef (id, c', t'')) rest,
-                Int.Set.union s'' s',
-                Id.Set.union trans'' trans'
-            | LocalAssum (id,_) ->
-              Term.mkNamedProd_or_LetIn (LocalAssum (id, t'')) rest, s', trans')
-    | [] ->
-      let t', s, trans = subst_evar_constr evm evs n EConstr.mkVar concl in
-      subst_vars acc 0 t', s, trans
-  in aux [] 0 (List.rev hyps)
-
-let trunc_named_context n ctx =
-  let len = List.length ctx in
-    List.firstn (len - n) ctx
-
-let rec chop_product n t =
-  let pop t = Vars.lift (-1) t in
-  if Int.equal n 0 then Some t
-  else
-    match Constr.kind t with
-      | Prod (_, _, b) ->  if Vars.noccurn 1 b then chop_product (pred n) (pop b) else None
-      | _ -> None
-
-let evar_dependencies evm oev =
-  let one_step deps =
-    Evar.Set.fold (fun ev s ->
-      let evi = Evd.find evm ev in
-      let deps' = Evd.evars_of_filtered_evar_info evm evi in
-      if Evar.Set.mem oev deps' then
-        invalid_arg ("Ill-formed evar map: cycle detected for evar " ^ Pp.string_of_ppcmds @@ Evar.print oev)
-      else Evar.Set.union deps' s)
-      deps deps
-  in
-  let rec aux deps =
-    let deps' = one_step deps in
-      if Evar.Set.equal deps deps' then deps
-      else aux deps'
-  in aux (Evar.Set.singleton oev)
-
-let move_after (id, ev, deps as obl) l =
-  let rec aux restdeps = function
-    | (id', _, _) as obl' :: tl ->
-        let restdeps' = Evar.Set.remove id' restdeps in
-          if Evar.Set.is_empty restdeps' then
-            obl' :: obl :: tl
-          else obl' :: aux restdeps' tl
-    | [] -> [obl]
-  in aux (Evar.Set.remove id deps) l
-
-let sort_dependencies evl =
-  let rec aux l found list =
-    match l with
-    | (id, ev, deps) as obl :: tl ->
-        let found' = Evar.Set.union found (Evar.Set.singleton id) in
-          if Evar.Set.subset deps found' then
-            aux tl found' (obl :: list)
-          else aux (move_after obl tl) found list
-    | [] -> List.rev list
-  in aux evl Evar.Set.empty []
-
-let eterm_obligations env name evm fs ?status t ty =
-  (* 'Serialize' the evars *)
-  let nc = Environ.named_context env in
-  let nc_len = Context.Named.length nc in
-  let evm = Evarutil.nf_evar_map_undefined evm in
-  let evl = Evarutil.non_instantiated evm in
-  let evl = Evar.Map.bindings evl in
-  let evl = List.map (fun (id, ev) -> (id, ev, evar_dependencies evm id)) evl in
-  let sevl = sort_dependencies evl in
-  let evl = List.map (fun (id, ev, _) -> id, ev) sevl in
-  let evn =
-    let i = ref (-1) in
-      List.rev_map (fun (id, ev) -> incr i;
-                      (id, (!i, Id.of_string
-                              (Id.to_string name ^ "_obligation_" ^ string_of_int (succ !i))),
-                       ev)) evl
-  in
-  let evts =
-    (* Remove existential variables in types and build the corresponding products *)
-    List.fold_right
-      (fun (id, (n, nstr), ev) l ->
-         let hyps = Evd.evar_filtered_context ev in
-         let hyps = trunc_named_context nc_len hyps in
-         let evtyp, deps, transp = etype_of_evar evm l hyps ev.Evd.evar_concl in
-         let evtyp, hyps, chop =
-           match chop_product fs evtyp with
-           | Some t -> t, trunc_named_context fs hyps, fs
-           | None -> evtyp, hyps, 0
-         in
-         let loc, k = Evd.evar_source id evm in
-         let status = match k with
-           | Evar_kinds.QuestionMark { Evar_kinds.qm_obligation=o } -> o
-           | _ -> match status with
-                 | Some o -> o
-                 | None -> Evar_kinds.Define (not (Program.get_proofs_transparency ()))
-         in
-         let force_status, status, chop = match status with
-           | Evar_kinds.Define true as stat ->
-              if not (Int.equal chop fs) then true, Evar_kinds.Define false, None
-              else false, stat, Some chop
-           | s -> false, s, None
-         in
-         let info = { ev_name = (n, nstr);
-                      ev_hyps = hyps; ev_status = force_status, status; ev_chop = chop;
-                      ev_src = loc, k; ev_typ = evtyp ; ev_deps = deps; ev_tac = None }
-         in (id, info) :: l)
-      evn []
-  in
-  let t', _, transparent = (* Substitute evar refs in the term by variables *)
-    subst_evar_constr evm evts 0 EConstr.mkVar t
-  in
-  let ty, _, _ = subst_evar_constr evm evts 0 EConstr.mkVar ty in
-  let evars =
-    List.map (fun (ev, info) ->
-      let { ev_name = (_, name); ev_status = force_status, status;
-            ev_src = src; ev_typ = typ; ev_deps = deps; ev_tac = tac } = info
-      in
-      let force_status, status = match status with
-        | Evar_kinds.Define true when Id.Set.mem name transparent ->
-          true, Evar_kinds.Define false
-        | _ -> force_status, status
-      in name, typ, src, (force_status, status), deps, tac) evts
-  in
-  let evnames = List.map (fun (ev, info) -> ev, snd info.ev_name) evts in
-  let evmap f c = pi1 (subst_evar_constr evm evts 0 f c) in
-    Array.of_list (List.rev evars), (evnames, evmap), t', ty
-
 let pperror cmd = CErrors.user_err ~hdr:"Program" cmd
 let error s = pperror (str s)
 
@@ -270,11 +34,6 @@ let explain_no_obligations = function
     Some ident -> str "No obligations for program " ++ Id.print ident
   | None -> str "No obligations remaining"
 
-type obligation_info =
-    (Names.Id.t * types * Evar_kinds.t Loc.located *
-       (bool * Evar_kinds.obligation_definition_status)
-       * Int.Set.t * unit Proofview.tactic option) array
-
 let assumption_message = Declare.assumption_message
 
 let default_tactic = ref (Proofview.tclUNIT ())
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 101958072a..280b9a0c50 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -8,43 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Environ
 open Constr
-open Evd
-open Names
-
-val check_evars : env -> evar_map -> unit
-
-val evar_dependencies : evar_map -> Evar.t -> Evar.Set.t
-val sort_dependencies : (Evar.t * evar_info * Evar.Set.t) list -> (Evar.t * evar_info * Evar.Set.t) list
-
-(* ident, type, location, (opaque or transparent, expand or define), dependencies, tactic to solve it *)
-type obligation_info =
-  (Id.t * types * Evar_kinds.t Loc.located *
-   (bool * Evar_kinds.obligation_definition_status) * Int.Set.t * unit Proofview.tactic option) array
-
-(* env, id, evars, number of function prototypes to try to clear from
-   evars contexts, object and type *)
-val eterm_obligations
-  :  env
-  -> Id.t
-  -> evar_map
-  -> int
-  -> ?status:Evar_kinds.obligation_definition_status
-  -> EConstr.constr
-  -> EConstr.types
-  -> obligation_info *
-
-     (* Existential key, obl. name, type as product, location of the
-        original evar, associated tactic, status and dependencies as
-        indexes into the array *)
-     ((Evar.t * Id.t) list * ((Id.t -> EConstr.constr) -> EConstr.constr -> constr)) *
-
-     (* Translations from existential identifiers to obligation
-        identifiers and for terms with existentials to closed terms,
-        given a translation from obligation identifiers to constrs,
-        new term, new type *)
-     constr * types
 
 val default_tactic : unit Proofview.tactic ref
 
@@ -61,12 +25,12 @@ val add_definition
   -> ?reduce:(constr -> constr)
   -> ?hook:DeclareDef.Hook.t
   -> ?opaque:bool
-  -> obligation_info
+  -> RetrieveObl.obligation_info
   -> DeclareObl.progress
 
 val add_mutual_definitions
   (* XXX: unify with MutualEntry *)
-  : (Names.Id.t * constr * types * Impargs.manual_implicits * obligation_info) list
+  : (Names.Id.t * constr * types * Impargs.manual_implicits * RetrieveObl.obligation_info) list
   -> uctx:UState.t
   -> ?udecl:UState.universe_decl
   (** Universe binders and constraints *)
diff --git a/vernac/retrieveObl.ml b/vernac/retrieveObl.ml
new file mode 100644
index 0000000000..c529972b8d
--- /dev/null
+++ b/vernac/retrieveObl.ml
@@ -0,0 +1,296 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Names
+
+(**
+   - Get types of existentials ;
+   - Flatten dependency tree (prefix order) ;
+   - Replace existentials by de Bruijn indices in term, applied to the right arguments ;
+   - Apply term prefixed by quantification on "existentials".
+*)
+
+let check_evars env evm =
+  Evar.Map.iter
+    (fun key evi ->
+      if Evd.is_obligation_evar evm key then ()
+      else
+        let loc, k = Evd.evar_source key evm in
+        Pretype_errors.error_unsolvable_implicit ?loc env evm key None)
+    (Evd.undefined_map evm)
+
+type obligation_info =
+  ( Names.Id.t
+  * Constr.types
+  * Evar_kinds.t Loc.located
+  * (bool * Evar_kinds.obligation_definition_status)
+  * Int.Set.t
+  * unit Proofview.tactic option )
+  array
+
+type oblinfo =
+  { ev_name : int * Id.t
+  ; ev_hyps : EConstr.named_context
+  ; ev_status : bool * Evar_kinds.obligation_definition_status
+  ; ev_chop : int option
+  ; ev_src : Evar_kinds.t Loc.located
+  ; ev_typ : Constr.types
+  ; ev_tac : unit Proofview.tactic option
+  ; ev_deps : Int.Set.t }
+
+(** Substitute evar references in t using de Bruijn indices,
+  where n binders were passed through. *)
+
+let succfix (depth, fixrels) = (succ depth, List.map succ fixrels)
+
+let subst_evar_constr evm evs n idf t =
+  let seen = ref Int.Set.empty in
+  let transparent = ref Id.Set.empty in
+  let evar_info id = CList.assoc_f Evar.equal id evs in
+  let rec substrec (depth, fixrels) c =
+    match EConstr.kind evm c with
+    | Constr.Evar (k, args) ->
+      let {ev_name = id, idstr; ev_hyps = hyps; ev_chop = chop} =
+        try evar_info k
+        with Not_found ->
+          CErrors.anomaly ~label:"eterm"
+            Pp.(
+              str "existential variable "
+              ++ int (Evar.repr k)
+              ++ str " not found.")
+      in
+      seen := Int.Set.add id !seen;
+      (* Evar arguments are created in inverse order,
+         and we must not apply to defined ones (i.e. LetIn's)
+      *)
+      let args =
+        let n = match chop with None -> 0 | Some c -> c in
+        let l, r = CList.chop n (List.rev (Array.to_list args)) in
+        List.rev r
+      in
+      let args =
+        let rec aux hyps args acc =
+          let open Context.Named.Declaration in
+          match (hyps, args) with
+          | LocalAssum _ :: tlh, c :: tla ->
+            aux tlh tla (substrec (depth, fixrels) c :: acc)
+          | LocalDef _ :: tlh, _ :: tla -> aux tlh tla acc
+          | [], [] -> acc
+          | _, _ -> acc
+          (*failwith "subst_evars: invalid argument"*)
+        in
+        aux hyps args []
+      in
+      if
+        List.exists
+          (fun x ->
+            match EConstr.kind evm x with
+            | Constr.Rel n -> Int.List.mem n fixrels
+            | _ -> false)
+          args
+      then transparent := Id.Set.add idstr !transparent;
+      EConstr.mkApp (idf idstr, Array.of_list args)
+    | Constr.Fix _ ->
+      EConstr.map_with_binders evm succfix substrec (depth, 1 :: fixrels) c
+    | _ -> EConstr.map_with_binders evm succfix substrec (depth, fixrels) c
+  in
+  let t' = substrec (0, []) t in
+  (EConstr.to_constr evm t', !seen, !transparent)
+
+(** Substitute variable references in t using de Bruijn indices,
+  where n binders were passed through. *)
+let subst_vars acc n t =
+  let var_index id = Util.List.index Id.equal id acc in
+  let rec substrec depth c =
+    match Constr.kind c with
+    | Constr.Var v -> (
+      try Constr.mkRel (depth + var_index v) with Not_found -> c )
+    | _ -> Constr.map_with_binders succ substrec depth c
+  in
+  substrec 0 t
+
+(** Rewrite type of an evar ([ H1 : t1, ... Hn : tn |- concl ])
+    to a product : forall H1 : t1, ..., forall Hn : tn, concl.
+    Changes evars and hypothesis references to variable references.
+*)
+let etype_of_evar evm evs hyps concl =
+  let open Context.Named.Declaration in
+  let rec aux acc n = function
+    | decl :: tl -> (
+      let t', s, trans =
+        subst_evar_constr evm evs n EConstr.mkVar
+          (Context.Named.Declaration.get_type decl)
+      in
+      let t'' = subst_vars acc 0 t' in
+      let rest, s', trans' =
+        aux (Context.Named.Declaration.get_id decl :: acc) (succ n) tl
+      in
+      let s' = Int.Set.union s s' in
+      let trans' = Id.Set.union trans trans' in
+      match decl with
+      | LocalDef (id, c, _) ->
+        let c', s'', trans'' = subst_evar_constr evm evs n EConstr.mkVar c in
+        let c' = subst_vars acc 0 c' in
+        ( Term.mkNamedProd_or_LetIn (LocalDef (id, c', t'')) rest
+        , Int.Set.union s'' s'
+        , Id.Set.union trans'' trans' )
+      | LocalAssum (id, _) ->
+        (Term.mkNamedProd_or_LetIn (LocalAssum (id, t'')) rest, s', trans') )
+    | [] ->
+      let t', s, trans = subst_evar_constr evm evs n EConstr.mkVar concl in
+      (subst_vars acc 0 t', s, trans)
+  in
+  aux [] 0 (List.rev hyps)
+
+let trunc_named_context n ctx =
+  let len = List.length ctx in
+  CList.firstn (len - n) ctx
+
+let rec chop_product n t =
+  let pop t = Vars.lift (-1) t in
+  if Int.equal n 0 then Some t
+  else
+    match Constr.kind t with
+    | Constr.Prod (_, _, b) ->
+      if Vars.noccurn 1 b then chop_product (pred n) (pop b) else None
+    | _ -> None
+
+let evar_dependencies evm oev =
+  let one_step deps =
+    Evar.Set.fold
+      (fun ev s ->
+        let evi = Evd.find evm ev in
+        let deps' = Evd.evars_of_filtered_evar_info evm evi in
+        if Evar.Set.mem oev deps' then
+          invalid_arg
+            ( "Ill-formed evar map: cycle detected for evar "
+            ^ Pp.string_of_ppcmds @@ Evar.print oev )
+        else Evar.Set.union deps' s)
+      deps deps
+  in
+  let rec aux deps =
+    let deps' = one_step deps in
+    if Evar.Set.equal deps deps' then deps else aux deps'
+  in
+  aux (Evar.Set.singleton oev)
+
+let move_after ((id, ev, deps) as obl) l =
+  let rec aux restdeps = function
+    | ((id', _, _) as obl') :: tl ->
+      let restdeps' = Evar.Set.remove id' restdeps in
+      if Evar.Set.is_empty restdeps' then obl' :: obl :: tl
+      else obl' :: aux restdeps' tl
+    | [] -> [obl]
+  in
+  aux (Evar.Set.remove id deps) l
+
+let sort_dependencies evl =
+  let rec aux l found list =
+    match l with
+    | ((id, ev, deps) as obl) :: tl ->
+      let found' = Evar.Set.union found (Evar.Set.singleton id) in
+      if Evar.Set.subset deps found' then aux tl found' (obl :: list)
+      else aux (move_after obl tl) found list
+    | [] -> List.rev list
+  in
+  aux evl Evar.Set.empty []
+
+let retrieve_obligations env name evm fs ?status t ty =
+  (* 'Serialize' the evars *)
+  let nc = Environ.named_context env in
+  let nc_len = Context.Named.length nc in
+  let evm = Evarutil.nf_evar_map_undefined evm in
+  let evl = Evarutil.non_instantiated evm in
+  let evl = Evar.Map.bindings evl in
+  let evl = List.map (fun (id, ev) -> (id, ev, evar_dependencies evm id)) evl in
+  let sevl = sort_dependencies evl in
+  let evl = List.map (fun (id, ev, _) -> (id, ev)) sevl in
+  let evn =
+    let i = ref (-1) in
+    List.rev_map
+      (fun (id, ev) ->
+        incr i;
+        ( id
+        , ( !i
+          , Id.of_string
+              (Id.to_string name ^ "_obligation_" ^ string_of_int (succ !i)) )
+        , ev ))
+      evl
+  in
+  let evts =
+    (* Remove existential variables in types and build the corresponding products *)
+    List.fold_right
+      (fun (id, (n, nstr), ev) l ->
+        let hyps = Evd.evar_filtered_context ev in
+        let hyps = trunc_named_context nc_len hyps in
+        let evtyp, deps, transp = etype_of_evar evm l hyps ev.Evd.evar_concl in
+        let evtyp, hyps, chop =
+          match chop_product fs evtyp with
+          | Some t -> (t, trunc_named_context fs hyps, fs)
+          | None -> (evtyp, hyps, 0)
+        in
+        let loc, k = Evd.evar_source id evm in
+        let status =
+          match k with
+          | Evar_kinds.QuestionMark {Evar_kinds.qm_obligation = o} -> o
+          | _ -> (
+            match status with
+            | Some o -> o
+            | None ->
+              Evar_kinds.Define (not (Program.get_proofs_transparency ())) )
+        in
+        let force_status, status, chop =
+          match status with
+          | Evar_kinds.Define true as stat ->
+            if not (Int.equal chop fs) then (true, Evar_kinds.Define false, None)
+            else (false, stat, Some chop)
+          | s -> (false, s, None)
+        in
+        let info =
+          { ev_name = (n, nstr)
+          ; ev_hyps = hyps
+          ; ev_status = (force_status, status)
+          ; ev_chop = chop
+          ; ev_src = (loc, k)
+          ; ev_typ = evtyp
+          ; ev_deps = deps
+          ; ev_tac = None }
+        in
+        (id, info) :: l)
+      evn []
+  in
+  let t', _, transparent =
+    (* Substitute evar refs in the term by variables *)
+    subst_evar_constr evm evts 0 EConstr.mkVar t
+  in
+  let ty, _, _ = subst_evar_constr evm evts 0 EConstr.mkVar ty in
+  let evars =
+    List.map
+      (fun (ev, info) ->
+        let { ev_name = _, name
+            ; ev_status = force_status, status
+            ; ev_src = src
+            ; ev_typ = typ
+            ; ev_deps = deps
+            ; ev_tac = tac } =
+          info
+        in
+        let force_status, status =
+          match status with
+          | Evar_kinds.Define true when Id.Set.mem name transparent ->
+            (true, Evar_kinds.Define false)
+          | _ -> (force_status, status)
+        in
+        (name, typ, src, (force_status, status), deps, tac))
+      evts
+  in
+  let evnames = List.map (fun (ev, info) -> (ev, snd info.ev_name)) evts in
+  let evmap f c = Util.pi1 (subst_evar_constr evm evts 0 f c) in
+  (Array.of_list (List.rev evars), (evnames, evmap), t', ty)
diff --git a/vernac/retrieveObl.mli b/vernac/retrieveObl.mli
new file mode 100644
index 0000000000..c9c45bd889
--- /dev/null
+++ b/vernac/retrieveObl.mli
@@ -0,0 +1,46 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+val check_evars : Environ.env -> Evd.evar_map -> unit
+
+type obligation_info =
+  ( Names.Id.t
+  * Constr.types
+  * Evar_kinds.t Loc.located
+  * (bool * Evar_kinds.obligation_definition_status)
+  * Int.Set.t
+  * unit Proofview.tactic option )
+  array
+(** ident, type, location of the original evar, (opaque or
+   transparent, expand or define), dependencies as indexes into the
+   array, tactic to solve it *)
+
+val retrieve_obligations :
+     Environ.env
+  -> Names.Id.t
+  -> Evd.evar_map
+  -> int
+  -> ?status:Evar_kinds.obligation_definition_status
+  -> EConstr.t
+  -> EConstr.types
+  -> obligation_info
+     * ( (Evar.t * Names.Id.t) list
+       * ((Names.Id.t -> EConstr.t) -> EConstr.t -> Constr.t) )
+     * Constr.t
+     * Constr.t
+(** [retrieve_obligations env id sigma fs ?status body type] returns
+   [obls, (evnames, evmap), nbody, ntype] a list of obligations built
+   from evars in [body, type].
+
+    [fs] is the number of function prototypes to try to clear from
+   evars contexts. [evnames, evmap) is the list of names /
+   substitution functions used to program with holes. This is not used
+   in Coq, but in the equations plugin; [evnames] is actually
+   redundant with the information contained in [obls] *)
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index 6e398d87ca..5a2bdb43d4 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -14,6 +14,7 @@ Proof_using
 Egramcoq
 Metasyntax
 DeclareUniv
+RetrieveObl
 DeclareDef
 DeclareObl
 Canonical