(** Print Assumption and opaque modules :

  Print Assumption used to consider as axioms the modular fields
  unexported by their signature, cf bug report #2186. This should
  now be fixed, let's test this here. *)

(* First, a minimal test-case *)

Axiom foo : nat.

Module Type T.
 Parameter bar : nat.
End T.

Module M : T.
  Module Hide. (* An entire sub-module could be hidden *)
  Definition x := foo.
  End Hide.
  Definition bar := Hide.x.
End M.

Module N (X:T) : T.
  Definition y := X.bar. (* A non-exported field *)
  Definition bar := y.
End N.

Module P := N M.

Print Assumptions M.bar. (* Should answer: foo *)
Print Assumptions P.bar. (* Should answer: foo *)


(* The original test-case of the bug-report *)

Require Import Arith.

Axiom extensionality : forall P Q (f g:P -> Q),
  (forall x, f x = g x) -> f = g.

Module Type ADD_COMM_EXT.
  Axiom add_comm_ext : forall n, (fun x => x + n) = (fun x => n + x).
End ADD_COMM_EXT.

Module AddCommExt_Opaque : ADD_COMM_EXT.
  Lemma add_comm_ext : forall n, (fun x => x + n) = (fun x => n + x).
  Proof.
    intro n; apply extensionality; auto with arith.
  Qed.
End AddCommExt_Opaque.

Module AddCommExt_Transparent <: ADD_COMM_EXT.
  Lemma add_comm_ext : forall n, (fun x => x + n) = (fun x => n + x).
  Proof.
    intro n; apply extensionality; auto with arith.
  Qed.
End AddCommExt_Transparent.

Print Assumptions AddCommExt_Opaque.add_comm_ext.
(* Should answer: extensionality *)

Print Assumptions AddCommExt_Transparent.add_comm_ext.
(* Should answer: extensionality *)

Lemma add1_comm_ext_opaque :
  (fun x => x + 1) = (fun x => 1 + x).
Proof (AddCommExt_Opaque.add_comm_ext 1).

Lemma add1_comm_ext_transparent :
  (fun x => x + 1) = (fun x => 1 + x).
Proof (AddCommExt_Transparent.add_comm_ext 1).

Print Assumptions add1_comm_ext_opaque.
(* Should answer: extensionality *)

Print Assumptions add1_comm_ext_transparent.
(* Should answer: extensionality *)

Module Type FALSE_POSITIVE.
  Axiom add_comm : forall n x, x + n = n + x.
End FALSE_POSITIVE.

Module false_positive : FALSE_POSITIVE.
  Lemma add_comm : forall n x, x + n = n + x.
  Proof. auto with arith. Qed.

  Print Assumptions add_comm.
  (* Should answer : Closed under the global context *)
End false_positive.

Lemma comm_plus5 : forall x,
  x + 5 = 5 + x.
Proof (false_positive.add_comm 5).

Print Assumptions comm_plus5.
(* Should answer : Closed under the global context *)

(** Print Assumption and Include *)

Module INCLUDE.

Module M.
Axiom foo : False.
End M.

Module N.
Include M.
End N.

Print Assumptions N.foo.

End INCLUDE.

(* Print Assumptions did not enter implementation of submodules (#7192) *)

Module SUBMODULES.

Definition a := True.
Module Type B. Axiom f : Prop. End B.
Module Type C. Declare Module D : B. End C.
Module E: C.
  Module D <: B. Definition f := a. End D.
End E.
Print Assumptions E.D.f.

(* Idem in the scope of a functor *)

Module Type T. End T.
Module F (X : T).
  Definition a := True.
  Module Type B. Axiom f : Prop. End B.
  Module Type C. Declare Module D : B. End C.
  Module E: C.
    Module D <: B. Definition f := a. End D.
  End E.
  Print Assumptions E.D.f.
End F.

End SUBMODULES.

(* Testing a variant of #7192 across files *)
(* This was missing in the original fix to #7192 *)
Require Import module_bug7192.
Print Assumptions M7192.D.f.

(* Testing reporting assumptions from modules in files *)
(* A regression introduced in the original fix to #7192 was missing implementations *)
Require Import module_bug8416.
Print Assumptions M8416.f.