diff options
| author | Matthieu Sozeau | 2020-12-01 08:57:54 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2020-12-01 08:57:54 +0100 |
| commit | 36e2df30d23d56f0a80adcd3ed5c04d64117af74 (patch) | |
| tree | 4d0b70137e9ac2ac239413c48078d5f125431246 /kernel/inductive.ml | |
| parent | 0af89e4c04b1ecf437a86b50a34a17eddee56b76 (diff) | |
Use ~l2r:true to restore previous order of unfolding when typing predicates of cases.
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 2c0865348e..83e31a1881 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -337,7 +337,7 @@ let check_correct_arity env c pj ind specif params = match ar, kind pt' with | (LocalAssum (_,a1))::ar', Prod (na1,a1',t) -> let () = - try conv_leq env a1 a1' + try conv_leq ~l2r:true env a1 a1' with NotConvertible -> raise (LocalArity None) in srec (push_rel (LocalAssum (na1,a1)) env) ar' t (* The last Prod domain is the type of the scrutinee *) @@ -351,7 +351,7 @@ let check_correct_arity env c pj ind specif params = let () = (* This ensures that the type of the scrutinee is <= the inductive type declared in the predicate. *) - try conv_leq env dep_ind a1' + try conv_leq ~l2r:true env dep_ind a1' with NotConvertible -> raise (LocalArity None) in let () = check_allowed_sort ksort specif in |