diff options
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/checkInductive.ml | 2 | ||||
| -rw-r--r-- | checker/dune | 1 |
2 files changed, 2 insertions, 1 deletions
diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml index d20eea7874..06ee4fcc7a 100644 --- a/checker/checkInductive.ml +++ b/checker/checkInductive.ml @@ -61,7 +61,7 @@ let to_entry (mb:mutual_inductive_body) : Entries.mutual_inductive_entry = mind_entry_params = mb.mind_params_ctxt; mind_entry_inds; mind_entry_universes; - mind_entry_variance = mb.mind_variance; + mind_entry_cumulative= Option.has_some mb.mind_variance; mind_entry_private = mb.mind_private; } diff --git a/checker/dune b/checker/dune index 73cbbc8d19..af7d4f2923 100644 --- a/checker/dune +++ b/checker/dune @@ -12,6 +12,7 @@ (executable (name coqchk) (public_name coqchk) + (modes exe byte) (package coq) (modules coqchk) (flags :standard -open Coq_checklib) |