From be83b52cf50ed4c596e40cfd52da03258a7a4a18 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 16 Jan 2017 13:22:42 +0100
Subject: [location] Move Glob_term.predicate_pattern to located.

We continue the uniformization pass. No big news here, trying to be
minimally invasive.
---
 interp/notation_ops.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'interp/notation_ops.ml')

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))
 
-- 
cgit v1.2.3