diff options
-rw-r--r-- | interp/coqlib.ml | 3 | ||||
-rw-r--r-- | interp/coqlib.mli | 6 | ||||
-rw-r--r-- | lib/util.ml | 6 | ||||
-rw-r--r-- | lib/util.mli | 6 | ||||
-rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 1 | ||||
-rw-r--r-- | plugins/funind/recdef.ml | 2 | ||||
-rw-r--r-- | plugins/subtac/subtac_cases.ml | 14 | ||||
-rw-r--r-- | plugins/subtac/subtac_coercion.ml | 20 | ||||
-rw-r--r-- | plugins/subtac/subtac_command.ml | 12 | ||||
-rw-r--r-- | plugins/subtac/subtac_pretyping_F.ml | 2 | ||||
-rw-r--r-- | plugins/subtac/subtac_utils.ml | 127 | ||||
-rw-r--r-- | plugins/subtac/subtac_utils.mli | 80 |
12 files changed, 142 insertions, 137 deletions
diff --git a/interp/coqlib.ml b/interp/coqlib.ml index 54a1d6149..76a4cf88a 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -180,14 +180,11 @@ type coq_bool_data = { andb_prop : constr; andb_true_intro : constr} -type 'a delayed = unit -> 'a - let build_bool_type () = { andb = init_constant ["Datatypes"] "andb"; andb_prop = init_constant ["Datatypes"] "andb_prop"; andb_true_intro = init_constant ["Datatypes"] "andb_true_intro" } - let build_sigma_set () = anomaly "Use build_sigma_type" let build_sigma_type () = diff --git a/interp/coqlib.mli b/interp/coqlib.mli index 73427d902..c4693479b 100644 --- a/interp/coqlib.mli +++ b/interp/coqlib.mli @@ -11,6 +11,7 @@ open Libnames open Nametab open Term open Pattern +open Util (** This module collects the global references, constructions and patterns of the standard library used in ocaml files *) @@ -84,9 +85,8 @@ val glob_jmeq : global_reference at compile time. Therefore, we can only provide methods to build them at runtime. This is the purpose of the [constr delayed] and [constr_pattern delayed] types. Objects of this time needs to be - applied to [()] to get the actual constr or pattern at runtime *) - -type 'a delayed = unit -> 'a + forced with [delayed_force] to get the actual constr or pattern + at runtime. *) type coq_bool_data = { andb : constr; diff --git a/lib/util.ml b/lib/util.ml index ad48e7981..2711eee24 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -1179,6 +1179,12 @@ let iterate_for a b f x = let rec iterate i v = if i > b then v else iterate (succ i) (f i v) in iterate a x +(* Delayed computations *) + +type 'a delayed = unit -> 'a + +let delayed_force f = f () + (* Misc *) type ('a,'b) union = Inl of 'a | Inr of 'b diff --git a/lib/util.mli b/lib/util.mli index f8fbc1f68..bbef3462a 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -291,6 +291,12 @@ val iterate : ('a -> 'a) -> int -> 'a -> 'a val repeat : int -> ('a -> unit) -> 'a -> unit val iterate_for : int -> int -> (int -> 'a -> 'a) -> 'a -> 'a +(** {6 Delayed computations. } *) + +type 'a delayed = unit -> 'a + +val delayed_force : 'a delayed -> 'a + (** {6 Misc. } *) type ('a,'b) union = Inl of 'a | Inr of 'b diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 361df3d1c..4f96ce06e 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1345,7 +1345,6 @@ and acc_inv_id = Recdef.acc_inv_id and ltof_ref = Recdef.ltof_ref and acc_rel = Recdef.acc_rel and well_founded = Recdef.well_founded -and delayed_force = Recdef.delayed_force and h_intros = Recdef.h_intros and list_rewrite = Recdef.list_rewrite and evaluable_of_global_reference = Recdef.evaluable_of_global_reference diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index fe6402db7..be2c24602 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -286,8 +286,6 @@ let find_reference sl s = (List.map id_of_string (List.rev sl))) (id_of_string s)));; -let delayed_force f = f () - let le_lt_SS = function () -> (constant ["Recdef"] "le_lt_SS") let le_lt_n_Sm = function () -> (coq_base_constant "le_lt_n_Sm") 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 |