diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-01-27 22:07:57 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-01-27 22:07:57 +0000 |
| commit | 0bfefe15d6c174c60cc0eb50a54254c20228f30e (patch) | |
| tree | 0593e4f0fd310a47e74fc47757d706ff2be93d51 /theories/Program | |
| 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 'theories/Program')
0 files changed, 0 insertions, 0 deletions