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 /pretyping/unification.mli | |
| 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 'pretyping/unification.mli')
| -rw-r--r-- | pretyping/unification.mli | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 37eaa5802..cc781c871 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -66,3 +66,12 @@ val w_merge : env -> bool -> unify_flags -> evar_map * (metavariable * constr * (instance_constraint * instance_typing_status)) list * (env * types pexistential * types) list -> evar_map +val unify_0 : Environ.env -> + Evd.evar_map -> + Evd.conv_pb -> + unify_flags -> + Term.types -> + Term.types -> + Evd.evar_map * Evd.metabinding list * + (Environ.env * Term.types Term.pexistential * Term.constr) list + |