diff options
| author | barras | 2005-11-18 20:10:45 +0000 |
|---|---|---|
| committer | barras | 2005-11-18 20:10:45 +0000 |
| commit | d677987add1acff62543c658f994476a06374c41 (patch) | |
| tree | 760704166b4a425fd7deb74aed5d5bb7e5754cf5 /kernel | |
| parent | 89df70511ac211f47a1aa29a21622103eff3b1c2 (diff) | |
petites corrections + contournement bug projections
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7585 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/closure.ml | 10 | ||||
| -rw-r--r-- | kernel/closure.mli | 4 |
2 files changed, 6 insertions, 8 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml index 577ea5cb24..b791687855 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -532,6 +532,8 @@ let fterm_of v = v.term let set_norm v = v.norm <- Norm let is_val v = v.norm = Norm +let mk_atom c = {norm=Norm;term=FAtom c} + (* Could issue a warning if no is still Red, pointing out that we loose sharing. *) let update v1 (no,t) = @@ -546,7 +548,7 @@ let update v1 (no,t) = when the lift is 0. *) let rec lft_fconstr n ft = match ft.term with - | (FInd _|FConstruct _|FFlex(ConstKey _|VarKey _)|FAtom _) -> ft + | (FInd _|FConstruct _|FFlex(ConstKey _|VarKey _)) -> ft | FRel i -> {norm=Norm;term=FRel(i+n)} | FLambda(k,tys,f,e) -> {norm=Cstr; term=FLambda(k,tys,f,subs_shft(n,e))} | FFix(fx,e) -> {norm=Cstr; term=FFix(fx,subs_shft(n,e))} @@ -725,11 +727,7 @@ let rec to_constr constr_fun lfts v = | FRel i -> mkRel (reloc_rel i lfts) | FFlex (RelKey p) -> mkRel (reloc_rel p lfts) | FFlex (VarKey x) -> mkVar x - | FAtom c -> - (match kind_of_term c with - | Sort s -> mkSort s - | Meta m -> mkMeta m - | _ -> assert false) + | FAtom c -> exliftn lfts c | FCast (a,b) -> mkCast (constr_fun lfts a, constr_fun lfts b) | FFlex (ConstKey op) -> mkConst op diff --git a/kernel/closure.mli b/kernel/closure.mli index 0882758576..e394b15b8b 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -155,8 +155,8 @@ val fterm_of : fconstr -> fterm val term_of_fconstr : fconstr -> constr val destFLambda : (fconstr subs -> constr -> fconstr) -> fconstr -> name * fconstr * fconstr -(* prevents a term from being evaluated *) -val set_norm : fconstr -> unit +(* mk_atom: prevents a term from being evaluated *) +val mk_atom : constr -> fconstr (* Global and local constant cache *) type clos_infos |