diff options
| author | herbelin | 2012-01-27 22:07:57 +0000 |
|---|---|---|
| committer | herbelin | 2012-01-27 22:07:57 +0000 |
| commit | 0bfefe15d6c174c60cc0eb50a54254c20228f30e (patch) | |
| tree | 0593e4f0fd310a47e74fc47757d706ff2be93d51 /pretyping | |
| parent | c51a32a5f3825dfd78212c976fb0d2d62b4e7d71 (diff) | |
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
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/namegen.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |