diff options
| author | Matthieu Sozeau | 2014-07-03 23:24:17 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-07-03 23:24:17 +0200 |
| commit | 7e4925b78162226331c65ef77f2da681a0b8ee48 (patch) | |
| tree | cd2dd3da8364319eee84d0335d8a8b7e5ce2ace3 /toplevel/command.ml | |
| parent | 84377c4d13418b0614d12a98a3f01421b52ac1e6 (diff) | |
Properly compute the transitive closure of the system of constraints
generated by a mutual inductive definition (bug found in CFGV). Actually this
code can move out of the kernel.
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 95ddf1fb06..4fc574daf5 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -390,7 +390,7 @@ let sup_list = List.fold_left Univ.sup Univ.type0m_univ let extract_level env evd tys = let sorts = List.map (fun ty -> let ctx, concl = Reduction.dest_prod_assum env ty in - sign_level env evd ctx) tys + sign_level env evd ((Anonymous, None, concl) :: ctx)) tys in sup_list sorts let inductive_levels env evdref poly arities inds = |