diff options
| author | Arnaud Spiwack | 2015-06-24 15:24:49 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2015-06-24 17:55:47 +0200 |
| commit | 75381f7356133f68637fc9bbc0a213dcfa6e2c71 (patch) | |
| tree | 702f46fe78ed264f6d74f364b3e22c387beed185 | |
| parent | ec74137b4e4b96135c43570b5f149e7e1ec0db9c (diff) | |
When assuming an inductive type positive, then it is declared "unsafe" to the interfaces.
| -rw-r--r-- | toplevel/command.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index ca925d4904..6beaf54c53 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -645,7 +645,10 @@ let do_mutual_inductive chk indl poly prv finite = (* Declare the possible notations of inductive types *) List.iter Metasyntax.add_notation_interpretation ntns; (* Declare the coercions *) - List.iter (fun qid -> Class.try_add_new_coercion (locate qid) false poly) coes + List.iter (fun qid -> Class.try_add_new_coercion (locate qid) false poly) coes; + (* If [chk] is [false] (i.e. positivity is assumed) declares itself + as unsafe. *) + if not chk then Pp.feedback Feedback.AddedAxiom else () (* 3c| Fixpoints and co-fixpoints *) |