diff options
Diffstat (limited to 'checker/indtypes.ml')
| -rw-r--r-- | checker/indtypes.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/indtypes.ml b/checker/indtypes.ml index a667bb8a3..29b16392b 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -176,7 +176,7 @@ let typecheck_arity env params inds = (* Allowed eliminations *) let check_predicativity env s small level = - match s, fst (engagement env) with + match s, engagement env with Type u, _ -> (* let u' = fresh_local_univ () in *) (* let cst = *) |