diff options
| author | Gaëtan Gilbert | 2020-07-07 14:25:20 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-11-16 11:12:44 +0100 |
| commit | 9990bea3e163850c0ac4dca982c73d2b2bc19a38 (patch) | |
| tree | 28d9ddc1dec90446dbbbcfb448dcce80862431a8 /checker | |
| parent | 779d2b915a970cdfc87d3d1b69e10bab04094f33 (diff) | |
Infrastructure for cumulative inductive syntax (no grammar extension yet)
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") |