diff options
| author | Matthieu Sozeau | 2014-06-04 15:42:41 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-04 15:48:32 +0200 |
| commit | 2ac8e0edebe0d9a6bde4d997327dbd2ffcde08b6 (patch) | |
| tree | b144dcb1689899b5135289903932b18de55d9904 /pretyping | |
| parent | 86c6649382bb9e42281ffe956c627c6d3987559b (diff) | |
- Allow parsing of @const@{instance} for specifying universe instances of polymorphic
constants.
Diffstat (limited to 'pretyping')
| -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 2b3e943559..4936ba4264 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -386,6 +386,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 + | Construct _ -> true | Fix _ | CoFix _ -> true | _ -> false |