diff options
| -rw-r--r-- | test-suite/bugs/closed/335.v | 5 | ||||
| -rw-r--r-- | test-suite/success/import_lib.v | 202 |
2 files changed, 207 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/335.v b/test-suite/bugs/closed/335.v new file mode 100644 index 000000000..166fa7a9f --- /dev/null +++ b/test-suite/bugs/closed/335.v @@ -0,0 +1,5 @@ +(* Compatibility of Require with backtracking at interactive module end *) + +Module A. +Require List. +End A. diff --git a/test-suite/success/import_lib.v b/test-suite/success/import_lib.v new file mode 100644 index 000000000..fcedb2b1a --- /dev/null +++ b/test-suite/success/import_lib.v @@ -0,0 +1,202 @@ +Definition le_trans := 0. + + +Module Test_Read. + Module M. + Require Le. (* Reading without importing *) + + Check Le.le_trans. + + Lemma th0 : le_trans = 0. + reflexivity. + Qed. + End M. + + Check Le.le_trans. + + Lemma th0 : le_trans = 0. + reflexivity. + Qed. + + Import M. + + Lemma th1 : le_trans = 0. + reflexivity. + Qed. +End Test_Read. + + +(****************************************************************) + +Definition le_decide := 1. (* from Arith/Compare *) +Definition min := 0. (* from Arith/Min *) + +Module Test_Require. + + Module M. + Require Import Compare. (* Imports Min as well *) + + Lemma th1 : le_decide = le_decide. + reflexivity. + Qed. + + Lemma th2 : min = min. + reflexivity. + Qed. + + End M. + + (* Checks that Compare and List are loaded *) + Check Compare.le_decide. + Check Min.min. + + + (* Checks that Compare and List are _not_ imported *) + Lemma th1 : le_decide = 1. + reflexivity. + Qed. + + Lemma th2 : min = 0. + reflexivity. + Qed. + + (* It should still be the case after Import M *) + Import M. + + Lemma th3 : le_decide = 1. + reflexivity. + Qed. + + Lemma th4 : min = 0. + reflexivity. + Qed. + +End Test_Require. + +(****************************************************************) + +Module Test_Import. + Module M. + Import Compare. (* Imports Min as well *) + + Lemma th1 : le_decide = le_decide. + reflexivity. + Qed. + + Lemma th2 : min = min. + reflexivity. + Qed. + + End M. + + (* Checks that Compare and List are loaded *) + Check Compare.le_decide. + Check Min.min. + + + (* Checks that Compare and List are _not_ imported *) + Lemma th1 : le_decide = 1. + reflexivity. + Qed. + + Lemma th2 : min = 0. + reflexivity. + Qed. + + (* It should still be the case after Import M *) + Import M. + + Lemma th3 : le_decide = 1. + reflexivity. + Qed. + + Lemma th4 : min = 0. + reflexivity. + Qed. +End Test_Import. + +(************************************************************************) + +Module Test_Export. + Module M. + Export Compare. (* Exports Min as well *) + + Lemma th1 : le_decide = le_decide. + reflexivity. + Qed. + + Lemma th2 : min = min. + reflexivity. + Qed. + + End M. + + + (* Checks that Compare and List are _not_ imported *) + Lemma th1 : le_decide = 1. + reflexivity. + Qed. + + Lemma th2 : min = 0. + reflexivity. + Qed. + + + (* After Import M they should be imported as well *) + + Import M. + + Lemma th3 : le_decide = le_decide. + reflexivity. + Qed. + + Lemma th4 : min = min. + reflexivity. + Qed. +End Test_Export. + + +(************************************************************************) + +Module Test_Require_Export. + + Definition mult_sym := 1. (* from Arith/Mult *) + Definition plus_sym := 0. (* from Arith/Plus *) + + Module M. + Require Export Mult. (* Exports Plus as well *) + + Lemma th1 : mult_comm = mult_comm. + reflexivity. + Qed. + + Lemma th2 : plus_comm = plus_comm. + reflexivity. + Qed. + + End M. + + + (* Checks that Mult and Plus are _not_ imported *) + Lemma th1 : mult_sym = 1. + reflexivity. + Qed. + + Lemma th2 : plus_sym = 0. + reflexivity. + Qed. + + + (* After Import M they should be imported as well *) + + Import M. + + Lemma th3 : mult_comm = mult_comm. + reflexivity. + Qed. + + Lemma th4 : plus_comm = plus_comm. + reflexivity. + Qed. + +End Test_Require_Export. |