diff options
| author | Emilio Jesus Gallego Arias | 2017-01-16 13:22:42 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-04-24 23:58:23 +0200 |
| commit | be83b52cf50ed4c596e40cfd52da03258a7a4a18 (patch) | |
| tree | 92e1e62378d2274751ab46673e2ee56fe4f65999 /interp/notation_ops.ml | |
| parent | ad3aab9415b98a247a6cbce05752632c3c42391c (diff) | |
[location] Move Glob_term.predicate_pattern to located.
We continue the uniformization pass. No big news here, trying to be
minimally invasive.
Diffstat (limited to 'interp/notation_ops.ml')
| -rw-r--r-- | interp/notation_ops.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 29f42d0e9e..a25fd81f32 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -179,7 +179,7 @@ let glob_constr_of_notation_constr_with_binders loc g f e = function | Some (ind,nal) -> let e',nal' = List.fold_right (fun na (e',nal) -> let e',na' = g e' na in e',na'::nal) nal (e',[]) in - e',Some (loc,ind,nal') in + e',Some (loc,(ind,nal')) in let e',na' = g e' na in (e',(f e tm,(na',t'))::tml')) tml (e,[]) in let fold (idl,e) na = let (e,na) = g e na in ((name_cons na idl,e),na) in @@ -356,8 +356,8 @@ let notation_constr_and_vars_of_glob_constr a = List.map (fun (tm,(na,x)) -> add_name found na; Option.iter - (fun (_,_,nl) -> List.iter (add_name found) nl) x; - (aux tm,(na,Option.map (fun (_,ind,nal) -> (ind,nal)) x))) tml, + (fun (_,(_,nl)) -> List.iter (add_name found) nl) x; + (aux tm,(na,Option.map (fun (_,(ind,nal)) -> (ind,nal)) x))) tml, List.map f eqnl) | GLetTuple (loc,nal,(na,po),b,c) -> add_name found na; @@ -589,7 +589,7 @@ let abstract_return_type_context pi mklam tml rtno = rtno let abstract_return_type_context_glob_constr = - abstract_return_type_context (fun (_,_,nal) -> nal) + abstract_return_type_context (fun (_,(_,nal)) -> nal) (fun na c -> GLambda(Loc.ghost,na,Explicit,GHole(Loc.ghost,Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None),c)) |