From 0bfefe15d6c174c60cc0eb50a54254c20228f30e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 27 Jan 2012 22:07:57 +0000
Subject: Printing bugs with match patterns: - namegen.ml: if a matching
 variable has the same name as a constructor,   rename it, even if the
 conflicting constructor name is defined in a   different module; -
 constrextern.ml: protect code for printing cases as terms are from  
 requesting info in the global env when printers are called from ocamldebug  
 since the global env is undefined in this situation.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14947 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/namegen.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml
index 2ad2f3515c..abb6b510d1 100644
--- a/pretyping/namegen.ml
+++ b/pretyping/namegen.ml
@@ -53,7 +53,7 @@ let is_global id =
 let is_constructor id =
   try
     match locate (qualid_of_ident id) with
-      | ConstructRef _ as ref -> not (is_imported_ref ref)
+      | ConstructRef _ -> true
       | _ -> false
   with Not_found ->
     false
-- 
cgit v1.2.3