diff options
| author | Pierre-Marie Pédrot | 2019-09-02 08:56:59 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-09-02 08:56:59 +0200 |
| commit | 083e83a2e82c17c13b5af7d59029d4ef0aa1b613 (patch) | |
| tree | 7609e9b92c93fe21603aaa2f7d90805e30812f53 /printing/printer.ml | |
| parent | 1f74267d7e4affe14dbafc1a6f1e6f3f465f75a8 (diff) | |
| parent | 24a9a9c4bef18133c0b5070992d3396ff7596a7c (diff) | |
Merge PR #9918: Fix #9294: critical bug with template polymorphism
Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: herbelin
Ack-by: mattam82
Reviewed-by: ppedrot
Diffstat (limited to 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index e3225fadd5..328082fbc2 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -854,6 +854,8 @@ type axiom = | Constant of Constant.t (* An axiom or a constant. *) | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *) | Guarded of GlobRef.t (* a constant whose (co)fixpoints have been assumed to be guarded *) + | TemplatePolymorphic of MutInd.t (* A mutually inductive definition whose template polymorphism + on parameter universes has not been checked. *) | TypeInType of GlobRef.t (* a constant which relies on type in type *) type context_object = @@ -873,10 +875,13 @@ struct Constant.CanOrd.compare k1 k2 | Positive m1 , Positive m2 -> MutInd.CanOrd.compare m1 m2 + | TemplatePolymorphic m1, TemplatePolymorphic m2 -> + MutInd.CanOrd.compare m1 m2 | Guarded k1 , Guarded k2 -> GlobRef.Ordered.compare k1 k2 | _ , Constant _ -> 1 | _ , Positive _ -> 1 + | _, TemplatePolymorphic _ -> 1 | _ -> -1 let compare x y = @@ -937,6 +942,9 @@ let pr_assumptionset env sigma s = hov 2 (safe_pr_inductive env m ++ spc () ++ strbrk"is assumed to be positive.") | Guarded gr -> hov 2 (safe_pr_global env gr ++ spc () ++ strbrk"is assumed to be guarded.") + | TemplatePolymorphic m -> + hov 2 (safe_pr_inductive env m ++ spc () ++ + strbrk"is assumed template polymorphic on all its universe parameters.") | TypeInType gr -> hov 2 (safe_pr_global env gr ++ spc () ++ strbrk"relies on an unsafe hierarchy.") in |