From bf13037e9ca39da28fb648e5488ce56ef8a1f1e2 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 17 Jan 2017 15:06:26 +0100
Subject: [location] Use located in misctypes.

---
 interp/smartlocate.ml | 6 +++---
 interp/stdarg.ml      | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'interp')

diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index d863e05616..64d260cc1b 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -66,16 +66,16 @@ let global_with_alias ?head r =
 let smart_global ?head = function
   | AN r ->
       global_with_alias ?head r
-  | ByNotation (loc,ntn,sc) ->
+  | ByNotation (loc,(ntn,sc)) ->
       Notation.interp_notation_as_global_reference loc (fun _ -> true) ntn sc
 
 let smart_global_inductive = function
   | AN r ->
       global_inductive_with_alias r
-  | ByNotation (loc,ntn,sc) ->
+  | ByNotation (loc,(ntn,sc)) ->
       destIndRef
         (Notation.interp_notation_as_global_reference loc isIndRef ntn sc)
 
 let loc_of_smart_reference = function
   | AN r -> loc_of_reference r
-  | ByNotation (loc,_,_) -> loc
+  | ByNotation (loc,(_,_)) -> loc
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index 341ff5662c..c0dd9e45c4 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -34,7 +34,7 @@ let wit_pre_ident : string uniform_genarg_type =
 
 let loc_of_or_by_notation f = function
   | AN c -> f c
-  | ByNotation (loc,s,_) -> loc
+  | ByNotation (loc,(s,_)) -> loc
 
 let wit_int_or_var =
   make0 ~dyn:(val_tag (topwit wit_int)) "int_or_var"
-- 
cgit v1.2.3