4 files changed, 15 insertions, 15 deletions
diff --git a/plugins/micromega/OrderedRing.v b/plugins/micromega/OrderedRing.v
index b260feab12..2246af64da 100644
--- a/plugins/micromega/OrderedRing.v
+++ b/plugins/micromega/OrderedRing.v
@@ -85,9 +85,9 @@ Notation "x < y" := (rlt x y).
 
 
 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 sor_setoid.
 
 
diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v
index 68add5b3dc..fb16c55c2f 100644
--- a/plugins/micromega/RingMicromega.v
+++ b/plugins/micromega/RingMicromega.v
@@ -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.
@@ -414,7 +414,7 @@ Proof.
   simpl ; intros.
   destruct (nth_in_or_default n l (Pc cO, Equal)).
   (* index is in bounds *)
-  apply H ; congruence.
+  apply H. congruence.
   (* index is out-of-bounds *)
   inversion H0.
   rewrite e. simpl.
diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v
index d8ab6fd30d..78837d4cd1 100644
--- a/plugins/micromega/ZMicromega.v
+++ b/plugins/micromega/ZMicromega.v
@@ -317,7 +317,7 @@ Qed.
 
 Require Import QArith.
 
-Inductive ZArithProof : Type :=
+Inductive ZArithProof :=
 | DoneProof
 | RatProof : ZWitness -> ZArithProof -> ZArithProof
 | CutProof : ZWitness -> ZArithProof -> ZArithProof
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 9515c5de92..d11454b276 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -536,10 +536,10 @@ struct
 
   let get_left_construct term =
    match Term.kind_of_term term with
-    | Term.Construct(_,i) -> (i,[| |])
+    | Term.Construct((_,i),_) -> (i,[| |])
     | Term.App(l,rst) ->
        (match Term.kind_of_term l with
-        | Term.Construct(_,i) -> (i,rst)
+        | Term.Construct((_,i),_) -> (i,rst)
         |   _     -> raise ParseError
        )
     | _ ->   raise ParseError
@@ -833,8 +833,8 @@ struct
 
   let parse_zop (op,args) =
    match kind_of_term op with
-    | Const x -> (assoc_const op zop_table, args.(0) , args.(1))
-    |  Ind(n,0) ->
+    | Const (x,_) -> (assoc_const op zop_table, args.(0) , args.(1))
+    | Ind((n,0),_) ->
         if Constr.equal op (Lazy.force coq_Eq) && Constr.equal args.(0) (Lazy.force coq_Z)
         then (Mc.OpEq, args.(1), args.(2))
         else raise ParseError
@@ -842,8 +842,8 @@ struct
 
   let parse_rop (op,args) =
     match kind_of_term op with
-     | Const x -> (assoc_const op rop_table, args.(0) , args.(1))
-     |  Ind(n,0) ->
+     | Const (x,_) -> (assoc_const op rop_table, args.(0) , args.(1))
+     | Ind((n,0),_) ->
         if Constr.equal op (Lazy.force coq_Eq) && Constr.equal args.(0) (Lazy.force coq_R)
         then (Mc.OpEq, args.(1), args.(2))
         else raise ParseError