From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Sun, 25 Jan 2015 14:42:51 +0100
Subject: Imported Upstream version 8.5~beta1+dfsg

---
 plugins/setoid_ring/Ncring_tac.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'plugins/setoid_ring/Ncring_tac.v')

diff --git a/plugins/setoid_ring/Ncring_tac.v b/plugins/setoid_ring/Ncring_tac.v
index 4fb02909..31c9e54d 100644
--- a/plugins/setoid_ring/Ncring_tac.v
+++ b/plugins/setoid_ring/Ncring_tac.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        *)
@@ -76,11 +76,11 @@ Instance  reify_mul (R:Type)
  : reify (mul:=op) (PEmul e1 e2) lvar (op t1 t2)|10.
 
 Instance  reify_mul_ext (R:Type) `{Ring R}
-  lvar z e2 t2 
+  lvar (z:Z) e2 t2 
  `{Ring (T:=R)}
  {_:reify e2 lvar t2}
  : reify (PEmul (PEc z) e2) lvar
-      (@multiplication Z _ _  z t2)|9.
+      (@multiplication Z _ _ z t2)|9.
 
 Instance  reify_sub (R:Type)
  e1 lvar t1 e2 t2 op
@@ -127,7 +127,6 @@ Definition list_reifyl (R:Type) lexpr lvar lterm
 
 Unset Implicit Arguments.
 
-
 Ltac lterm_goal g :=
   match g with
   | ?t1 == ?t2 => constr:(t1::t2::nil)
@@ -138,6 +137,7 @@ Ltac lterm_goal g :=
 Lemma Zeqb_ok: forall x y : Z, Zeq_bool x y = true -> x == y.
  intros x y H. rewrite (Zeq_bool_eq x y H). reflexivity. Qed. 
 
+
 Ltac reify_goal lvar lexpr lterm:=
   (*idtac lvar; idtac lexpr; idtac lterm;*)
   match lexpr with
-- 
cgit v1.2.3