diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-04-09 10:13:28 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-04-09 10:13:28 +0000 |
| commit | 16ea6252339bed9901fff48b5883f4d471a88e7a (patch) | |
| tree | 92278fec909264b6c5eb6160c10d26b9893990d4 /pretyping | |
| parent | e2a8e020542e32b51ff5951d40bed3dad68c903d (diff) | |
Backtrack on 12061 (type checking for bug #2084 too strong as soon as we use
Type instead of sort variables for unknown levels in unification).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12075 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/unification.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 0b3eedcb8..217376acc 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -495,7 +495,8 @@ let unify_to_type env evd flags c u = let t = get_type_of env sigma c in let t = Tacred.hnf_constr env sigma (nf_betaiota sigma (nf_meta evd t)) in let u = Tacred.hnf_constr env sigma u in - unify_0 env sigma Cumul flags t u + try unify_0 env sigma Cumul flags t u + with e when precatchable_exception e -> ([],[]) let unify_type env evd flags mv c = let mvty = Typing.meta_type evd mv in |