diff options
| author | Matthieu Sozeau | 2014-04-07 19:21:05 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-06 09:58:59 +0200 |
| commit | 4cb7fe525a472928aee02d772458d28a2b71072a (patch) | |
| tree | 5934260488727e9c06871ce775376535c252f721 /tactics | |
| parent | 2d6de8b102ea3cd05c5d193190faf787ccb84baa (diff) | |
- Fix arity handling in retyping (de Bruijn bug!)
- Enforce that no u <= Prop/Set can be added for u introduced by the user in Evd.process_constraints.
(Needs to be enforced in the kernel as well, but that's the main entry point).
- Fix a test-suite script and remove a regression comment, it's just as before now.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/rewrite.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index c6c4049923..dc9cc471c2 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -633,12 +633,12 @@ let unify_eqn env (sigma, cstrs) hypinfo by t = and ty2 = Typing.type_of env'.env env'.evd c2 in if convertible env env'.evd ty1 ty2 then - (if occur_meta_or_existential prf then + (* (if occur_meta_or_existential prf then *) (hypinfo := refresh_hypinfo env env'.evd !hypinfo; env'.evd, prf, c1, c2, car, rel) - else (** Evars have been solved, we can go back to the initial evd, - but keep the potential refinement of existing evars. *) - env'.evd, prf, c1, c2, car, rel) + (* else (\** Evars have been solved, we can go back to the initial evd, *) + (* but keep the potential refinement of existing evars. *\) *) + (* env'.evd, prf, c1, c2, car, rel) *) else raise Reduction.NotConvertible in let evars = evd', Evar.Set.empty in |