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

(limited to 'printing/ppconstr.ml')

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index a389ee1752..39f91b795a 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -17,7 +17,6 @@ open Pputils
 open Ppextend
 open Constrexpr
 open Constrexpr_ops
-open Topconstr
 open Decl_kinds
 open Misctypes
 open Locus
@@ -309,7 +308,8 @@ let split_lambda = function
 
 let rename na na' t c =
   match (na,na') with
-    | (_,Name id), (_,Name id') -> (na',t,replace_vars_constr_expr [id,id'] c)
+    | (_,Name id), (_,Name id') ->
+      (na',t,Topconstr.replace_vars_constr_expr [id,id'] c)
     | (_,Name id), (_,Anonymous) -> (na,t,c)
     | _ -> (na',t,c)
 
-- 
cgit v1.2.3