diff options
Diffstat (limited to 'interp/notation_ops.ml')
| -rw-r--r-- | interp/notation_ops.ml | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 81e2ac810..f4b74d62c 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -104,7 +104,7 @@ let glob_constr_of_notation_constr_with_binders loc g f e = function GRec (loc,fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl) | NCast (c,k) -> GCast (loc,f e c,Miscops.map_cast_type (f e) k) | NSort x -> GSort (loc,x) - | NHole (x, arg) -> GHole (loc, x, arg) + | NHole (x, naming, arg) -> GHole (loc, x, naming, arg) | NPatVar n -> GPatVar (loc,(false,n)) | NRef x -> GRef (loc,x,None) @@ -287,7 +287,7 @@ let notation_constr_and_vars_of_glob_constr a = NRec (fk,idl,dll,Array.map aux tl,Array.map aux bl) | GCast (_,c,k) -> NCast (aux c,Miscops.map_cast_type aux k) | GSort (_,s) -> NSort s - | GHole (_,w,arg) -> NHole (w, arg) + | GHole (_,w,naming,arg) -> NHole (w, naming, arg) | GRef (_,r,_) -> NRef r | GPatVar (_,(_,n)) -> NPatVar n | GEvar _ -> @@ -465,7 +465,7 @@ let rec subst_notation_constr subst bound raw = | NPatVar _ | NSort _ -> raw - | NHole (knd, solve) -> + | NHole (knd, naming, solve) -> let nknd = match knd with | Evar_kinds.ImplicitArg (ref, i, b) -> let nref, _ = subst_global subst ref in @@ -474,7 +474,7 @@ let rec subst_notation_constr subst bound raw = in let nsolve = Option.smartmap (Genintern.generic_substitute subst) solve in if nsolve == solve && nknd == knd then raw - else NHole (nknd, nsolve) + else NHole (nknd, naming, nsolve) | NCast (r1,k) -> let r1' = subst_notation_constr subst bound r1 in @@ -498,11 +498,11 @@ let abstract_return_type_context pi mklam tml rtno = let abstract_return_type_context_glob_constr = abstract_return_type_context (fun (_,_,nal) -> nal) (fun na c -> - GLambda(Loc.ghost,na,Explicit,GHole(Loc.ghost,Evar_kinds.InternalHole,None),c)) + GLambda(Loc.ghost,na,Explicit,GHole(Loc.ghost,Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None),c)) let abstract_return_type_context_notation_constr = abstract_return_type_context snd - (fun na c -> NLambda(na,NHole (Evar_kinds.InternalHole, None),c)) + (fun na c -> NLambda(na,NHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None),c)) exception No_match @@ -555,7 +555,7 @@ let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with | (_,Name id2) when Id.List.mem id2 (fst metas) -> let rhs = match na1 with | Name id1 -> GVar (Loc.ghost,id1) - | Anonymous -> GHole (Loc.ghost,Evar_kinds.InternalHole,None) in + | Anonymous -> GHole (Loc.ghost,Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None) in alp, bind_env alp sigma id2 rhs | (Name id1,Name id2) -> (id1,id2)::alp,sigma | (Anonymous,Anonymous) -> alp,sigma @@ -579,7 +579,7 @@ let rec match_iterated_binders islambda decls = function match_iterated_binders islambda ((na,bk,None,t)::decls) b | GLetIn (loc,na,c,b) when glue_letin_with_decls -> match_iterated_binders islambda - ((na,Explicit (*?*), Some c,GHole(loc,Evar_kinds.BinderType na,None))::decls) b + ((na,Explicit (*?*), Some c,GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None))::decls) b | b -> (decls,b) let remove_sigma x (sigmavar,sigmalist,sigmabinders) = @@ -733,7 +733,7 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 = to print "{x:_ & P x}" knowing that notation "{x & P x}" is not defined. *) | b1, NLambda (Name id,(NHole _ | NVar _ as t2),b2) when inner -> let id' = Namegen.next_ident_away id (free_glob_vars b1) in - let t1 = GHole(Loc.ghost,Evar_kinds.BinderType (Name id'),None) in + let t1 = GHole(Loc.ghost,Evar_kinds.BinderType (Name id'),Misctypes.IntroAnonymous,None) in let sigma = match t2 with | NHole _ -> sigma | NVar id2 -> bind_env alp sigma id2 t1 |