diff options
| author | Matthieu Sozeau | 2014-04-01 19:19:22 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-06 09:58:58 +0200 |
| commit | a2fce6d14d00a437466a1f7e3b53a77229f87980 (patch) | |
| tree | 2e88133b978c67c222f0bfd7c13416609cdc84ac /pretyping/unification.ml | |
| parent | 4d7956a9b3f7f44aa9dae1bf22258b12dacab65f (diff) | |
- Fix eq_constr_universes restricted to Sorts.equal
- Fix passing of universe contexts through definitions/proofs, abstract is ok now, even
in presence of polymorphism
- Correctly mark unresolvable the evars made by the Simple abstraction.
Diffstat (limited to 'pretyping/unification.ml')
| -rw-r--r-- | pretyping/unification.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 9e662150ee..0ab886ca30 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -384,6 +384,7 @@ let is_rigid_head flags t = match kind_of_term t with | Const (cst,u) -> not (Cpred.mem cst (snd flags.modulo_delta)) | Ind (i,u) -> true + | Fix _ | CoFix _ -> true | _ -> false let force_eqs c = |