Make Coq 8.5 the default target for Fiat-Crypto

Instructions for 8.4 build in the README

1 files changed, 7 insertions, 7 deletions

diff --git a/coqprime/Coqprime/Root.v b/coqprime/Coqprime/Root.v
index 4e74a4d2f..2f65790d6 100644
--- a/coqprime/Coqprime/Root.v
+++ b/coqprime/Coqprime/Root.v
@@ -11,11 +11,11 @@
                                                                                                          
       Proof that a polynomial has at most n roots                                 
 ************************************************************************)
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.Lists.List.
-Require Import Coqprime.UList.
-Require Import Coqprime.Tactic.
-Require Import Coqprime.Permutation.
+Require Import ZArith.
+Require Import List.
+Require Import UList.
+Require Import Tactic.
+Require Import Permutation.
 
 Open Scope Z_scope.
 
@@ -33,8 +33,8 @@ Let pol := list A.
 Definition toA z := 
 match z with 
   Z0  => zero 
-| Zpos p => iter_pos  p _ (plus one) zero 
-| Zneg p => op (iter_pos p _ (plus one) zero) 
+| Zpos p => iter_pos _ (plus one) zero p 
+| Zneg p => op (iter_pos _ (plus one) zero p) 
 end.
 
 Fixpoint eval (p: pol) (x: A) {struct p} : A :=