diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-04-07 12:53:41 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:58:58 +0200 |
| commit | 105db906ae45e792d1caeeb2e3fb7f69944b2caa (patch) | |
| tree | b12ca28e6b172d2524c6a11c851c7d568f6a2411 /proofs/clenvtac.ml | |
| parent | b17c1e128fad2e84ebe4e4742b47bd67d88c56d6 (diff) | |
- Fixes for canonical structure resolution (check that the initial term indeed unifies
with the projected term, keeping track of universes).
- Fix the [unify] tactic to fail properly.
- Fix unification to disallow lowering a global Type(i) universe to Prop or Set.
Diffstat (limited to 'proofs/clenvtac.ml')
| -rw-r--r-- | proofs/clenvtac.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 112402bca..6873bbb11 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -107,8 +107,11 @@ let fail_quick_unif_flags = { let unifyTerms ?(flags=fail_quick_unif_flags) m n gls = let env = pf_env gls in let evd = create_goal_evar_defs (project gls) in - let evd' = w_unify env evd CONV ~flags m n in - tclIDTAC {it = gls.it; sigma = evd'; } + try + let evd' = w_unify env evd CONV ~flags m n in + tclIDTAC {it = gls.it; sigma = evd'; } + with e when Errors.noncritical e -> + tclFAIL 0 (Errors.print e) gls let unify ?(flags=fail_quick_unif_flags) m gls = let n = pf_concl gls in unifyTerms ~flags m n gls |