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/constrextern.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'interp/constrextern.ml')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 62b8cdcea8..299ea8d792 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -21,6 +21,8 @@ open Sign
 open Environ
 open Libnames
 open Impargs
+open Constrexpr
+open Notation_term
 open Topconstr
 open Glob_term
 open Glob_ops
@@ -456,7 +458,7 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
       match t with
 	| PatCstr (loc,_,_,na) ->
 	  let p = apply_notation_to_pattern loc
-	    (match_aconstr_cases_pattern t pat) allscopes vars keyrule in
+	    (match_notation_constr_cases_pattern t pat) allscopes vars keyrule in
 	  insert_pat_alias loc p na
 	| PatVar (loc,Anonymous) -> CPatAtom (loc, None)
 	| PatVar (loc,Name id) -> CPatAtom (loc, Some (Ident (loc,id)))
@@ -910,7 +912,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
           | _ -> raise No_match in
 	(* Try matching ... *)
 	let terms,termlists,binders =
-          match_aconstr !print_universes t pat in
+          match_notation_constr !print_universes t pat in
 	(* Try availability of interpretation ... *)
         let e =
           match keyrule with
-- 
cgit v1.2.3