fix unused quantified variables

bench/typing/good/clash_namespace1.why

@@ -3,7 +3,7 @@
 
 theory A
   type t
-  axiom Ax : forall x:t. true
+  axiom Ax : forall x:t. x=x
 end
 
 theory B

examples/check-builtin/minmax.why

@@ -4,5 +4,5 @@ theory MinMax
   goal G : forall x y z : t. ge z y -> ge z x -> ge y x ->
                              min x (max (min z x) y) = x
 
-  goal G2 : forall x y z : t. max x y = x -> ge x y
+  goal G2 : forall x y: t. max x y = x -> ge x y
 end
\ No newline at end of file

examples/explicit_subst.why

@@ -37,7 +37,7 @@ theory LambdaCalc
   forall t : term 'b.
   subst (Var j) i t = if i = j then t else (Var j)  (* correct ?*)
 
-  axiom Subst_def1 : forall i j : nat.
+  axiom Subst_def1 : forall i : nat.
   forall t : term 'b. subst (Var i) i t = t
 
   axiom Subst_def2 : forall t1 : term 'a. forall i : nat.
@@ -48,7 +48,7 @@ theory LambdaCalc
   function app (t1 : term 'a) (t2 : term 'b) : term 'a
 
   axiom App_def :
-  forall t1 : term 'a. forall i : nat. forall t2 : term 'b.
+  forall t1 : term 'a. forall t2 : term 'b.
   app (Lambda t1) t2 = subst t1 Zero t2
 
 (* When we remove one of the following example the axiomatic is not anymore inconsistent *)
