From 255f7938cf92216bc134099c50bd8258044be644 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 29 May 2012 11:09:05 +0000
Subject: Strongly reduce the dependencies of grammar.cma, modulo two hacks

 - in g_constr.ml4, we avoid a dependency on Notation_ops by copying
   the pseudo-ident hack ldots_var = ".."

 - in egrammar.ml4 we duplicate the error message
   error_invalid_pattern_notaition.
   To adapt via Errors.register_handler...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15383 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/base_include | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'dev/base_include')

diff --git a/dev/base_include b/dev/base_include
index 38a5972e96..a0c4928f62 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -13,6 +13,7 @@
 #directory "proofs";;
 #directory "tactics";;
 #directory "translate";;
+#directory "intf";;
 
 #directory "+camlp4";; (* lazy solution: add both of camlp4/5 so that *)
 #directory "+camlp5";; (* Gramext is found in top_printers.ml *)
@@ -68,6 +69,7 @@ open Library
 
 open Cases
 open Pattern
+open Patternops
 open Cbv
 open Classops
 open Pretyping
@@ -76,6 +78,7 @@ open Classops
 open Clenv
 open Clenvtac
 open Glob_term
+open Glob_ops
 open Coercion
 open Recordops
 open Detyping
@@ -102,7 +105,11 @@ open Notation
 open Ppextend
 open Reserve
 open Syntax_def
+open Constrexpr
+open Constrexpr_ops
 open Topconstr
+open Notation_term
+open Notation_ops
 open Prettyp
 open Search
 
-- 
cgit v1.2.3