theories: add back "oldlibs" in the CI + fix

config/tests.config

@@ -7,7 +7,7 @@ okdirs = theories/prelude
 
 [test-stdlib]
 okdirs  = !theories
-exclude = theories/prelude theories/oldlibs
+exclude = theories/prelude
 
 [test-examples]
 okdirs  = !examples

theories/oldlibs/CyclicGroup.ec

@@ -15,9 +15,10 @@ op g1 = g ^ F.zero.
 
 axiom gpow_log (a:group): g ^ (log a) = a.
 axiom log_gpow x : log (g ^ x) = x.
+axiom nosmt log_g : log g = F.one.
 
 lemma nosmt log_bij x y: x = y <=> log x = log y by smt (gpow_log).
-lemma nosmt pow_bij (x y:F.t): x = y <=> g^x =g^y by [].
+lemma nosmt pow_bij (x y:F.t): x = y <=> g^x =g^y by smt.
 
 
 axiom inv_def (a:group): inv a = g ^ (-log a).
@@ -27,9 +28,9 @@ axiom mul_pow g (x y:t): g ^ x * g ^ y = g ^ (x + y).
 
 axiom pow_pow g (x y:t): (g ^ x) ^ y = g ^ (x * y).
 
-lemma nosmt log_pow (g1:group) x: log (g1 ^ x) = log g1 * x by [].
+lemma nosmt log_pow (g1:group) x: log (g1 ^ x) = log g1 * x by smt.
 
-lemma nosmt log_mul (g1 g2:group): log (g1 * g2) = log g1 + log g2 by [].
+lemma nosmt log_mul (g1 g2:group): log (g1 * g2) = log g1 + log g2 by smt.
 
 lemma nosmt pow_mul (g1 g2:group) x: g1^x * g2^x = (g1*g2)^x.
 proof.
@@ -65,12 +66,6 @@ proof strict.
   by rewrite -div_def sub_def addfN.
 qed.
 
-lemma nosmt log_g : log g = F.one.
-proof strict.
- have H: log g - log g = F.one + -log g by smt.
- have H1: log g = log g + F.one + -log g; smt.
-qed.
-
 lemma nosmt g_neq0 : g1 <> g.
 proof.
   rewrite /g1 -{2}(gpow_log g) log_g -pow_bij;smt.

theories/oldlibs/OldDistr.ec

@@ -87,11 +87,11 @@ qed.
 
 lemma nosmt mu_or_le (d:'a distr) (p q:'a -> bool) r1 r2:
   mu d p <= r1 => mu d q <= r2 =>
-  mu d (predU p q) <= r1 + r2 by [].
+  mu d (predU p q) <= r1 + r2 by smt.
 
 lemma nosmt mu_and  (d:'a distr) (p q:'a -> bool):
   mu d (predI p q) = mu d p + mu d q - mu d (predU p q)
-by [].
+by smt.
 
 lemma nosmt mu_and_le_l (d:'a distr) (p q:'a -> bool) r:
   mu d p <= r =>
@@ -185,7 +185,7 @@ qed.
 
 lemma weight_0_mu (d:'a distr):
   weight d = 0%r => forall p, mu d p = 0%r
-by [].
+by smt.
 
 lemma mu_one (P:'a -> bool) (d:'a distr):
   P == predT =>

theories/oldlibs/OldFMap.ec

@@ -181,7 +181,7 @@ lemma set_set (m : ('a,'b) fmap) x x' y y':
    m.[x <- y].[x' <- y'] = if x = x' then m.[x' <- y']
                            else m.[x' <- y'].[x <- y].
 proof.
-rewrite fmapP=> a; case (x = x')=> [<<- {x'} | ne_x_x']; rewrite !getP.
+rewrite fmapP=> a; case (x = x')=> [<<- | ne_x_x']; rewrite !getP.
 + by case (a = x).
 by case (a = x')=> //; case (a = x)=> // ->;rewrite ne_x_x'.
 qed.
@@ -295,7 +295,7 @@ proof.
 rewrite allE allP; split=> [h a|h [a b] /= ^ab_in_m].
 + rewrite mem_domE mem_map_fst=> -[b] ^ab_in_m+.
   by rewrite mem_assoc_uniq 1:uniq_keys -getE /oget=> ->; apply (@h (a,b)).
-rewrite mem_assoc_uniq 1:uniq_keys -getE=> /(@congr1 oget) <-.
+rewrite mem_assoc_uniq 1:uniq_keys -getE=> /(@congr1 oget) /= <-.
 by apply/h; rewrite mem_domE mem_map_fst; exists b.
 qed.
 
@@ -701,11 +701,11 @@ qed.
 
 lemma set_eq_except x b (m : ('a, 'b) fmap):
   eq_except m.[x <- b] m (pred1 x).
-proof. by rewrite eq_exceptP=> x'; rewrite !getP=> ->. qed.
+proof. by rewrite eq_exceptP=> x'; rewrite !getP /pred1 /= => ->. qed.
 
 lemma set2_eq_except x b b' (m : ('a, 'b) fmap):
   eq_except m.[x <- b] m.[x <- b'] (pred1 x).
-proof. by rewrite eq_exceptP=> x'; rewrite !getP=> ->. qed.
+proof. by rewrite eq_exceptP=> x'; rewrite !getP /pred1 /= => ->. qed.
 
 lemma eq_except_set_eq (m1 m2 : ('a, 'b) fmap) x:
   mem (dom m1) x =>

theories/oldlibs/PrimeField.ec

@@ -156,21 +156,21 @@ by ringeq.
 
 import Int.
 lemma nosmt toint_pos (x:t): 0 <= toint x
-by [].
+by smt.
 
 lemma nosmt toint_lt (x:t): toint x < q
-by [].
+by smt.
 
 lemma nosmt toint_le (x:t): toint x <= q - 1
-by [].
+by smt.
 
 lemma nosmt toofint (x:int): 0 <= x => x < q => toint (ofint x) = x.
 proof.
   move=> Hp Hlt;rewrite toofint_mod IntDiv.modz_small /#.
 qed.
 
 lemma nosmt ofint1_: ofint 1 = F.one
-by [].
+by smt.
 
 theory FDistr.
 

theories/oldlibs/Prime_field.ec

@@ -92,7 +92,7 @@ qed.
 
 lemma nosmt gf_q_minus_minus (x:gf_q):
   -(-x) = x
-by [].
+by smt.
 
 lemma gf_q_minus_distr (x y z:gf_q):
   x * (y - z) = x * y - x * z.