@@ -142,7 +142,7 @@ theory LambdaCalc2
   function app (t1 : app 'b 'a) (t2 : 'b) : 'a
 
   axiom App_def :
-  forall t1 : 'a. forall i : nat. forall t2 : 'b.
+  forall t1 : 'a. forall t2 : 'b.
   app (lambda t1) t2 = subst t1 Zero t2
 
   (* axiom Subst_app : *)

examples/hoare_logic/wp3.mlw

@@ -179,7 +179,7 @@ inductive one_step env env expr env env expr =
                  sigma' pi' (Eassign x e')
 
   | one_step_assign_value:
-      forall sigma pi:env, x:ident, v:value, e:term.
+      forall sigma pi:env, x:ident, v:value.
         one_step sigma pi (Eassign x (Evalue v))
                  (IdMap.set sigma x v) pi void
 

examples/hoare_logic/wp4.mlw

@@ -232,7 +232,7 @@ inductive one_step env stack expr env stack expr =
                  sigma' pi' (Eassign x e')
 
   | one_step_assign_value:
-      forall sigma:env, pi:stack, x:refident, v:value, e:term.
+      forall sigma:env, pi:stack, x:refident, v:value.
         one_step sigma pi (Eassign x (Evalue v))
                  (IdMap.set sigma x v) pi void
 
@@ -242,7 +242,7 @@ inductive one_step env stack expr env stack expr =
           one_step sigma pi (Eseq e1 e2) sigma' pi' (Eseq e1' e2)
 
   | one_step_seq_value:
-      forall sigma:env, pi:stack, id:ident, e:expr.
+      forall sigma:env, pi:stack, e:expr.
         one_step sigma pi (Eseq void e) sigma pi e
 
   | one_step_let_ctxt:
@@ -255,16 +255,16 @@ inductive one_step env stack expr env stack expr =
         one_step sigma pi (Elet id (Evalue v) e) sigma (Cons (id,v) pi) e
 
   | one_step_if_ctxt:
-      forall sigma sigma':env, pi pi':stack, id:ident, e1 e1' e2 e3:expr.
+      forall sigma sigma':env, pi pi':stack, e1 e1' e2 e3:expr.
         one_step sigma pi e1 sigma' pi' e1' ->
           one_step sigma pi (Eif e1 e2 e3) sigma' pi' (Eif e1' e2 e3)
 
   | one_step_if_true:
-      forall sigma:env, pi:stack, e:term, e1 e2:expr.
+      forall sigma:env, pi:stack, e1 e2:expr.
         one_step sigma pi (Eif (Evalue (Vbool True)) e1 e2) sigma pi e1
 
   | one_step_if_false:
-      forall sigma:env, pi:stack, e:term, e1 e2:expr.
+      forall sigma:env, pi:stack, e1 e2:expr.
         one_step sigma pi (Eif (Evalue (Vbool False)) e1 e2) sigma pi e2
 
   | one_step_assert:

examples/programs/euler002.mlw

@@ -45,11 +45,11 @@ theory FibSumEven "sum of even-valued Fibonacci numbers"
      (* Note: we take for granted that [fib] is an
         increasing sequence *)
 
-  axiom SumYes: forall n m s:int.
+  axiom SumYes: forall n m:int.
      n >= 0 -> (fib n) < m -> mod (fib n) 2 = 0 ->
        fib_sum_even_lt_from m n = fib_sum_even_lt_from m (n+1) + (fib n)
 
-  axiom SumOdd: forall n m s:int.
+  axiom SumOdd: forall n m:int.
      n >= 0 -> mod (fib n) 2 <> 0 ->
        fib_sum_even_lt_from m n = fib_sum_even_lt_from m (n+1)
 

examples/programs/list_rev.mlw

@@ -99,7 +99,7 @@ module M
 
   (** Frame for list_disj *)
   axiom frame_list_disj :
-    forall ft : ft pointer, next : next,
+    forall next : next,
         p1 : pointer, p2 : pointer, q : pointer, v : pointer
         [list_disj (list_ft next[q <- v] p1) next[q <- v] p2].
       (not in_ft q (list_ft next p1)) -> (not in_ft q (list_ft next p2))
@@ -148,7 +148,7 @@ module M
 
   (** frame model *)
   axiom frame_model :
-    forall ft : ft pointer, next : next,
+    forall next : next,
     p : pointer, q : pointer, v : pointer[model next[q <- v] p].
     (not in_ft q (list_ft next p))
     -> model next p = model next[q <- v] p
@@ -316,7 +316,7 @@ module M2
 
   (** frame model *)
   lemma frame_model :
-    forall ft : ft pointer, next : next,
+    forall next : next,
     p : pointer, q : pointer, v : pointer[model next[q <- v] p].
     is_list next p ->
     (not in_ft q (list_ft next p)) ->

examples/set.why

@@ -14,10 +14,10 @@ theory Bidule
   goal Inter : forall s1 s2 : s. forall x : a.
     mem x (inter s1 s2) -> (mem x s1 /\ mem x s2)
 
-  goal Union_inter : forall s1 s2 s3 : s. forall x : a.
+  goal Union_inter : forall s1 s2 s3 : s. 
     equal (inter (union s1 s2) s3) (union (inter s1 s3) (inter s2 s3))
 
-  lemma Union_assoc : forall s1 s2 s3 : s. forall x : a.
+  lemma Union_assoc : forall s1 s2 s3 : s. 
     equal (union (union s1 s2) s3) (union s1 (union s2 s3))
 
   clone algebra.Assoc with type t = s, function op = union, goal Assoc

examples/triangle_inequality.why

@@ -51,18 +51,18 @@ theory CauchySchwarzInequality
     forall x y:real. y <> 0.0 -> (x/y)*y = x
 
   lemma p_val_part:
-    forall x1 x2 y1 y2 t:real.
+    forall x1 x2 y1 y2:real.
       norm2 y1 y2 > 0.0 ->
         p x1 x2 y1 y2 (- dot x1 x2 y1 y2 / norm2 y1 y2) =
         norm2 x1 x2 - sqr (dot x1 x2 y1 y2) / norm2 y1 y2
 
   lemma p_val_part_pos:
-    forall x1 x2 y1 y2 t:real.
+    forall x1 x2 y1 y2:real.
       norm2 y1 y2 > 0.0 ->
         norm2 x1 x2 - sqr (dot x1 x2 y1 y2) / norm2 y1 y2 >= 0.0
 
   lemma p_val_part_pos_aux:
-    forall x1 x2 y1 y2 t:real.
+    forall x1 x2 y1 y2:real.
       norm2 y1 y2 > 0.0 ->
         norm2 y1 y2 * p x1 x2 y1 y2 (- dot x1 x2 y1 y2 / norm2 y1 y2) >= 0.0
 

theories/graph.why

@@ -57,7 +57,7 @@ theory IntPathWeight
   end
 
   lemma path_weight_right_extension:
-    forall x y z: vertex, l: list vertex.
+    forall x y: vertex, l: list vertex.
     path_weight (l ++ Cons x Nil) y = path_weight l x + weight x y
 
   lemma path_weight_decomposition:

theories/number.why

@@ -135,7 +135,7 @@ theory Gcd
   use int.EuclideanDivision
 
   lemma Gcd_euclidean_mod:
-    forall a b g: int [gcd b (EuclideanDivision.mod a b)].
+    forall a b: int [gcd b (EuclideanDivision.mod a b)].
     b <> 0 -> gcd b (EuclideanDivision.mod a b) = gcd a b
 
   lemma gcd_mult: forall a b c: int. 0 <= c -> gcd (c * a) (c * b) = c * gcd a b

theories/real.why

@@ -111,7 +111,7 @@ theory FromInt
   axiom Mul:
     forall x y:int. from_int (Int.(*) x y) = from_int x * from_int y
   axiom Neg:
-    forall x y:int. from_int (Int.(-_) (x)) = - from_int x
+    forall x:int. from_int (Int.(-_) (x)) = - from_int x
 
 end