diff options
| author | barras | 2004-09-15 16:50:56 +0000 |
|---|---|---|
| committer | barras | 2004-09-15 16:50:56 +0000 |
| commit | 2d707f4445c0cc86d8f8c30bdbe9eecf956997f9 (patch) | |
| tree | 9d6c2ff5489ba6bbf5683963108c34aa10b81e6f /interp/constrintern.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 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 03cd671aff..28f0de932a 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -625,7 +625,7 @@ let locate_if_isevar loc na = function (try match na with | Name id -> Reserve.find_reserved_type id | Anonymous -> raise Not_found - with Not_found -> RHole (loc, BinderType na)) + with Not_found -> RHole (loc, Evd.BinderType na)) | x -> x let check_hidden_implicit_parameters id (_,_,_,indnames,_) = @@ -669,8 +669,8 @@ let get_implicit_name n imps = else Some (Impargs.name_of_implicit (List.nth imps (n-1))) let set_hole_implicit i = function - | RRef (loc,r) -> (loc,ImplicitArg (r,i)) - | RVar (loc,id) -> (loc,ImplicitArg (VarRef id,i)) + | RRef (loc,r) -> (loc,Evd.ImplicitArg (r,i)) + | RVar (loc,id) -> (loc,Evd.ImplicitArg (VarRef id,i)) | _ -> anomaly "Only refs have implicits" let exists_implicit_name id = @@ -908,7 +908,7 @@ let internalise sigma env allow_soapp lvar c = let p' = option_app (intern_type env'') po in RIf (loc, c', (na', p'), intern env b1, intern env b2) | CHole loc -> - RHole (loc, QuestionMark) + RHole (loc, Evd.QuestionMark) | CPatVar (loc, n) when allow_soapp -> RPatVar (loc, n) | CPatVar (loc, (false,n)) when Options.do_translate () -> @@ -943,7 +943,7 @@ let internalise sigma env allow_soapp lvar c = (env,bl) nal | LocalRawDef((loc,na),def) -> ((name_fold Idset.add na ids,ts,sc), - (na,Some(intern env def),RHole(loc,BinderType na))::bl) + (na,Some(intern env def),RHole(loc,Evd.BinderType na))::bl) and intern_eqn n (ids,tmp_scope,scopes as env) (loc,lhs,rhs) = let idsl_pll = List.map (intern_cases_pattern scopes ([],[]) None) lhs in |