From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Nov 2015 11:31:34 +0100 Subject: Imported Upstream version 8.5~beta3+dfsg --- test-suite/output/PrintAssumptions.v | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) (limited to 'test-suite/output/PrintAssumptions.v') diff --git a/test-suite/output/PrintAssumptions.v b/test-suite/output/PrintAssumptions.v index f23bc498..c2003816 100644 --- a/test-suite/output/PrintAssumptions.v +++ b/test-suite/output/PrintAssumptions.v @@ -94,3 +94,19 @@ 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. -- cgit v1.2.3