diff options
| author | Matthieu Sozeau | 2014-04-07 12:53:41 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-06 09:58:58 +0200 |
| commit | 105db906ae45e792d1caeeb2e3fb7f69944b2caa (patch) | |
| tree | b12ca28e6b172d2524c6a11c851c7d568f6a2411 /pretyping/unification.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 'pretyping/unification.ml')
| -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 0ab886ca30..b1b2bc05b6 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -706,7 +706,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag else error_cannot_unify (fst curenvnb) sigma (cM,cN) and solve_canonical_projection curenvnb pb b cM f1l1 cN f2l2 (sigma,ms,es) = - let (ctx,c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) = + let (ctx,t,c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) = try Evarconv.check_conv_record f1l1 f2l2 with Not_found -> error_cannot_unify (fst curenvnb) sigma (cM,cN) in @@ -730,6 +730,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag substn params1 params in let (substn,_,_) = Reductionops.Stack.fold2 (unirec_rec curenvnb pb b false) substn ts ts1 in let app = mkApp (c, Array.rev_of_list ks) in + (* let substn = unirec_rec curenvnb pb b false substn t cN in *) unirec_rec curenvnb pb b false substn c1 app with Invalid_argument "Reductionops.Stack.fold2" -> error_cannot_unify (fst curenvnb) sigma (cM,cN) |