Imported Upstream version 8.5~beta1+dfsg

1 files changed, 16 insertions, 15 deletions

diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v
index a2136506..a0545637 100644
--- a/plugins/micromega/RingMicromega.v
+++ b/plugins/micromega/RingMicromega.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -57,7 +57,7 @@ Variables ceqb cleb : C -> C -> bool.
 Variable phi : C -> R.
 
 (* Power coefficients *)
-Variable E : Set. (* the type of exponents *)
+Variable E : Type. (* the type of exponents *)
 Variable pow_phi : N -> E.
 Variable rpow : R -> E -> R.
 
@@ -78,9 +78,9 @@ Record SORaddon := mk_SOR_addon {
 Variable addon : SORaddon.
 
 Add Relation R req
-  reflexivity proved by sor.(SORsetoid).(@Equivalence_Reflexive _ _ )
-  symmetry proved by sor.(SORsetoid).(@Equivalence_Symmetric _ _ )
-  transitivity proved by sor.(SORsetoid).(@Equivalence_Transitive _ _ )
+  reflexivity proved by sor.(SORsetoid).(@Equivalence_Reflexive _ _)
+  symmetry proved by sor.(SORsetoid).(@Equivalence_Symmetric _ _)
+  transitivity proved by sor.(SORsetoid).(@Equivalence_Transitive _ _)
 as micomega_sor_setoid.
 
 Add Morphism rplus with signature req ==> req ==> req as rplus_morph.
@@ -141,8 +141,8 @@ Qed.
 
 Definition PolC := Pol C. (* polynomials in generalized Horner form, defined in Ring_polynom or EnvRing *)
 Definition PolEnv := Env R. (* For interpreting PolC *)
-Definition eval_pol (env : PolEnv) (p:PolC) : R :=
-   Pphi rplus rtimes phi env p.
+Definition eval_pol : PolEnv -> PolC -> R :=
+   Pphi rplus rtimes phi.
 
 Inductive Op1 : Set := (* relations with 0 *)
 | Equal (* == 0 *)
@@ -412,12 +412,12 @@ Proof.
   induction e.
   (* PsatzIn *)
   simpl ; intros.
-  destruct (nth_in_or_default n l (Pc cO, Equal)).
+  destruct (nth_in_or_default n l (Pc cO, Equal)) as [Hin|Heq].
   (* index is in bounds *)
-  apply H ; congruence.
+  apply H. congruence.
   (* index is out-of-bounds *)
   inversion H0.
-  rewrite e. simpl.
+  rewrite Heq. simpl.
   now apply  addon.(SORrm).(morph0).
   (* PsatzSquare *)
   simpl. intros. inversion H0.
@@ -679,7 +679,8 @@ match o with
 | OpGt => fun x y : R => y < x
 end.
 
-Definition  eval_pexpr (l : PolEnv) (pe : PExpr C) : R := PEeval rplus rtimes rminus ropp phi pow_phi rpow l pe.
+Definition  eval_pexpr : PolEnv -> PExpr C -> R :=
+ PEeval rplus rtimes rminus ropp phi pow_phi rpow.
 
 Record Formula (T:Type) : Type := {
   Flhs : PExpr T;
@@ -910,7 +911,7 @@ Proof.
   unfold pow_N. ring.
 Qed.
 
-Definition denorm (p : Pol C)  := xdenorm xH p.
+Definition denorm := xdenorm xH.
 
 Lemma denorm_correct : forall p env, eval_pol env p == eval_pexpr env (denorm p).
 Proof.
@@ -947,7 +948,7 @@ Variable phi_C_of_S :   forall c,  phiS c =  phi (C_of_S c).
 Fixpoint map_PExpr (e : PExpr S) : PExpr C :=
   match e with
     | PEc c => PEc (C_of_S c)
-    | PEX p => PEX _ p
+    | PEX _ p => PEX _ p
     | PEadd e1 e2 => PEadd (map_PExpr e1) (map_PExpr e2)
     | PEsub e1 e2 => PEsub (map_PExpr e1) (map_PExpr e2)
     | PEmul e1 e2 => PEmul (map_PExpr e1) (map_PExpr e2)
@@ -960,8 +961,8 @@ Definition map_Formula (f : Formula S)  : Formula C :=
     Build_Formula (map_PExpr l) o (map_PExpr r).
 
 
-Definition eval_sexpr (env : PolEnv) (e : PExpr S) : R :=
-  PEeval rplus rtimes rminus ropp phiS pow_phi rpow env e.
+Definition eval_sexpr : PolEnv -> PExpr S -> R :=
+  PEeval rplus rtimes rminus ropp phiS pow_phi rpow.
 
 Definition eval_sformula (env : PolEnv) (f : Formula S) : Prop :=
   let (lhs, op, rhs) := f in