Imported Upstream version 8.8.2upstream/8.8.2

1 files changed, 0 insertions, 1171 deletions

diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
deleted file mode 100644
index 29d74573..00000000
--- a/toplevel/obligations.ml
+++ /dev/null
@@ -1,1171 +0,0 @@
-open Printf
-open Globnames
-open Libobject
-open Entries
-open Decl_kinds
-open Declare
-
-(**
-   - 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 Term
-open Vars
-open Names
-open Evd
-open Pp
-open CErrors
-open Util
-
-let declare_fix_ref = ref (fun ?opaque _ _ _ _ _ _ -> assert false)
-let declare_definition_ref = ref (fun _ _ _ _ _ -> assert false)
-
-let succfix (depth, fixrels) =
-  (succ depth, List.map succ fixrels)
-
-let check_evars env evm =
-  Evar.Map.iter
-  (fun key evi ->
-   let (loc,k) = evar_source key evm in
-     match k with
-     | Evar_kinds.QuestionMark _
-     | Evar_kinds.ImplicitArg (_,_,false) -> ()
-     | _ ->
-       Pretype_errors.error_unsolvable_implicit loc env evm key None)
-  (Evd.undefined_map evm)
-
-type oblinfo =
-  { ev_name: int * Id.t;
-    ev_hyps: Context.Named.t;
-    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 evs n idf t =
-  let open Context.Named.Declaration in
-  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 kind_of_term 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 =
-	     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 kind_of_term x with
-            | Rel n -> Int.List.mem n fixrels
-            | _ -> false) args
-          then
-	    transparent := Id.Set.add idstr !transparent;
-	  mkApp (idf idstr, Array.of_list args)
-    | Fix _ ->
-	map_constr_with_binders succfix substrec (depth, 1 :: fixrels) c
-    | _ -> map_constr_with_binders succfix substrec (depth, fixrels) c
-  in
-  let t' = substrec (0, []) t in
-    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 kind_of_term c with
-    | Var v -> (try mkRel (depth + (var_index v)) with Not_found -> c)
-    | _ -> map_constr_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 evs hyps concl =
-  let open Context.Named.Declaration in
-  let rec aux acc n = function
-      decl :: tl ->
-	let t', s, trans = subst_evar_constr evs n mkVar (get_type decl) in
-	let t'' = subst_vars acc 0 t' in
-	let rest, s', trans' = aux (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 evs n mkVar c in
-		let c' = subst_vars acc 0 c' in
-		  mkNamedProd_or_LetIn (LocalDef (id, c', t'')) rest,
-		Int.Set.union s'' s',
-		Id.Set.union trans'' trans'
-	    | LocalAssum (id,_) ->
-		mkNamedProd_or_LetIn (LocalAssum (id, t'')) rest, s', trans')
-    | [] ->
-	let t', s, trans = subst_evar_constr evs n 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 =
-  if Int.equal n 0 then Some t
-  else
-    match kind_of_term t with
-      | Prod (_, _, b) ->  if noccurn 1 b then chop_product (pred n) (Termops.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' = evars_of_filtered_evar_info evi in
-      if Evar.Set.mem oev deps' then
-	invalid_arg ("Ill-formed evar map: cycle detected for evar " ^ string_of_existential 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 []
-
-open Environ
-
-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 l hyps ev.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 = evar_source id evm in
-	 let status = match k with
-           | Evar_kinds.QuestionMark 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 evts 0 mkVar t 
-  in
-  let ty, _, _ = subst_evar_constr evts 0 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 evts 0 f c) in
-    Array.of_list (List.rev evars), (evnames, evmap), t', ty
-
-let tactics_module = ["Program";"Tactics"]
-let safe_init_constant md name () =
-  Coqlib.check_required_library ("Coq"::md);
-  Coqlib.gen_constant "Obligations" md name
-let hide_obligation = safe_init_constant tactics_module "obligation"
-
-let pperror cmd = CErrors.errorlabstrm "Program" cmd
-let error s = pperror (str s)
-
-let reduce c =
-  Reductionops.clos_norm_flags CClosure.betaiota (Global.env ()) Evd.empty c
-
-exception NoObligations of Id.t option
-
-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 * Term.types * Evar_kinds.t Loc.located *
-       (bool * Evar_kinds.obligation_definition_status)
-       * Int.Set.t * unit Proofview.tactic option) array
-
-type 'a obligation_body = 
-  | DefinedObl of 'a
-  | TermObl of constr
-
-type obligation =
-  { obl_name : Id.t;
-    obl_type : types;
-    obl_location : Evar_kinds.t Loc.located;
-    obl_body : constant obligation_body option;
-    obl_status : bool * Evar_kinds.obligation_definition_status;
-    obl_deps : Int.Set.t;
-    obl_tac : unit Proofview.tactic option;
-  }
-
-type obligations = (obligation array * int)
-
-type fixpoint_kind =
-  | IsFixpoint of (Id.t Loc.located option * Constrexpr.recursion_order_expr) list
-  | IsCoFixpoint
-
-type notations = (Vernacexpr.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
-
-type program_info_aux = {
-  prg_name: Id.t;
-  prg_body: constr;
-  prg_type: constr;
-  prg_ctx:  Evd.evar_universe_context;
-  prg_pl: Id.t Loc.located list option;
-  prg_obligations: obligations;
-  prg_deps : Id.t list;
-  prg_fixkind : fixpoint_kind option ;
-  prg_implicits : (Constrexpr.explicitation * (bool * bool * bool)) list;
-  prg_notations : notations ;
-  prg_kind : definition_kind;
-  prg_reduce : constr -> constr;
-  prg_hook : (Evd.evar_universe_context -> unit) Lemmas.declaration_hook;
-  prg_opaque : bool;
-  prg_sign: named_context_val;
-}
-
-type program_info = program_info_aux CEphemeron.key
-
-let get_info x =
-  try CEphemeron.get x
-  with CEphemeron.InvalidKey ->
-    CErrors.anomaly Pp.(str "Program obligation can't be accessed by a worker")
-
-let assumption_message = Declare.assumption_message
-
-let default_tactic = ref (Proofview.tclUNIT ())
-
-(* true = hide obligations *)
-let hide_obligations = ref false
-
-let set_hide_obligations = (:=) hide_obligations
-let get_hide_obligations () = !hide_obligations
-
-open Goptions
-let _ =
-  declare_bool_option
-    { optsync  = true;
-      optdepr  = false;
-      optname  = "Hidding of Program obligations";
-      optkey   = ["Hide";"Obligations"];
-      optread  = get_hide_obligations;
-      optwrite = set_hide_obligations; }
-
-let shrink_obligations = ref true
-
-let set_shrink_obligations = (:=) shrink_obligations
-let get_shrink_obligations () = !shrink_obligations
-
-let _ =
-  declare_bool_option
-    { optsync  = true;
-      optdepr  = true;
-      optname  = "Shrinking of Program obligations";
-      optkey   = ["Shrink";"Obligations"];
-      optread  = get_shrink_obligations;
-      optwrite = set_shrink_obligations; }
-
-let evar_of_obligation o = make_evar (Global.named_context_val ()) o.obl_type
-
-let get_body obl =
-  match obl.obl_body with
-  | None -> None
-  | Some (DefinedObl c) ->
-    let ctx = Environ.constant_context (Global.env ()) c in
-    let pc = (c, Univ.UContext.instance ctx) in
-      Some (DefinedObl pc)
-  | Some (TermObl c) ->
-      Some (TermObl c)
-
-let get_obligation_body expand obl =
-  match get_body obl with
-  | None -> None
-  | Some c ->
-     if expand && snd obl.obl_status == Evar_kinds.Expand then
-       match c with
-       | DefinedObl pc -> Some (constant_value_in (Global.env ()) pc)
-       | TermObl c -> Some c
-     else (match c with
-	   | DefinedObl pc -> Some (mkConstU pc)
-	   | TermObl c -> Some c)
-
-let obl_substitution expand obls deps =
-  Int.Set.fold
-    (fun x acc ->
-       let xobl = obls.(x) in
-       match get_obligation_body expand xobl with
-       | None -> acc
-       | Some oblb -> (xobl.obl_name, (xobl.obl_type, oblb)) :: acc)
-    deps []
-
-let subst_deps expand obls deps t =
-  let osubst = obl_substitution expand obls deps in
-    (Vars.replace_vars (List.map (fun (n, (_, b)) -> n, b) osubst) t)
-
-let rec prod_app t n =
-  match kind_of_term (strip_outer_cast t) with
-    | Prod (_,_,b) -> subst1 n b
-    | LetIn (_, b, t, b') -> prod_app (subst1 b b') n
-    | _ ->
-	errorlabstrm "prod_app"
-	  (str"Needed a product, but didn't find one" ++ fnl ())
-
-
-(* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *)
-let prod_applist t nL = List.fold_left prod_app t nL
-
-let replace_appvars subst =
-  let rec aux c = 
-    let f, l = decompose_app c in
-      if isVar f then
-	try
-	  let c' = List.map (map_constr aux) l in
-	  let (t, b) = Id.List.assoc (destVar f) subst in
-	    mkApp (delayed_force hide_obligation, 
-		   [| prod_applist t c'; applistc b c' |])
-	with Not_found -> map_constr aux c
-      else map_constr aux c
-  in map_constr aux
-       
-let subst_prog expand obls ints prg =
-  let subst = obl_substitution expand obls ints in
-    if get_hide_obligations () then
-      (replace_appvars subst prg.prg_body,
-       replace_appvars subst ((* Termops.refresh_universes *) prg.prg_type))
-    else 
-      let subst' = List.map (fun (n, (_, b)) -> n, b) subst in
-	(Vars.replace_vars subst' prg.prg_body,
-	 Vars.replace_vars subst' ((* Termops.refresh_universes *) prg.prg_type))
-
-let subst_deps_obl obls obl =
-  let t' = subst_deps true obls obl.obl_deps obl.obl_type in
-    { obl with obl_type = t' }
-
-module ProgMap = Id.Map
-
-let map_replace k v m = ProgMap.add k (CEphemeron.create v) (ProgMap.remove k m)
-
-let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m []
-
-let from_prg : program_info ProgMap.t ref =
-  Summary.ref ProgMap.empty ~name:"program-tcc-table"
-
-let close sec =
-  if not (ProgMap.is_empty !from_prg) then
-    let keys = map_keys !from_prg in
-      errorlabstrm "Program" 
-	(str "Unsolved obligations when closing " ++ str sec ++ str":" ++ spc () ++
-	   prlist_with_sep spc (fun x -> Nameops.pr_id x) keys ++
-	   (str (if Int.equal (List.length keys) 1 then " has " else " have ") ++
-	      str "unsolved obligations"))
-
-let input : program_info ProgMap.t -> obj =
-  declare_object
-    { (default_object "Program state") with
-      cache_function = (fun (na, pi) -> from_prg := pi);
-      load_function = (fun _ (_, pi) -> from_prg := pi);
-      discharge_function = (fun _ -> close "section"; None);
-      classify_function = (fun _ -> close "module"; Dispose) }
-    
-open Evd
-
-let progmap_remove prg =
-  Lib.add_anonymous_leaf (input (ProgMap.remove prg.prg_name !from_prg))
-  
-let progmap_add n prg =
-  Lib.add_anonymous_leaf (input (ProgMap.add n prg !from_prg))
-
-let progmap_replace prg' = 
-  Lib.add_anonymous_leaf (input (map_replace prg'.prg_name prg' !from_prg))
-
-let rec intset_to = function
-    -1 -> Int.Set.empty
-  | n -> Int.Set.add n (intset_to (pred n))
-
-let subst_body expand prg =
-  let obls, _ = prg.prg_obligations in
-  let ints = intset_to (pred (Array.length obls)) in
-    subst_prog expand obls ints prg
-
-let declare_definition prg =
-  let body, typ = subst_body true prg in
-  let nf = Universes.nf_evars_and_universes_opt_subst (fun x -> None)
-    (Evd.evar_universe_context_subst prg.prg_ctx) in
-  let opaque = prg.prg_opaque in
-  let fix_exn = Stm.get_fix_exn () in
-  let pl, ctx =
-    Evd.universe_context ?names:prg.prg_pl (Evd.from_ctx prg.prg_ctx) in
-  let ce =
-    definition_entry ~fix_exn
-     ~opaque ~types:(nf typ) ~poly:(pi2 prg.prg_kind)
-     ~univs:(Evd.evar_context_universe_context prg.prg_ctx) (nf body)
-  in
-  let () = progmap_remove prg in
-  let cst =
-    !declare_definition_ref prg.prg_name 
-     prg.prg_kind ce prg.prg_implicits
-     (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r prg.prg_ctx; r))
-  in
-  Universes.register_universe_binders cst pl;
-  cst
-      
-open Pp
-
-let rec lam_index n t acc =
-  match kind_of_term t with
-    | Lambda (Name n', _, _) when Id.equal n n' ->
-      acc
-    | Lambda (_, _, b) ->
-	lam_index n b (succ acc)
-    | _ -> raise Not_found
-
-let compute_possible_guardness_evidences (n,_) fixbody fixtype =
-  match n with
-  | Some (loc, n) -> [lam_index n fixbody 0]
-  | None ->
-      (* If recursive argument was not given by user, we try all args.
-	 An earlier approach was to look only for inductive arguments,
-	 but doing it properly involves delta-reduction, and it finally
-         doesn't seem to worth the effort (except for huge mutual
-	 fixpoints ?) *)
-      let m = Termops.nb_prod fixtype in
-      let ctx = fst (decompose_prod_n_assum m fixtype) in
-	List.map_i (fun i _ -> i) 0 ctx
-
-let mk_proof c = ((c, Univ.ContextSet.empty), Safe_typing.empty_private_constants)
-
-let declare_mutual_definition l =
-  let len = List.length l in
-  let first = List.hd l in
-  let fixdefs, fixtypes, fiximps =
-    List.split3
-      (List.map (fun x -> 
-	let subs, typ = (subst_body true x) in
-	let term = snd (Reductionops.splay_lam_n (Global.env ()) Evd.empty len subs) in
-	let typ = snd (Reductionops.splay_prod_n (Global.env ()) Evd.empty len typ) in
-	  x.prg_reduce term, x.prg_reduce typ, x.prg_implicits) l)
-  in
-(*   let fixdefs = List.map reduce_fix fixdefs in *)
-  let fixkind = Option.get first.prg_fixkind in
-  let arrrec, recvec = Array.of_list fixtypes, Array.of_list fixdefs in
-  let fixdecls = (Array.of_list (List.map (fun x -> Name x.prg_name) l), arrrec, recvec) in
-  let (local,poly,kind) = first.prg_kind in
-  let fixnames = first.prg_deps in
-  let opaque = first.prg_opaque in
-  let kind = if fixkind != IsCoFixpoint then Fixpoint else CoFixpoint in
-  let indexes, fixdecls =
-    match fixkind with
-      | IsFixpoint wfl ->
-	  let possible_indexes =
-	    List.map3 compute_possible_guardness_evidences
-              wfl fixdefs fixtypes in
-	  let indexes = 
-              Pretyping.search_guard
-              Loc.ghost (Global.env())
-              possible_indexes fixdecls in
-          Some indexes, 
-          List.map_i (fun i _ ->
-            mk_proof (mkFix ((indexes,i),fixdecls))) 0 l
-      | IsCoFixpoint ->
-          None,
-          List.map_i (fun i _ ->
-            mk_proof (mkCoFix (i,fixdecls))) 0 l
-  in
-  (* Declare the recursive definitions *)
-  let ctx = Evd.evar_context_universe_context first.prg_ctx in
-  let fix_exn = Stm.get_fix_exn () in
-  let kns = List.map4 (!declare_fix_ref ~opaque (local, poly, kind) ctx)
-    fixnames fixdecls fixtypes fiximps in
-    (* Declare notations *)
-    List.iter Metasyntax.add_notation_interpretation first.prg_notations;
-    Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames;
-    let gr = List.hd kns in
-    let kn = match gr with ConstRef kn -> kn | _ -> assert false in
-    Lemmas.call_hook fix_exn first.prg_hook local gr first.prg_ctx;
-    List.iter progmap_remove l; kn
-
-let decompose_lam_prod c ty =
-  let open Context.Rel.Declaration in
-  let rec aux ctx c ty =
-    match kind_of_term c, kind_of_term ty with
-    | LetIn (x, b, t, c), LetIn (x', b', t', ty)
-	 when eq_constr b b' && eq_constr t t' ->
-       let ctx' = Context.Rel.add (LocalDef (x,b',t')) ctx in
-       aux ctx' c ty
-    | _, LetIn (x', b', t', ty) ->
-       let ctx' = Context.Rel.add (LocalDef (x',b',t')) ctx in
-       aux ctx' (lift 1 c) ty
-    | LetIn (x, b, t, c), _ ->
-       let ctx' = Context.Rel.add (LocalDef (x,b,t)) ctx in
-       aux ctx' c (lift 1 ty)
-    | Lambda (x, b, t), Prod (x', b', t')
-       (* By invariant, must be convertible *) ->
-       let ctx' = Context.Rel.add (LocalAssum (x,b')) ctx in
-       aux ctx' t t'
-    | Cast (c, _, _), _ -> aux ctx c ty
-    | _, _ -> ctx, c, ty
-  in aux Context.Rel.empty c ty
-
-let shrink_body c ty =
-  let open Context.Rel.Declaration in
-  let ctx, b, ty =
-    match ty with
-    | None ->
-       let ctx, b = decompose_lam_assum c in
-       ctx, b, None
-    | Some ty ->
-       let ctx, b, ty = decompose_lam_prod c ty in
-       ctx, b, Some ty
-  in
-  let b', ty', n, args =
-    List.fold_left (fun (b, ty, i, args) decl ->
-        if noccurn 1 b && Option.cata (noccurn 1) true ty then
-	  subst1 mkProp b, Option.map (subst1 mkProp) ty, succ i, args
-	else
-	  let args = if is_local_assum decl then mkRel i :: args else args in
-          mkLambda_or_LetIn decl b, Option.map (mkProd_or_LetIn decl) ty,
-	  succ i, args)
-     (b, ty, 1, []) ctx
-  in ctx, b', ty', Array.of_list args
-
-let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst]
-
-let add_hint local prg cst =
-  Hints.add_hints local [Id.to_string prg.prg_name] (unfold_entry cst)
-
-let declare_obligation prg obl body ty uctx =
-  let body = prg.prg_reduce body in
-  let ty = Option.map prg.prg_reduce ty in
-  match obl.obl_status with
-  | _, Evar_kinds.Expand -> false, { obl with obl_body = Some (TermObl body) }
-  | force, Evar_kinds.Define opaque ->
-      let opaque = not force && opaque in
-      let poly = pi2 prg.prg_kind in
-      let ctx, body, ty, args =
-	if get_shrink_obligations () && not poly then
-	  shrink_body body ty else [], body, ty, [||]
-      in
-      let body = ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in
-      let ce =
-        { const_entry_body = Future.from_val ~fix_exn:(fun x -> x) body;
-          const_entry_secctx = None;
-	  const_entry_type = ty;
-	  const_entry_polymorphic = poly;
-	  const_entry_universes = uctx;
-	  const_entry_opaque = opaque;
-          const_entry_inline_code = false;
-          const_entry_feedback = None;
-      } in
-      (** ppedrot: seems legit to have obligations as local *)
-      let constant = Declare.declare_constant obl.obl_name ~local:true
-	(DefinitionEntry ce,IsProof Property)
-      in
-	if not opaque then add_hint false prg constant;
-	definition_message obl.obl_name;
-	true, { obl with obl_body =
-	    if poly then
-	      Some (DefinedObl constant)
-	    else
-	      Some (TermObl (it_mkLambda_or_LetIn (mkApp (mkConst constant, args)) ctx)) }
-
-let init_prog_info ?(opaque = false) sign n pl b t ctx deps fixkind
-		   notations obls impls kind reduce hook =
-  let obls', b =
-    match b with
-    | None ->
-	assert(Int.equal (Array.length obls) 0);
-	let n = Nameops.add_suffix n "_obligation" in
-	  [| { obl_name = n; obl_body = None;
-	       obl_location = Loc.ghost, Evar_kinds.InternalHole; obl_type = t;
-	       obl_status = false, Evar_kinds.Expand; obl_deps = Int.Set.empty;
-	       obl_tac = None } |],
-	mkVar n
-    | Some b ->
-	Array.mapi
-	  (fun i (n, t, l, o, d, tac) ->
-            { obl_name = n ; obl_body = None; 
-	      obl_location = l; obl_type = t; obl_status = o;
-	      obl_deps = d; obl_tac = tac })
-	  obls, b
-  in
-    { prg_name = n ; prg_body = b; prg_type = reduce t; 
-      prg_ctx = ctx; prg_pl = pl;
-      prg_obligations = (obls', Array.length obls');
-      prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ;
-      prg_implicits = impls; prg_kind = kind; prg_reduce = reduce; 
-      prg_hook = hook; prg_opaque = opaque;
-      prg_sign = sign }
-
-let map_cardinal m =
-  let i = ref 0 in
-  ProgMap.iter (fun _ v ->
-		if snd (CEphemeron.get v).prg_obligations > 0 then incr i) m;
-  !i
-
-exception Found of program_info
-
-let map_first m =
-  try
-    ProgMap.iter (fun _ v ->
-		  if snd (CEphemeron.get v).prg_obligations > 0 then
-		    raise (Found v)) m;
-    assert(false)
-  with Found x -> x
-
-let get_prog name =
-  let prg_infos = !from_prg in
-    match name with
-	Some n ->
-	  (try get_info (ProgMap.find n prg_infos)
-	   with Not_found -> raise (NoObligations (Some n)))
-      | None ->
-	  (let n = map_cardinal prg_infos in
-	     match n with
-		 0 -> raise (NoObligations None)
-	       | 1 -> get_info (map_first prg_infos)
-	       | _ ->
-                let progs = Id.Set.elements (ProgMap.domain prg_infos) in
-                let prog = List.hd progs in
-                let progs = prlist_with_sep pr_comma Nameops.pr_id progs in
-                errorlabstrm ""
-                  (str "More than one program with unsolved obligations: " ++ progs
-                  ++ str "; use the \"of\" clause to specify, as in \"Obligation 1 of " ++ Nameops.pr_id prog ++ str "\""))
-
-let get_any_prog () =
-  let prg_infos = !from_prg in
-  let n = map_cardinal prg_infos in
-  if n > 0 then get_info (map_first prg_infos)
-  else raise (NoObligations None)
-
-let get_prog_err n =
-  try get_prog n with NoObligations id -> pperror (explain_no_obligations id)
-
-let get_any_prog_err () =
-  try get_any_prog () with NoObligations id -> pperror (explain_no_obligations id)
-
-let obligations_solved prg = Int.equal (snd prg.prg_obligations) 0
-
-let all_programs () =
-  ProgMap.fold (fun k p l -> p :: l) !from_prg []
-
-type progress =
-    | Remain of int
-    | Dependent
-    | Defined of global_reference
-
-let obligations_message rem =
-  if rem > 0 then
-    if Int.equal rem 1 then
-      Flags.if_verbose Feedback.msg_info (int rem ++ str " obligation remaining")
-    else
-      Flags.if_verbose Feedback.msg_info (int rem ++ str " obligations remaining")
-  else
-    Flags.if_verbose Feedback.msg_info (str "No more obligations remaining")
-
-let update_obls prg obls rem =
-  let prg' = { prg with prg_obligations = (obls, rem) } in
-    progmap_replace prg';
-    obligations_message rem;
-    if rem > 0 then Remain rem
-    else (
-      match prg'.prg_deps with
-      | [] ->
-	  let kn = declare_definition prg' in
-	    progmap_remove prg';
-	    Defined kn
-      | l ->
-	  let progs = List.map (fun x -> get_info (ProgMap.find x !from_prg)) prg'.prg_deps in
-	    if List.for_all (fun x -> obligations_solved x) progs then
-	      let kn = declare_mutual_definition progs in
-		Defined (ConstRef kn)
-	    else Dependent)
-
-let is_defined obls x = not (Option.is_empty obls.(x).obl_body)
-
-let deps_remaining obls deps =
-  Int.Set.fold
-    (fun x acc ->
-      if is_defined obls x then acc
-      else x :: acc)
-    deps []
-
-let dependencies obls n =
-  let res = ref Int.Set.empty in
-    Array.iteri
-      (fun i obl ->
-	if not (Int.equal i n) && Int.Set.mem n obl.obl_deps then
-	  res := Int.Set.add i !res)
-      obls;
-    !res
-
-let goal_kind poly = Decl_kinds.Local, poly, Decl_kinds.DefinitionBody Decl_kinds.Definition
-
-let goal_proof_kind poly = Decl_kinds.Local, poly, Decl_kinds.Proof Decl_kinds.Lemma
-
-let kind_of_obligation poly o =
-  match o with
-  | Evar_kinds.Define false | Evar_kinds.Expand -> goal_kind poly
-  | _ -> goal_proof_kind poly
-
-let not_transp_msg =
-  str "Obligation should be transparent but was declared opaque." ++ spc () ++
-    str"Use 'Defined' instead."
-
-let err_not_transp () = pperror not_transp_msg
-
-let rec string_of_list sep f = function
-    [] -> ""
-  | x :: [] -> f x
-  | x :: ((y :: _) as tl) -> f x ^ sep ^ string_of_list sep f tl
-
-(* Solve an obligation using tactics, return the corresponding proof term *)
-
-let solve_by_tac name evi t poly ctx =
-  let id = name in
-  let concl = evi.evar_concl in
-  (* spiwack: the status is dropped. *)
-  let (entry,_,ctx') = Pfedit.build_constant_by_tactic 
-    id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps concl (Tacticals.New.tclCOMPLETE t) in
-  let env = Global.env () in
-  let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in
-  let body, eff = Future.force entry.const_entry_body in
-  assert(Safe_typing.empty_private_constants = eff);
-  let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in
-  Inductiveops.control_only_guard (Global.env ()) (fst body);
-  (fst body), entry.const_entry_type, Evd.evar_universe_context ctx'
-
-let obligation_terminator name num guard hook auto pf =
-  let open Proof_global in
-  let term = Lemmas.universe_proof_terminator guard hook in
-  match pf with
-  | Admitted _ -> apply_terminator term pf
-  | Proved (opq, id, proof) ->
-    if not !shrink_obligations then apply_terminator term pf
-    else
-      let (_, (entry, uctx, _)) = Pfedit.cook_this_proof proof in
-      let env = Global.env () in
-      let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in
-      let ty = entry.Entries.const_entry_type in
-      let (body, cstr), eff = Future.force entry.Entries.const_entry_body in
-      assert(Safe_typing.empty_private_constants = eff);
-      let sigma = Evd.from_ctx (fst uctx) in
-      let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in
-      Inductiveops.control_only_guard (Global.env ()) body;
-      (** Declare the obligation ourselves and drop the hook *)
-      let prg = get_info (ProgMap.find name !from_prg) in
-      let ctx = Evd.evar_universe_context sigma in
-      let prg = { prg with prg_ctx = ctx } in
-      let obls, rem = prg.prg_obligations in
-      let obl = obls.(num) in
-      let status =
-        match obl.obl_status, opq with
-        | (_, Evar_kinds.Expand), Vernacexpr.Opaque _ -> err_not_transp ()
-        | (true, _), Vernacexpr.Opaque _ -> err_not_transp ()
-        | (false, _), Vernacexpr.Opaque _ -> Evar_kinds.Define true
-        | (_, Evar_kinds.Define true), Vernacexpr.Transparent -> Evar_kinds.Define false
-        | (_, status), Vernacexpr.Transparent -> status
-      in
-      let obl = { obl with obl_status = false, status } in
-      let uctx = Evd.evar_context_universe_context ctx in
-      let (_, obl) = declare_obligation prg obl body ty uctx in
-      let obls = Array.copy obls in
-      let _ = obls.(num) <- obl in
-      try
-      ignore (update_obls prg obls (pred rem));
-      if pred rem > 0 then
-        begin
-	  let deps = dependencies obls num in
-	  if not (Int.Set.is_empty deps) then
-	    ignore (auto (Some name) None deps)
-	end
-      with e when CErrors.noncritical e ->
-        let e = CErrors.push e in
-        pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e))
-
-let obligation_hook prg obl num auto ctx' _ gr =
-  let obls, rem = prg.prg_obligations in
-  let cst = match gr with ConstRef cst -> cst | _ -> assert false in
-  let transparent = evaluable_constant cst (Global.env ()) in
-  let () = match obl.obl_status with
-      (true, Evar_kinds.Expand) 
-    | (true, Evar_kinds.Define true) ->
-       if not transparent then err_not_transp ()
-    | _ -> ()
-in
-  let obl = { obl with obl_body = Some (DefinedObl cst) } in
-  let () = if transparent then add_hint true prg cst in
-  let obls = Array.copy obls in
-  let _ = obls.(num) <- obl in
-  let ctx' = match ctx' with None -> prg.prg_ctx | Some ctx' -> ctx' in
-  let ctx' =
-    if not (pi2 prg.prg_kind) (* Not polymorphic *) then
-      (* The universe context was declared globally, we continue
-         from the new global environment. *)
-      let evd = Evd.from_env (Global.env ()) in
-      let ctx' = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx')) in
-        Evd.evar_universe_context ctx'
-    else ctx'
-  in
-  let prg = { prg with prg_ctx = ctx' } in
-  let () =
-    try ignore (update_obls prg obls (pred rem))
-    with e when CErrors.noncritical e ->
-      let e = CErrors.push e in
-      pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e))
-  in
-  if pred rem > 0 then begin
-    let deps = dependencies obls num in
-    if not (Int.Set.is_empty deps) then
-      ignore (auto (Some prg.prg_name) None deps)
-  end
-
-let rec solve_obligation prg num tac =
-  let user_num = succ num in
-  let obls, rem = prg.prg_obligations in
-  let obl = obls.(num) in
-  let remaining = deps_remaining obls obl.obl_deps in
-  let () =
-    if not (Option.is_empty obl.obl_body) then
-      pperror (str "Obligation" ++ spc () ++ int user_num ++ str "already" ++ spc() ++ str "solved.");
-    if not (List.is_empty remaining) then
-      pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) "
-        ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) remaining));
-  in
-  let obl = subst_deps_obl obls obl in
-  let kind = kind_of_obligation (pi2 prg.prg_kind) (snd obl.obl_status) in
-  let evd = Evd.from_ctx prg.prg_ctx in
-  let evd = Evd.update_sigma_env evd (Global.env ()) in
-  let auto n tac oblset = auto_solve_obligations n ~oblset tac in
-  let terminator guard hook =
-    Proof_global.make_terminator
-      (obligation_terminator prg.prg_name num guard hook auto) in
-  let hook ctx = Lemmas.mk_hook (obligation_hook prg obl num auto ctx) in
-  let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd obl.obl_type ~terminator hook in
-  let _ = Pfedit.by !default_tactic in
-  Option.iter (fun tac -> Pfedit.set_end_tac tac) tac
-
-and obligation (user_num, name, typ) tac =
-  let num = pred user_num in
-  let prg = get_prog_err name in
-  let obls, rem = prg.prg_obligations in
-    if num < Array.length obls then
-      let obl = obls.(num) in
-	match obl.obl_body with
-	    None -> solve_obligation prg num tac
-	  | Some r -> error "Obligation already solved"
-    else error (sprintf "Unknown obligation number %i" (succ num))
-
-
-and solve_obligation_by_tac prg obls i tac =
-  let obl = obls.(i) in
-    match obl.obl_body with
-    | Some _ -> None
-    | None ->
-	try
-	  if List.is_empty (deps_remaining obls obl.obl_deps) then
-	    let obl = subst_deps_obl obls obl in
-	    let tac =
-	      match tac with
-	      | Some t -> t
-	      | None ->
-		  match obl.obl_tac with
-		  | Some t -> t
-		  | None -> !default_tactic
-	    in
-	    let evd = Evd.from_ctx prg.prg_ctx in
-	    let evd = Evd.update_sigma_env evd (Global.env ()) in
-	    let t, ty, ctx =
-	      solve_by_tac obl.obl_name (evar_of_obligation obl) tac
-	        (pi2 prg.prg_kind) (Evd.evar_universe_context evd)
-	    in
-	    let uctx = Evd.evar_context_universe_context ctx in
-	    let prg = {prg with prg_ctx = ctx} in
-	    let def, obl' = declare_obligation prg obl t ty uctx in
-	      obls.(i) <- obl';
-	      if def && not (pi2 prg.prg_kind) then (
-	        (* Declare the term constraints with the first obligation only *)
-	        let evd = Evd.from_env (Global.env ()) in
-	        let evd = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx)) in
-		let ctx' = Evd.evar_universe_context evd in
-		  Some {prg with prg_ctx = ctx'})
-	      else Some prg
-	  else None
-	with e when CErrors.noncritical e ->
-          let (e, _) = CErrors.push e in
-          match e with
-	  | Refiner.FailError (_, s) ->
-	      user_err_loc (fst obl.obl_location, "solve_obligation", Lazy.force s)
-          | e -> None (* FIXME really ? *)
-
-and solve_prg_obligations prg ?oblset tac =
-  let obls, rem = prg.prg_obligations in
-  let rem = ref rem in
-  let obls' = Array.copy obls in
-  let set = ref Int.Set.empty in
-  let p = match oblset with
-    | None -> (fun _ -> true)
-    | Some s -> set := s;
-      (fun i -> Int.Set.mem i !set)
-  in
-  let prgref = ref prg in
-  let _ =
-    Array.iteri (fun i x ->
-      if p i then
-        match solve_obligation_by_tac !prgref obls' i tac with
-	| None -> ()
- 	| Some prg' ->
-	   prgref := prg';
-	   let deps = dependencies obls i in
- 	   (set := Int.Set.union !set deps;
- 	    decr rem))
-      obls'
-  in
-    update_obls !prgref obls' !rem
-
-and solve_obligations n tac =
-  let prg = get_prog_err n in
-    solve_prg_obligations prg tac
-
-and solve_all_obligations tac =
-  ProgMap.iter (fun k v -> ignore(solve_prg_obligations (get_info v) tac)) !from_prg
-
-and try_solve_obligation n prg tac =
-  let prg = get_prog prg in
-  let obls, rem = prg.prg_obligations in
-  let obls' = Array.copy obls in
-    match solve_obligation_by_tac prg obls' n tac with
-    | Some prg' -> ignore(update_obls prg' obls' (pred rem))
-    | None -> ()
-
-and try_solve_obligations n tac =
-  try ignore (solve_obligations n tac) with NoObligations _ -> ()
-
-and auto_solve_obligations n ?oblset tac : progress =
-  Flags.if_verbose Feedback.msg_info (str "Solving obligations automatically...");
-  try solve_prg_obligations (get_prog_err n) ?oblset tac with NoObligations _ -> Dependent
-
-open Pp
-let show_obligations_of_prg ?(msg=true) prg =
-  let n = prg.prg_name in
-  let obls, rem = prg.prg_obligations in
-  let showed = ref 5 in
-    if msg then Feedback.msg_info (int rem ++ str " obligation(s) remaining: ");
-    Array.iteri (fun i x ->
-		   match x.obl_body with
-		   | None ->
-		       if !showed > 0 then (
-		         decr showed;
-			 let x = subst_deps_obl obls x in
-			 Feedback.msg_info (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++
-				   str "of" ++ spc() ++ Id.print n ++ str ":" ++ spc () ++
-				   hov 1 (Printer.pr_constr_env (Global.env ()) Evd.empty x.obl_type ++
-					    str "." ++ fnl ())))
-		   | Some _ -> ())
-      obls
-
-let show_obligations ?(msg=true) n =
-  let progs = match n with
-    | None -> all_programs ()
-    | Some n ->
-	try [ProgMap.find n !from_prg]
-	with Not_found -> raise (NoObligations (Some n))
-  in List.iter (fun x -> show_obligations_of_prg ~msg (get_info x)) progs
-
-let show_term n =
-  let prg = get_prog_err n in
-  let n = prg.prg_name in
-    (Id.print n ++ spc () ++ str":" ++ spc () ++
-	     Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
-	    ++ Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_body)
-
-let add_definition n ?term t ctx ?pl ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
-    ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) obls =
-  let sign = Decls.initialize_named_context_for_proof () in
-  let info = Id.print n ++ str " has type-checked" in
-  let prg = init_prog_info sign ~opaque n pl term t ctx [] None [] obls implicits kind reduce hook in
-  let obls,_ = prg.prg_obligations in
-  if Int.equal (Array.length obls) 0 then (
-    Flags.if_verbose Feedback.msg_info (info ++ str ".");
-    let cst = declare_definition prg in
-      Defined cst)
-  else (
-    let len = Array.length obls in
-    let _ = Flags.if_verbose Feedback.msg_info (info ++ str ", generating " ++ int len ++ str " obligation(s)") in
-      progmap_add n (CEphemeron.create prg);
-      let res = auto_solve_obligations (Some n) tactic in
-	match res with
-	| Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
-	| _ -> res)
-
-let add_mutual_definitions l ctx ?pl ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce)
-    ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) notations fixkind =
-  let sign = Decls.initialize_named_context_for_proof () in
-  let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
-    List.iter
-    (fun  (n, b, t, imps, obls) ->
-     let prg = init_prog_info sign ~opaque n pl (Some b) t ctx deps (Some fixkind)
-       notations obls imps kind reduce hook 
-     in progmap_add n (CEphemeron.create prg)) l;
-    let _defined =
-      List.fold_left (fun finished x ->
-	if finished then finished
-	else
-	  let res = auto_solve_obligations (Some x) tactic in
-	    match res with
-	    | Defined _ -> 
-		(* If one definition is turned into a constant, 
-		   the whole block is defined. *) true
-	    | _ -> false)
-	false deps
-    in ()
-
-let admit_prog prg =
-  let obls, rem = prg.prg_obligations in
-  let obls = Array.copy obls in
-    Array.iteri 
-      (fun i x ->
-        match x.obl_body with
-        | None ->
-            let x = subst_deps_obl obls x in
-	    let ctx = Evd.evar_context_universe_context prg.prg_ctx in
-            let kn = Declare.declare_constant x.obl_name ~local:true
-              (ParameterEntry (None,false,(x.obl_type,ctx),None), IsAssumption Conjectural)
-            in
-              assumption_message x.obl_name;
-              obls.(i) <- { x with obl_body = Some (DefinedObl kn) }
-        | Some _ -> ())
-      obls;
-    ignore(update_obls prg obls 0)
-
-let rec admit_all_obligations () =
-  let prg = try Some (get_any_prog ()) with NoObligations _ -> None in
-  match prg with
-  | None -> ()
-  | Some prg ->
-    admit_prog prg;
-    admit_all_obligations ()
-
-let admit_obligations n =
-  match n with
-  | None -> admit_all_obligations ()
-  | Some _ ->
-    let prg = get_prog_err n in
-    admit_prog prg
-
-let next_obligation n tac =
-  let prg = match n with
-  | None -> get_any_prog_err ()
-  | Some _ -> get_prog_err n
-  in
-  let obls, rem = prg.prg_obligations in
-  let is_open _ x = Option.is_empty x.obl_body && List.is_empty (deps_remaining obls x.obl_deps) in
-  let i = match Array.findi is_open obls with
-  | Some i -> i
-  | None -> anomaly (Pp.str "Could not find a solvable obligation.")
-  in
-  solve_obligation prg i tac
-
-let init_program () =
-  Coqlib.check_required_library Coqlib.datatypes_module_name;
-  Coqlib.check_required_library ["Coq";"Init";"Specif"];
-  Coqlib.check_required_library ["Coq";"Program";"Tactics"]
-
-
-let set_program_mode c =
-  if c then
-    if !Flags.program_mode then ()
-    else begin
-      init_program ();
-      Flags.program_mode := true;
-    end