diff options
| author | coqbot-app[bot] | 2020-11-17 13:26:45 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-17 13:26:45 +0000 |
| commit | 60f25e251ccdb13a80bd307e8955d6c672f9b76a (patch) | |
| tree | cb3645758702361fd847e4c6267a19508ed55630 /checker | |
| parent | 81ff5b8b3033edb97e51c00a73878745fed4ddcb (diff) | |
| parent | f3c24a6246249db25bcc5c4a3e34040a8667ca02 (diff) | |
Merge PR #12653: Syntax for specifying cumulative inductives
Reviewed-by: mattam82
Reviewed-by: maximedenes
Reviewed-by: jfehrle
Ack-by: gares
Ack-by: Zimmi48
Ack-by: ppedrot
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/checkInductive.ml | 3 | ||||
| -rw-r--r-- | checker/checker.ml | 4 |
2 files changed, 5 insertions, 2 deletions
diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml index 7bb714aa17..7513564cf0 100644 --- a/checker/checkInductive.ml +++ b/checker/checkInductive.ml @@ -69,6 +69,7 @@ let to_entry (mb:mutual_inductive_body) : Entries.mutual_inductive_entry = in let mind_entry_template = Array.exists check_template mb.mind_packets in let () = if mind_entry_template then assert (Array.for_all check_template mb.mind_packets) in + let mind_entry_variance = Option.map (Array.map (fun v -> Some v)) mb.mind_variance in { mind_entry_record; mind_entry_finite = mb.mind_finite; @@ -76,7 +77,7 @@ let to_entry (mb:mutual_inductive_body) : Entries.mutual_inductive_entry = mind_entry_inds; mind_entry_universes; mind_entry_template; - mind_entry_cumulative= Option.has_some mb.mind_variance; + mind_entry_variance; mind_entry_private = mb.mind_private; } diff --git a/checker/checker.ml b/checker/checker.ml index e2c90e2b93..08d92bb7b3 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -298,7 +298,9 @@ let explain_exn = function | DisallowedSProp -> str"DisallowedSProp" | BadRelevance -> str"BadRelevance" | BadInvert -> str"BadInvert" - | UndeclaredUniverse _ -> str"UndeclaredUniverse")) + | UndeclaredUniverse _ -> str"UndeclaredUniverse" + | BadVariance _ -> str "BadVariance" + )) | InductiveError e -> hov 0 (str "Error related to inductive types") |