Move [delayed] to util and use [force_delayed] everywhere to force

thunks. Move from [lazy] to [delayed] in subtac.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13227 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 127 insertions, 128 deletions

diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml
index 491b44fbb..d84a9d2ed 100644
--- a/plugins/subtac/subtac_cases.ml
+++ b/plugins/subtac/subtac_cases.ml
@@ -20,13 +20,11 @@ open Sign
 open Reductionops
 open Typeops
 open Type_errors
-
 open Rawterm
 open Retyping
 open Pretype_errors
 open Evarutil
 open Evarconv
-
 open Subtac_utils
 
 (************************************************************************)
@@ -1511,11 +1509,11 @@ let eq_id avoid id =
   let hid' = next_ident_away hid avoid in
     hid'
 
-let mk_eq typ x y = mkApp (Lazy.force eq_ind, [| typ; x ; y |])
-let mk_eq_refl typ x = mkApp (Lazy.force eq_refl, [| typ; x |])
+let mk_eq typ x y = mkApp (delayed_force eq_ind, [| typ; x ; y |])
+let mk_eq_refl typ x = mkApp (delayed_force eq_refl, [| typ; x |])
 let mk_JMeq typ x typ' y =
-  mkApp (Lazy.force Subtac_utils.jmeq_ind, [| typ; x ; typ'; y |])
-let mk_JMeq_refl typ x = mkApp (Lazy.force Subtac_utils.jmeq_refl, [| typ; x |])
+  mkApp (delayed_force Subtac_utils.jmeq_ind, [| typ; x ; typ'; y |])
+let mk_JMeq_refl typ x = mkApp (delayed_force Subtac_utils.jmeq_refl, [| typ; x |])
 
 let hole = RHole (dummy_loc, Evd.QuestionMark (Evd.Define true))
 
@@ -1607,7 +1605,7 @@ let vars_of_ctx ctx =
 	| Some t' when kind_of_term t' = Rel 0 ->
 	    prev,
 	    (RApp (dummy_loc,
-		(RRef (dummy_loc, Lazy.force refl_ref)), [hole; RVar (dummy_loc, prev)])) :: vars
+		(RRef (dummy_loc, delayed_force refl_ref)), [hole; RVar (dummy_loc, prev)])) :: vars
 	| _ ->
 	    match na with
 		Anonymous -> raise (Invalid_argument "vars_of_ctx")
@@ -1648,7 +1646,7 @@ let build_ineqs prevpatterns pats liftsign =
 			  lift_rel_context len ppat_sign @ sign,
 			  len',
 			  succ n, (* nth pattern *)
-			  mkApp (Lazy.force eq_ind,
+			  mkApp (delayed_force eq_ind,
 				[| lift (len' + liftsign) curpat_ty;
 				   liftn (len + liftsign) (succ lens) ppat_c ;
 				   lift len' curpat_c |]) ::
diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml
index fe4db0de1..4efe3cc59 100644
--- a/plugins/subtac/subtac_coercion.ml
+++ b/plugins/subtac/subtac_coercion.ml
@@ -36,7 +36,7 @@ let rec disc_subset x =
       (match kind_of_term c with
       Ind i ->
 	let len = Array.length l in
-	let sig_ = Lazy.force sig_ in
+	let sig_ = delayed_force sig_ in
 	  if len = 2 && i = Term.destInd sig_.typ
 	  then
 	    let (a, b) = pair_of_array l in
@@ -50,7 +50,7 @@ and disc_exist env x =
   | App (c, l) ->
       (match kind_of_term c with
       Construct c ->
-	if c = Term.destConstruct (Lazy.force sig_).intro
+	if c = Term.destConstruct (delayed_force sig_).intro
 	then Some (l.(0), l.(1), l.(2), l.(3))
 	else None
       | _ -> None)
@@ -63,7 +63,7 @@ module Coercion = struct
   let disc_proj_exist env x =
     match kind_of_term x with
       | App (c, l) ->
-	  (if Term.eq_constr c (Lazy.force sig_).proj1
+	  (if Term.eq_constr c (delayed_force sig_).proj1
 	     && Array.length l = 3
 	   then disc_exist env l.(2)
 	   else None)
@@ -97,7 +97,7 @@ module Coercion = struct
 	  Some (u, p) ->
 	    let f, ct = aux u in
 	      (Some (fun x ->
-		       app_opt f (mkApp ((Lazy.force sig_).proj1,
+		       app_opt f (mkApp ((delayed_force sig_).proj1,
 					 [| u; p; x |]))),
 	       ct)
 	| None -> (None, v)
@@ -143,9 +143,9 @@ module Coercion = struct
 		in
 		let args = List.rev (restargs @ mkRel 1 :: lift_args 1 tele) in
 		let pred = mkLambda (n, eqT, applistc (lift 1 c) args) in
-		let eq = mkApp (Lazy.force eq_ind, [| eqT; hdx; hdy |]) in
+		let eq = mkApp (delayed_force eq_ind, [| eqT; hdx; hdy |]) in
 		let evar = make_existential loc env isevars eq in
-		let eq_app x = mkApp (Lazy.force eq_rect,
+		let eq_app x = mkApp (delayed_force eq_rect,
 				      [| eqT; hdx; pred; x; hdy; evar|]) in
 		  aux (hdy :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i)  (fun x -> eq_app (co x))
 	  else Some co
@@ -184,8 +184,8 @@ module Coercion = struct
 	      (match kind_of_term c, kind_of_term c' with
 		   Ind i, Ind i' -> (* Inductive types *)
 		     let len = Array.length l in
-		     let existS = Lazy.force existS in
-		     let prod = Lazy.force prod in
+		     let existS = delayed_force existS in
+		     let prod = delayed_force prod in
 		       (* Sigma types *)
 		       if len = Array.length l' && len = 2 && i = i'
 			 && (i = Term.destInd existS.typ || i = Term.destInd prod.typ)
@@ -276,7 +276,7 @@ module Coercion = struct
 	  Some (u, p) ->
 	    let c = coerce_unify env u y in
 	    let f x =
-	      app_opt c (mkApp ((Lazy.force sig_).proj1,
+	      app_opt c (mkApp ((delayed_force sig_).proj1,
 				[| u; p; x |]))
 	    in Some f
 	| None ->
@@ -289,7 +289,7 @@ module Coercion = struct
 			 let evar = make_existential loc env isevars (mkApp (p, [| cx |]))
 			 in
 			   (mkApp
-			      ((Lazy.force sig_).intro,
+			      ((delayed_force sig_).intro,
 			       [| u; p; cx; evar |])))
 	      | None ->
 		  raise NoSubtacCoercion
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index d93a4b695..0027cb1ff 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -256,14 +256,14 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
       it_mkLambda_or_LetIn measure letbinders,
       it_mkLambda_or_LetIn measure binders
     in
-    let comb = constr_of_global (Lazy.force measure_on_R_ref) in
+    let comb = constr_of_global (delayed_force measure_on_R_ref) in
     let wf_rel = mkApp (comb, [| argtyp; relargty; rel; measure |]) in
     let wf_rel_fun x y =
       mkApp (rel, [| subst1 x measure_body;
  		     subst1 y measure_body |])
     in wf_rel, wf_rel_fun, measure
   in
-  let wf_proof = mkApp (Lazy.force well_founded, [| argtyp ; wf_rel |]) in
+  let wf_proof = mkApp (delayed_force well_founded, [| argtyp ; wf_rel |]) in
   let argid' = id_of_string (string_of_id argname ^ "'") in
   let wfarg len = (Name argid', None,
   		  mkSubset (Name argid') argtyp
@@ -271,7 +271,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
   in
   let intern_bl = wfarg 1 :: [arg] in
   let _intern_env = push_rel_context intern_bl env in
-  let proj = (Lazy.force sig_).Coqlib.proj1 in
+  let proj = (delayed_force sig_).Coqlib.proj1 in
   let wfargpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel 3)) in
   let projection = (* in wfarg :: arg :: before *)
     mkApp (proj, [| argtyp ; wfargpred ; mkRel 1 |])
@@ -284,7 +284,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
   let intern_fun_binder = (Name (add_suffix recname "'"), None, intern_fun_arity_prod) in
   let curry_fun =
     let wfpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel (2 * len + 4))) in
-    let arg = mkApp ((Lazy.force sig_).intro, [| argtyp; wfpred; lift 1 make; mkRel 1 |]) in
+    let arg = mkApp ((delayed_force sig_).intro, [| argtyp; wfpred; lift 1 make; mkRel 1 |]) in
     let app = mkApp (mkRel (2 * len + 2 (* recproof + orig binders + current binders *)), [| arg |]) in
     let rcurry = mkApp (rel, [| measure; lift len measure |]) in
     let lam = (Name (id_of_string "recproof"), None, rcurry) in
@@ -310,7 +310,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
   let intern_body_lam = it_mkLambda_or_LetIn intern_body (curry_fun :: lift_lets @ fun_bl) in
   let prop = mkLambda (Name argname, argtyp, top_arity_let) in
   let def =
-    mkApp (constr_of_global (Lazy.force fix_sub_ref),
+    mkApp (constr_of_global (delayed_force fix_sub_ref),
 	  [| argtyp ; wf_rel ;
 	     make_existential dummy_loc ~opaque:(Define false) env isevars wf_proof ;
 	     prop ; intern_body_lam |])
@@ -433,7 +433,7 @@ let interp_recursive fixkind l boxed =
     List.fold_left2 (fun env' id t ->
       let sort = Retyping.get_type_of env !evdref t in
       let fixprot =
-	try mkApp (Lazy.force Subtac_utils.fix_proto, [|sort; t|])
+	try mkApp (delayed_force Subtac_utils.fix_proto, [|sort; t|])
 	with e -> t
       in
 	(id,None,fixprot) :: env')
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index 524cfd718..3bedebb14 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -253,7 +253,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	let newenv =
 	  let marked_ftys =
 	    Array.map (fun ty -> let sort = Retyping.get_type_of env !evdref ty in
-				   mkApp (Lazy.force Subtac_utils.fix_proto, [| sort; ty |]))
+			 mkApp (delayed_force Subtac_utils.fix_proto, [| sort; ty |]))
 	      ftys
 	  in
 	    push_rec_types (names,marked_ftys,[||]) env
diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml
index 06a80f68a..689b110f8 100644
--- a/plugins/subtac/subtac_utils.ml
+++ b/plugins/subtac/subtac_utils.ml
@@ -1,3 +1,5 @@
+(** -*- compile-command: "make -C ../.. plugins/subtac/subtac_plugin.cma" -*- *)
+
 open Evd
 open Libnames
 open Coqlib
@@ -18,14 +20,14 @@ let utils_module = "Utils"
 let fixsub_module = subtac_dir @ [fix_sub_module]
 let utils_module = subtac_dir @ [utils_module]
 let tactics_module = subtac_dir @ ["Tactics"]
-let init_constant dir s = gen_constant contrib_name dir s
-let init_reference dir s = gen_reference contrib_name dir s
+let init_constant dir s () = gen_constant contrib_name dir s
+let init_reference dir s () = gen_reference contrib_name dir s
 
-let fixsub = lazy (init_constant fixsub_module "Fix_sub")
-let ex_pi1 = lazy (init_constant utils_module "ex_pi1")
-let ex_pi2 = lazy (init_constant utils_module "ex_pi2")
+let fixsub = init_constant fixsub_module "Fix_sub"
+let ex_pi1 = init_constant utils_module "ex_pi1"
+let ex_pi2 = init_constant utils_module "ex_pi2"
 
-let make_ref l s = lazy (init_reference l s)
+let make_ref l s = init_reference l s
 let well_founded_ref = make_ref ["Init";"Wf"] "Well_founded"
 let acc_ref = make_ref  ["Init";"Wf"] "Acc"
 let acc_inv_ref = make_ref  ["Init";"Wf"] "Acc_inv"
@@ -41,68 +43,67 @@ let proj1_sig_ref = make_ref "Init.Specif.proj1_sig"
 let proj2_sig_ref = make_ref "Init.Specif.proj2_sig"
 
 let build_sig () =
-  { proj1 = init_constant ["Init"; "Specif"] "proj1_sig";
-    proj2 = init_constant ["Init"; "Specif"] "proj2_sig";
-    elim = init_constant ["Init"; "Specif"] "sig_rec";
-    intro = init_constant ["Init"; "Specif"] "exist";
-    typ = init_constant ["Init"; "Specif"] "sig" }
+  { proj1 = init_constant ["Init"; "Specif"] "proj1_sig" ();
+    proj2 = init_constant ["Init"; "Specif"] "proj2_sig" ();
+    elim = init_constant ["Init"; "Specif"] "sig_rec" ();
+    intro = init_constant ["Init"; "Specif"] "exist" ();
+    typ = init_constant ["Init"; "Specif"] "sig" () }
 
-let sig_ = lazy (build_sig ())
+let sig_ = build_sig
 
-let fix_proto = lazy (init_constant tactics_module "fix_proto")
+let fix_proto = init_constant tactics_module "fix_proto"
 let fix_proto_ref () = 
   match Nametab.global (make_ref "Program.Tactics.fix_proto") with
   | ConstRef c -> c
   | _ -> assert false
 
-let eq_ind = lazy (init_constant ["Init"; "Logic"] "eq")
-let eq_rec = lazy (init_constant ["Init"; "Logic"] "eq_rec")
-let eq_rect = lazy (init_constant ["Init"; "Logic"] "eq_rect")
-let eq_refl = lazy (init_constant ["Init"; "Logic"] "refl_equal")
-let eq_ind_ref = lazy (init_reference ["Init"; "Logic"] "eq")
-let refl_equal_ref = lazy (init_reference ["Init"; "Logic"] "refl_equal")
+let eq_ind = init_constant ["Init"; "Logic"] "eq"
+let eq_rec = init_constant ["Init"; "Logic"] "eq_rec"
+let eq_rect = init_constant ["Init"; "Logic"] "eq_rect"
+let eq_refl = init_constant ["Init"; "Logic"] "refl_equal"
+let eq_ind_ref = init_reference ["Init"; "Logic"] "eq"
+let refl_equal_ref = init_reference ["Init"; "Logic"] "refl_equal"
 
-let not_ref = lazy (init_constant ["Init"; "Logic"] "not")
+let not_ref = init_constant ["Init"; "Logic"] "not"
 
-let and_typ = lazy (Coqlib.build_coq_and ())
+let and_typ = Coqlib.build_coq_and
 
-let eqdep_ind = lazy (init_constant [ "Logic";"Eqdep"] "eq_dep")
-let eqdep_rec = lazy (init_constant ["Logic";"Eqdep"] "eq_dep_rec")
-let eqdep_ind_ref = lazy (init_reference [ "Logic";"Eqdep"] "eq_dep")
-let eqdep_intro_ref = lazy (init_reference [ "Logic";"Eqdep"] "eq_dep_intro")
+let eqdep_ind = init_constant [ "Logic";"Eqdep"] "eq_dep"
+let eqdep_rec = init_constant ["Logic";"Eqdep"] "eq_dep_rec"
+let eqdep_ind_ref = init_reference [ "Logic";"Eqdep"] "eq_dep"
+let eqdep_intro_ref = init_reference [ "Logic";"Eqdep"] "eq_dep_intro"
 
 let jmeq_ind =
-  lazy (check_required_library ["Coq";"Logic";"JMeq"];
-	init_constant ["Logic";"JMeq"] "JMeq")
+  init_constant ["Logic";"JMeq"] "JMeq"
+
 let jmeq_rec =
-  lazy (check_required_library ["Coq";"Logic";"JMeq"];
-	init_constant ["Logic";"JMeq"] "JMeq_rec")
+  init_constant ["Logic";"JMeq"] "JMeq_rec"
+
 let jmeq_refl =
-  lazy (check_required_library ["Coq";"Logic";"JMeq"];
-	init_constant ["Logic";"JMeq"] "JMeq_refl")
+  init_constant ["Logic";"JMeq"] "JMeq_refl"
 
-let ex_ind = lazy (init_constant ["Init"; "Logic"] "ex")
-let ex_intro = lazy (init_reference ["Init"; "Logic"] "ex_intro")
+let ex_ind = init_constant ["Init"; "Logic"] "ex"
+let ex_intro = init_reference ["Init"; "Logic"] "ex_intro"
 
-let proj1 = lazy (init_constant ["Init"; "Logic"] "proj1")
-let proj2 = lazy (init_constant ["Init"; "Logic"] "proj2")
+let proj1 = init_constant ["Init"; "Logic"] "proj1"
+let proj2 = init_constant ["Init"; "Logic"] "proj2"
 
-let boolind = lazy (init_constant ["Init"; "Datatypes"] "bool")
-let sumboolind = lazy (init_constant ["Init"; "Specif"] "sumbool")
-let natind = lazy (init_constant ["Init"; "Datatypes"] "nat")
-let intind = lazy (init_constant ["ZArith"; "binint"] "Z")
-let existSind = lazy (init_constant ["Init"; "Specif"] "sigS")
+let boolind = init_constant ["Init"; "Datatypes"] "bool"
+let sumboolind = init_constant ["Init"; "Specif"] "sumbool"
+let natind = init_constant ["Init"; "Datatypes"] "nat"
+let intind = init_constant ["ZArith"; "binint"] "Z"
+let existSind = init_constant ["Init"; "Specif"] "sigS"
 
-let existS = lazy (build_sigma_type ())
+let existS = build_sigma_type
 
-let prod = lazy (build_prod ())
+let prod = build_prod
 
 
 (* orders *)
-let well_founded = lazy (init_constant ["Init"; "Wf"] "well_founded")
-let fix = lazy (init_constant ["Init"; "Wf"] "Fix")
-let acc = lazy (init_constant ["Init"; "Wf"] "Acc")
-let acc_inv = lazy (init_constant ["Init"; "Wf"] "Acc_inv")
+let well_founded = init_constant ["Init"; "Wf"] "well_founded"
+let fix = init_constant ["Init"; "Wf"] "Fix"
+let acc = init_constant ["Init"; "Wf"] "Acc"
+let acc_inv = init_constant ["Init"; "Wf"] "Acc_inv"
 
 let extconstr = Constrextern.extern_constr true (Global.env ())
 let extsort s = Constrextern.extern_constr true (Global.env ()) (mkSort s)
@@ -151,8 +152,8 @@ let wf_relations = Hashtbl.create 10
 
 let std_relations () =
   let add k v = Hashtbl.add wf_relations k v in
-    add (init_constant ["Init"; "Peano"] "lt")
-      (lazy (init_constant ["Arith"; "Wf_nat"] "lt_wf"))
+    add (init_constant ["Init"; "Peano"] "lt" ())
+      (init_constant ["Arith"; "Wf_nat"] "lt_wf")
 
 let std_relations = Lazy.lazy_from_fun std_relations
 
@@ -226,7 +227,6 @@ let goal_fix_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Fixp
 open Tactics
 open Tacticals
 
-let id x = x
 let filter_map f l =
   let rec aux acc = function
       hd :: tl -> (match f hd with Some t -> aux (t :: acc) tl
@@ -257,51 +257,51 @@ let build_dependent_sum l =
 	  (fun typ ->
 	     let tex = mkLambda (Name n, t, typ) in
 	       conttype
-		 (mkApp (Lazy.force ex_ind, [| t; tex |])))
+		 (mkApp (ex_ind (), [| t; tex |])))
 	in
 	  aux (mkVar n :: names) conttac conttype tl
     | (n, t) :: [] ->
 	(conttac intros, conttype t)
     | [] -> raise (Invalid_argument "build_dependent_sum")
-  in aux [] id id (List.rev l)
+  in aux [] identity identity (List.rev l)
 
 open Proof_type
 open Tacexpr
 
 let mkProj1 a b c =
-  mkApp (Lazy.force proj1, [| a; b; c |])
+  mkApp (delayed_force proj1, [| a; b; c |])
 
 let mkProj2 a b c =
-  mkApp (Lazy.force proj2, [| a; b; c |])
+  mkApp (delayed_force proj2, [| a; b; c |])
 
 let mk_ex_pi1 a b c =
-  mkApp (Lazy.force ex_pi1, [| a; b; c |])
+  mkApp (delayed_force ex_pi1, [| a; b; c |])
 
 let mk_ex_pi2 a b c =
-  mkApp (Lazy.force ex_pi2, [| a; b; c |])
+  mkApp (delayed_force ex_pi2, [| a; b; c |])
 
 let mkSubset name typ prop =
-  mkApp ((Lazy.force sig_).typ,
+  mkApp ((delayed_force sig_).typ,
 	 [| typ; mkLambda (name, typ, prop) |])
 
-let mk_eq typ x y = mkApp (Lazy.force eq_ind, [| typ; x ; y |])
-let mk_eq_refl typ x = mkApp (Lazy.force eq_refl, [| typ; x |])
-let mk_JMeq typ x typ' y = mkApp (Lazy.force jmeq_ind, [| typ; x ; typ'; y |])
-let mk_JMeq_refl typ x = mkApp (Lazy.force jmeq_refl, [| typ; x |])
+let mk_eq typ x y = mkApp (delayed_force eq_ind, [| typ; x ; y |])
+let mk_eq_refl typ x = mkApp (delayed_force eq_refl, [| typ; x |])
+let mk_JMeq typ x typ' y = mkApp (delayed_force jmeq_ind, [| typ; x ; typ'; y |])
+let mk_JMeq_refl typ x = mkApp (delayed_force jmeq_refl, [| typ; x |])
 
 let unsafe_fold_right f = function
     hd :: tl -> List.fold_right f tl hd
   | [] -> raise (Invalid_argument "unsafe_fold_right")
 
 let mk_conj l =
-  let conj_typ = Lazy.force and_typ in
+  let conj_typ = delayed_force and_typ in
     unsafe_fold_right
       (fun c conj ->
 	 mkApp (conj_typ, [| c ; conj |]))
       l
 
 let mk_not c =
-  let notc = Lazy.force not_ref in
+  let notc = delayed_force not_ref in
     mkApp (notc, [| c |])
 
 let and_tac l hook =
@@ -336,7 +336,7 @@ let destruct_ex ext ex =
     match kind_of_term c with
 	App (f, args) ->
 	  (match kind_of_term f with
-	       Ind i when i = Term.destInd (Lazy.force ex_ind) && Array.length args = 2 ->
+	       Ind i when i = Term.destInd (delayed_force ex_ind) && Array.length args = 2 ->
 		 let (dom, rng) =
 		   try (args.(0), args.(1))
 		   with _ -> assert(false)
@@ -477,6 +477,7 @@ let pr_evar_map evd =
 
 let contrib_tactics_path =
   make_dirpath (List.map id_of_string ["Tactics";contrib_name;"Coq"])
+
 let tactics_tac s =
   lazy(make_kn (MPfile contrib_tactics_path) (make_dirpath []) (mk_label s))
 
diff --git a/plugins/subtac/subtac_utils.mli b/plugins/subtac/subtac_utils.mli
index d0ad334d3..f56c2932e 100644
--- a/plugins/subtac/subtac_utils.mli
+++ b/plugins/subtac/subtac_utils.mli
@@ -17,53 +17,53 @@ val contrib_name : string
 val subtac_dir : string list
 val fix_sub_module : string
 val fixsub_module : string list
-val init_constant : string list -> string -> constr
-val init_reference : string list -> string -> global_reference
-val fixsub : constr lazy_t
-val well_founded_ref : global_reference lazy_t
-val acc_ref : global_reference lazy_t
-val acc_inv_ref : global_reference lazy_t
-val fix_sub_ref : global_reference lazy_t
-val measure_on_R_ref : global_reference lazy_t
-val fix_measure_sub_ref : global_reference lazy_t
-val refl_ref : global_reference lazy_t
+val init_constant : string list -> string -> constr delayed
+val init_reference : string list -> string -> global_reference delayed
+val fixsub : constr delayed
+val well_founded_ref : global_reference delayed
+val acc_ref : global_reference delayed
+val acc_inv_ref : global_reference delayed
+val fix_sub_ref : global_reference delayed
+val measure_on_R_ref : global_reference delayed
+val fix_measure_sub_ref : global_reference delayed
+val refl_ref : global_reference delayed
 val lt_ref : reference
 val sig_ref : reference
 val proj1_sig_ref : reference
 val proj2_sig_ref : reference
 val build_sig : unit -> coq_sigma_data
-val sig_ : coq_sigma_data lazy_t
+val sig_ : coq_sigma_data delayed
 
-val fix_proto : constr lazy_t
+val fix_proto : constr delayed
 val fix_proto_ref : unit -> constant
 
-val eq_ind : constr lazy_t
-val eq_rec : constr lazy_t
-val eq_rect : constr lazy_t
-val eq_refl : constr lazy_t
-
-val not_ref : constr lazy_t
-val and_typ : constr lazy_t
-
-val eqdep_ind : constr lazy_t
-val eqdep_rec : constr lazy_t
-
-val jmeq_ind : constr lazy_t
-val jmeq_rec : constr lazy_t
-val jmeq_refl : constr lazy_t
-
-val boolind : constr lazy_t
-val sumboolind : constr lazy_t
-val natind : constr lazy_t
-val intind : constr lazy_t
-val existSind : constr lazy_t
-val existS : coq_sigma_data lazy_t
-val prod : coq_sigma_data lazy_t
-
-val well_founded : constr lazy_t
-val fix : constr lazy_t
-val acc : constr lazy_t
-val acc_inv : constr lazy_t
+val eq_ind : constr delayed
+val eq_rec : constr delayed
+val eq_rect : constr delayed
+val eq_refl : constr delayed
+
+val not_ref : constr delayed
+val and_typ : constr delayed
+
+val eqdep_ind : constr delayed
+val eqdep_rec : constr delayed
+
+val jmeq_ind : constr delayed
+val jmeq_rec : constr delayed
+val jmeq_refl : constr delayed
+
+val boolind : constr delayed
+val sumboolind : constr delayed
+val natind : constr delayed
+val intind : constr delayed
+val existSind : constr delayed
+val existS : coq_sigma_data delayed
+val prod : coq_sigma_data delayed
+
+val well_founded : constr delayed
+val fix : constr delayed
+val acc : constr delayed
+val acc_inv : constr delayed
 val extconstr : constr -> constr_expr
 val extsort : sorts -> constr_expr
 
@@ -81,7 +81,7 @@ val my_print_tycon_type : env -> type_constraint_type -> std_ppcmds
 val debug : int -> std_ppcmds -> unit
 val debug_msg : int -> std_ppcmds -> std_ppcmds
 val trace : std_ppcmds -> unit
-val wf_relations : (constr, constr lazy_t) Hashtbl.t
+val wf_relations : (constr, constr delayed) Hashtbl.t
 
 type binders = local_binder list
 val app_opt : ('a -> 'a) option -> 'a -> 'a