Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg

7 files changed, 107 insertions, 8 deletions

diff --git a/test-suite/output/ArgumentsScope.out b/test-suite/output/ArgumentsScope.out
new file mode 100644
index 00000000..6643c142
--- /dev/null
+++ b/test-suite/output/ArgumentsScope.out
@@ -0,0 +1,56 @@
+a : bool -> bool
+
+Argument scope is [bool_scope]
+Expands to: Variable a
+b : bool -> bool
+
+Argument scope is [bool_scope]
+Expands to: Variable b
+negb'' : bool -> bool
+
+Argument scope is [bool_scope]
+negb'' is transparent
+Expands to: Constant Top.A.B.negb''
+negb' : bool -> bool
+
+Argument scope is [bool_scope]
+negb' is transparent
+Expands to: Constant Top.A.negb'
+negb : bool -> bool
+
+Argument scope is [bool_scope]
+negb is transparent
+Expands to: Constant Coq.Init.Datatypes.negb
+a : bool -> bool
+
+Expands to: Variable a
+b : bool -> bool
+
+Expands to: Variable b
+negb : bool -> bool
+
+negb is transparent
+Expands to: Constant Coq.Init.Datatypes.negb
+negb' : bool -> bool
+
+negb' is transparent
+Expands to: Constant Top.A.negb'
+negb'' : bool -> bool
+
+negb'' is transparent
+Expands to: Constant Top.A.B.negb''
+a : bool -> bool
+
+Expands to: Variable a
+negb : bool -> bool
+
+negb is transparent
+Expands to: Constant Coq.Init.Datatypes.negb
+negb' : bool -> bool
+
+negb' is transparent
+Expands to: Constant Top.negb'
+negb'' : bool -> bool
+
+negb'' is transparent
+Expands to: Constant Top.negb''
diff --git a/test-suite/output/ArgumentsScope.v b/test-suite/output/ArgumentsScope.v
new file mode 100644
index 00000000..13b5e13d
--- /dev/null
+++ b/test-suite/output/ArgumentsScope.v
@@ -0,0 +1,29 @@
+(* A few tests to check Argument Scope Global command *)
+
+Section A.
+Variable a : bool -> bool.
+Definition negb' := negb.
+Section B.
+Variable b : bool -> bool.
+Definition negb'' := negb.
+About a.
+About b.
+About negb''.
+About negb'.
+About negb.
+Arguments Scope Global negb'' [ _ ].
+Arguments Scope Global negb' [ _ ].
+Arguments Scope Global negb [ _ ].
+Arguments Scope Global a [ _ ].
+Arguments Scope Global b [ _ ].
+About a.
+About b.
+About negb.
+About negb'.
+About negb''.
+End B.
+About a.
+End A.
+About negb.
+About negb'.
+About negb''.
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 9d0d0658..995754a6 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -21,7 +21,7 @@ Argument scopes are [nat_scope nat_scope _ _ _]
 foo = 
 fix foo (A : Type) (l : list A) {struct l} : option A :=
   match l with
-  | nil => None (A:=A)
+  | nil => None
   | x0 :: nil => Some x0
   | x0 :: (_ :: _) as l0 => foo A l0
   end
diff --git a/test-suite/output/Fixpoint.out b/test-suite/output/Fixpoint.out
index f4270d3d..c69d31f4 100644
--- a/test-suite/output/Fixpoint.out
+++ b/test-suite/output/Fixpoint.out
@@ -1,6 +1,6 @@
 fix F (A B : Set) (f : A -> B) (l : list A) {struct l} : 
 list B := match l with
-          | nil => nil (A:=B)
+          | nil => nil
           | a :: l0 => f a :: F A B f l0
           end
      : forall A B : Set, (A -> B) -> list A -> list B
@@ -13,13 +13,13 @@ fix even_pos_odd_pos 2
  with (odd_pos_even_pos (n:_) (H:odd n) {struct H} : n >= 1).
  intros.
  destruct H.
-   omega.
+  omega.
   
-   apply odd_pos_even_pos in H.
-   omega.
+  apply odd_pos_even_pos in H.
+  omega.
   
  intros.
  destruct H.
-  apply even_pos_odd_pos in H.
-  omega.
+ apply even_pos_odd_pos in H.
+ omega.
  
diff --git a/test-suite/output/Match_subterm.out b/test-suite/output/Match_subterm.out
new file mode 100644
index 00000000..951a98db
--- /dev/null
+++ b/test-suite/output/Match_subterm.out
@@ -0,0 +1,8 @@
+(0 = 1)
+eq
+nat
+0
+1
+S
+0
+2
diff --git a/test-suite/output/Match_subterm.v b/test-suite/output/Match_subterm.v
new file mode 100644
index 00000000..2c44b187
--- /dev/null
+++ b/test-suite/output/Match_subterm.v
@@ -0,0 +1,6 @@
+Goal 0 = 1.
+match goal with
+| |- context [?v] =>
+  idtac v ; fail
+| _ => idtac 2
+end.
diff --git a/test-suite/output/Tactics.out b/test-suite/output/Tactics.out
index 287e8488..ac5eedc1 100644
--- a/test-suite/output/Tactics.out
+++ b/test-suite/output/Tactics.out
@@ -1,4 +1,4 @@
-intro H; split; [  a H |  e H ].
+intro H; split; [ a H | e H ].
 
 intros; match goal with
         | |- context [if ?X then _ else _] => case X