diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-30 19:43:44 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-30 19:43:44 +0000 |
| commit | 4f70016289f15526b162582fc267374e2b60448e (patch) | |
| tree | 47abfac4e62dfe1dc5dcfad34050634480518709 /plugins/subtac/subtac_cases.ml | |
| parent | 13e53564fdc4beb14bd04612214a648630549417 (diff) | |
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
Diffstat (limited to 'plugins/subtac/subtac_cases.ml')
| -rw-r--r-- | plugins/subtac/subtac_cases.ml | 14 |
1 files changed, 6 insertions, 8 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 |]) :: |