diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-08-04 14:42:55 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-08-04 14:42:55 +0000 |
| commit | 726130d3d847e59d3556f6b302de155dc052d6a4 (patch) | |
| tree | 1a867c16ecfb46992dfc1ee76f7f1cb0b152249f /dev/include | |
| parent | cd411cddcd2f24c892146916e530635dda086d8d (diff) | |
Fix unification: detect invalid evar instantiations due to scoping earlier.
Add a debug printer for existential sets (used for frozen_evars in w_unify).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14384 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/include')
| -rw-r--r-- | dev/include | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/dev/include b/dev/include index 5d4872273..705e8e375 100644 --- a/dev/include +++ b/dev/include @@ -28,6 +28,7 @@ #install_printer (* Goal.goal *) ppgoalgoal;; #install_printer (* metaset.t *) ppmetas;; #install_printer (* evar_map *) ppevm;; +#install_printer (* ExistentialSet.t *) ppexistentialset;; #install_printer (* clenv *) ppclenv;; #install_printer (* env *) ppenv;; |