Adding an output test to check that the hint commands respect their locality.

2 files changed, 164 insertions, 0 deletions

diff --git a/test-suite/output/HintLocality.out b/test-suite/output/HintLocality.out
new file mode 100644
index 0000000000..37a0613b25
--- /dev/null
+++ b/test-suite/output/HintLocality.out
@@ -0,0 +1,92 @@
+Non-discriminated database
+Unfoldable variable definitions: all
+Unfoldable constant definitions: all except: id
+Cut: _
+For any goal ->   
+For nat ->   
+For S (modes !) ->   
+
+Non-discriminated database
+Unfoldable variable definitions: all
+Unfoldable constant definitions: all except: id
+Cut: _
+For any goal ->   
+For nat ->   
+For S (modes !) ->   
+
+Non-discriminated database
+Unfoldable variable definitions: all
+Unfoldable constant definitions: all except: id
+Cut: _
+For any goal ->   
+For nat ->   
+For S (modes !) ->   
+
+Non-discriminated database
+Unfoldable variable definitions: all
+Unfoldable constant definitions: all except: id
+Cut: _
+For any goal ->   
+For nat ->   
+For S (modes !) ->   
+
+Non-discriminated database
+Unfoldable variable definitions: all
+Unfoldable constant definitions: all
+Cut: emp
+For any goal ->   
+For nat ->   simple apply 0 ; trivial(level 1, pattern nat, id 0) 
+
+Non-discriminated database
+Unfoldable variable definitions: all
+Unfoldable constant definitions: all
+Cut: emp
+For any goal ->   
+For nat ->   simple apply 0 ; trivial(level 1, pattern nat, id 0) 
+
+Non-discriminated database
+Unfoldable variable definitions: all
+Unfoldable constant definitions: all except: id
+Cut: _
+For any goal ->   
+For nat ->   
+For S (modes !) ->   
+
+Non-discriminated database
+Unfoldable variable definitions: all
+Unfoldable constant definitions: all
+Cut: emp
+For any goal ->   
+For nat ->   simple apply 0 ; trivial(level 1, pattern nat, id 0) 
+
+Non-discriminated database
+Unfoldable variable definitions: all
+Unfoldable constant definitions: all except: id
+Cut: _
+For any goal ->   
+For nat ->   
+For S (modes !) ->   
+
+The command has indeed failed with message:
+This command does not support the global attribute in sections.
+The command has indeed failed with message:
+This command does not support the global attribute in sections.
+The command has indeed failed with message:
+This command does not support the global attribute in sections.
+The command has indeed failed with message:
+This command does not support the global attribute in sections.
+Non-discriminated database
+Unfoldable variable definitions: all
+Unfoldable constant definitions: all except: id
+Cut: _
+For any goal ->   
+For nat ->   
+For S (modes !) ->   
+
+Non-discriminated database
+Unfoldable variable definitions: all
+Unfoldable constant definitions: all
+Cut: emp
+For any goal ->   
+For nat ->   simple apply 0 ; trivial(level 1, pattern nat, id 0) 
+
diff --git a/test-suite/output/HintLocality.v b/test-suite/output/HintLocality.v
new file mode 100644
index 0000000000..4481335907
--- /dev/null
+++ b/test-suite/output/HintLocality.v
@@ -0,0 +1,72 @@
+(** Test hint command locality w.r.t. modules *)
+
+Create HintDb foodb.
+Create HintDb bardb.
+Create HintDb quxdb.
+
+#[global] Hint Immediate O : foodb.
+#[global] Hint Immediate O : bardb.
+#[global] Hint Immediate O : quxdb.
+
+Module Test.
+
+#[global] Hint Cut [ _ ] : foodb.
+#[global] Hint Mode S ! : foodb.
+#[global] Hint Opaque id : foodb.
+#[global] Remove Hints O : foodb.
+
+#[local] Hint Cut [ _ ] : bardb.
+#[local] Hint Mode S ! : bardb.
+#[local] Hint Opaque id : bardb.
+#[local] Remove Hints O : bardb.
+
+#[export] Hint Cut [ _ ] : quxdb.
+#[export] Hint Mode S ! : quxdb.
+#[export] Hint Opaque id : quxdb.
+#[export] Remove Hints O : quxdb.
+
+(** All three agree here *)
+
+Print HintDb foodb.
+Print HintDb bardb.
+Print HintDb quxdb.
+
+End Test.
+
+(** bardb and quxdb agree here *)
+
+Print HintDb foodb.
+Print HintDb bardb.
+Print HintDb quxdb.
+
+Import Test.
+
+(** foodb and quxdb agree here *)
+
+Print HintDb foodb.
+Print HintDb bardb.
+Print HintDb quxdb.
+
+(** Test hint command locality w.r.t. sections *)
+
+Create HintDb secdb.
+
+#[global] Hint Immediate O : secdb.
+
+Section Sec.
+
+Fail #[global] Hint Cut [ _ ] : secdb.
+Fail #[global] Hint Mode S ! : secdb.
+Fail #[global] Hint Opaque id : secdb.
+Fail #[global] Remove Hints O : secdb.
+
+#[local] Hint Cut [ _ ] : secdb.
+#[local] Hint Mode S ! : secdb.
+#[local] Hint Opaque id : secdb.
+#[local] Remove Hints O : secdb.
+
+Print HintDb secdb.
+
+End Sec.
+
+Print HintDb secdb.