From 392300a73bc4e57d2be865d9a8d77c608ef02f59 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 29 May 2012 11:08:50 +0000
Subject: New files intf/constrexpr.mli and intf/notation_term.mli out of
 Topconstr

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15375 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/syntax_def.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'interp/syntax_def.ml')

diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index eb6f50131f..f20d9727d8 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -11,7 +11,7 @@ open Util
 open Pp
 open Names
 open Libnames
-open Topconstr
+open Notation_term
 open Libobject
 open Lib
 open Nameops
@@ -38,7 +38,7 @@ let load_syntax_constant i ((sp,kn),(local,pat,onlyparse)) =
   Nametab.push_syndef (Nametab.Until i) sp kn
 
 let is_alias_of_already_visible_name sp = function
-  | _,ARef ref ->
+  | _,NRef ref ->
       let (dir,id) = repr_qualid (shortest_qualid_of_global Idset.empty ref) in
       dir = empty_dirpath && id = basename sp
   | _ ->
@@ -58,7 +58,7 @@ let cache_syntax_constant d =
   open_syntax_constant 1 d
 
 let subst_syntax_constant (subst,(local,pat,onlyparse)) =
-  (local,subst_interpretation subst pat,onlyparse)
+  (local,Topconstr.subst_interpretation subst pat,onlyparse)
 
 let classify_syntax_constant (local,_,_ as o) =
   if local then Dispose else Substitute o
@@ -71,7 +71,7 @@ let in_syntax_constant : bool * interpretation * bool -> obj =
     subst_function = subst_syntax_constant;
     classify_function = classify_syntax_constant }
 
-type syndef_interpretation = (identifier * subscopes) list * aconstr
+type syndef_interpretation = (identifier * subscopes) list * notation_constr
 
 (* Coercions to the general format of notation that also supports
    variables bound to list of expressions *)
-- 
cgit v1.2.3