diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-09-15 16:50:56 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-09-15 16:50:56 +0000 |
| commit | 2d707f4445c0cc86d8f8c30bdbe9eecf956997f9 (patch) | |
| tree | 9d6c2ff5489ba6bbf5683963108c34aa10b81e6f /pretyping/pretyping.ml | |
| parent | 8f5a7bbf2e5c64d6badd9e7c39da83d07b9c6f40 (diff) | |
hiding the meta_map in evar_defs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6109 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index d0402a552..0054c4770 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -276,7 +276,7 @@ let rec pretype tycon env isevars lvar = function | RHole (loc,k) -> (match tycon with | Some ty -> - { uj_val = e_new_isevar isevars env (loc,k) ty; uj_type = ty } + { uj_val = e_new_evar isevars env ~src:(loc,k) ty; uj_type = ty } | None -> error_unsolvable_implicit loc env (evars_of !isevars) k) | RRec (loc,fixkind,names,bl,lar,vdef) -> @@ -391,7 +391,7 @@ let rec pretype tycon env isevars lvar = function | RLetIn(loc,name,c1,c2) -> let j = pretype empty_tycon env isevars lvar c1 in - let t = Evarutil.refresh_universes j.uj_type in + let t = refresh_universes j.uj_type in let var = (name,Some j.uj_val,t) in let tycon = option_app (lift 1) tycon in let j' = pretype tycon (push_rel var env) isevars lvar c2 in @@ -529,7 +529,7 @@ let rec pretype tycon env isevars lvar = function Cases.pred_case_ml env (evars_of !isevars) false indt (0,fj.uj_type) in - if has_undefined_isevars !isevars pred then + if has_undefined_evars !isevars pred then use_constraint () else true, pred @@ -683,7 +683,8 @@ let rec pretype tycon env isevars lvar = function | None -> let p = match tycon with | Some ty -> ty - | None -> e_new_isevar isevars env (loc,InternalHole) (new_Type ()) + | None -> + e_new_evar isevars env ~src:(loc,InternalHole) (new_Type ()) in it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in let f cs b = @@ -750,7 +751,7 @@ let rec pretype tycon env isevars lvar = function let pred = Cases.pred_case_ml (* eta-expanse *) env (evars_of !isevars) isrec indt (i,fj.uj_type) in - if has_undefined_isevars !isevars pred then findtype (i+1) + if has_undefined_evars !isevars pred then findtype (i+1) else let pty = Retyping.get_type_of env (evars_of !isevars) pred in @@ -942,7 +943,7 @@ and pretype_type valcon env isevars lvar = function utj_type = s } | None -> let s = new_Type_sort () in - { utj_val = e_new_isevar isevars env loc (mkSort s); + { utj_val = e_new_evar isevars env ~src:loc (mkSort s); utj_type = s}) | c -> let j = pretype empty_tycon env isevars lvar c in |