diff options
| author | msozeau | 2011-06-08 08:30:42 +0000 |
|---|---|---|
| committer | msozeau | 2011-06-08 08:30:42 +0000 |
| commit | 2d7c366bc0392bc68d622f4c0dc6734a2dc9ed6c (patch) | |
| tree | 0be4b93e77a0309d3c2dce64ce27ebed13e9a87e /dev/header | |
| parent | aaf608630f8ae0ed9cfb4731bff0bd114cafc430 (diff) | |
Fixes in pruning in unification.
Properly normalize evars to reflect the already pruned evars in the type
of dependent evars to allow more precise restriction of hyps.
Directly check the type of an evar instance, allowing backtracking on
ill-typed instanciations.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14169 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/header')
0 files changed, 0 insertions, 0 deletions