diff options
| author |  puech <puech@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-08-08 08:46:34 +0000 |
|---|---|---|
| committer | puech <puech@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-08-08 08:46:34 +0000 |
| commit | 59462251fec623636b3a5396253e38f6d29bf747 (patch) | |
| tree | c23d7dff6718ce6e2211e719485f284f3bc8dd00 /checker | |
| parent | ca6b6bfde9a0c5b91a53e9c139140403369ff658 (diff) | |
Esubst: make types of substitutions & lifts private
Allows to be sure that we apply the smart constructors.
Propagate the change to Closure, Reduction, Term, Cbv and Newring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14386 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/closure.ml | 6 | ||||
| -rw-r--r-- | checker/reduction.ml | 2 | ||||
| -rw-r--r-- | checker/term.ml | 2 |
3 files changed, 5 insertions, 5 deletions
diff --git a/checker/closure.ml b/checker/closure.ml index 2227e392e..033e2bd73 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -428,7 +428,7 @@ let optimise_closure env c = let (c',(_,s)) = compact_constr (0,[]) c 1 in let env' = Array.map (fun i -> clos_rel env i) (Array.of_list s) in - (subs_cons (env', ESID 0),c') + (subs_cons (env', subs_id 0),c') let mk_lambda env t = let (env,t) = optimise_closure env t in @@ -559,7 +559,7 @@ let term_of_fconstr = | FFix(fx,e) when is_subs_id e & is_lift_id lfts -> Fix fx | FCoFix(cfx,e) when is_subs_id e & is_lift_id lfts -> CoFix cfx | _ -> to_constr term_of_fconstr_lift lfts v in - term_of_fconstr_lift ELID + term_of_fconstr_lift el_id @@ -806,7 +806,7 @@ let kh info v stk = fapp_stack(kni info v stk) let whd_val info v = with_stats (lazy (term_of_fconstr (kh info v []))) -let inject = mk_clos (ESID 0) +let inject = mk_clos (subs_id 0) let whd_stack infos m stk = let k = kni infos m stk in diff --git a/checker/reduction.ml b/checker/reduction.ml index efeaff07f..3aeaa1023 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -372,7 +372,7 @@ and convert_vect univ infos lft1 lft2 v1 v2 = let clos_fconv cv_pb env t1 t2 = let infos = create_clos_infos betaiotazeta env in let univ = universes env in - ccnv univ cv_pb infos ELID ELID (inject t1) (inject t2) + ccnv univ cv_pb infos el_id el_id (inject t1) (inject t2) let fconv cv_pb env t1 t2 = if eq_constr t1 t2 then () diff --git a/checker/term.ml b/checker/term.ml index 7d2241228..ab40b6fa7 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -261,7 +261,7 @@ let rec exliftn el c = match c with (* Lifting the binding depth across k bindings *) let liftn k n = - match el_liftn (pred n) (el_shft k ELID) with + match el_liftn (pred n) (el_shft k el_id) with | ELID -> (fun c -> c) | el -> exliftn el |