From 79b6291ccda61f631aa2cfec9a12d6ea2a34fa96 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 13 Mar 2013 18:01:16 +0000
Subject: Modules and ppvernac, sequel of Enrico's commit 16261

 After some investigation, I see no reason to try to hack
 the nametab in ppvernac, since everything happens there
 at a lower level (constr_expr). So the offending code that
 Enrico protected with a State.with_state_protection is now gone.

 By the way, moved some types from Declaremods to Vernacexpr
 to avoid some dependencies

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16300 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/topconstr.mli | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

(limited to 'interp')

diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 6cc3615f06..3561896433 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -7,12 +7,8 @@
 (************************************************************************)
 
 open Loc
-open Pp
 open Names
 open Libnames
-open Glob_term
-open Term
-open Mod_subst
 open Misctypes
 open Decl_kinds
 open Constrexpr
@@ -22,7 +18,7 @@ open Notation_term
 
 val oldfashion_patterns : bool ref
 
-(** Utilities on constr_expr                                           *)
+(** Utilities on constr_expr *)
 
 val replace_vars_constr_expr :
   (Id.t * Id.t) list -> constr_expr -> constr_expr
-- 
cgit v1.2.3