diff options
| author | Pierre-Marie Pédrot | 2019-08-14 14:24:47 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-08-14 14:24:47 +0200 |
| commit | 09002e0c20cf4da9cbb1e27146ae1fdd205b304a (patch) | |
| tree | 2948caf05c11b56bbf7643f532af4b1107370489 /vernac/comInductive.ml | |
| parent | b8477fb38842016c226ba9d7be8f60486411a2ee (diff) | |
| parent | 103af5bb20fd3bedb868df3031274089b7ffa5c0 (diff) | |
Merge PR #10642: Emit Feedback.AddedAxiom in Declare instead of higher layers
Reviewed-by: ppedrot
Diffstat (limited to 'vernac/comInductive.ml')
| -rw-r--r-- | vernac/comInductive.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 664010c917..adbe196699 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -567,9 +567,7 @@ let do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind ~uni (* Declare the possible notations of inductive types *) List.iter (Metasyntax.add_notation_interpretation (Global.env ())) ntns; (* Declare the coercions *) - List.iter (fun qid -> Class.try_add_new_coercion (Nametab.locate qid) ~local:false ~poly) coes; - (* If positivity is assumed declares itself as unsafe. *) - if Environ.deactivated_guard (Global.env ()) then Feedback.feedback Feedback.AddedAxiom else () + List.iter (fun qid -> Class.try_add_new_coercion (Nametab.locate qid) ~local:false ~poly) coes (** Prepare a "match" template for a given inductive type. For each branch of the match, we list the constructor name |