From e73d5db97cdb22cce2ee479469f62af3c4b6264a Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Fri, 8 Jul 2016 14:43:57 +0200
Subject: Port to Coq 8.5pl2

Manual merging of branch jhjourdan:coq8.5.
No other change un functionality.
---
 lib/Coqlib.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'lib/Coqlib.v')

diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index fc4a59f6..6fa82492 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -22,6 +22,8 @@ Require Export Znumtheory.
 Require Export List.
 Require Export Bool.
 
+Global Set Asymmetric Patterns.
+
 (** * Useful tactics *)
 
 Ltac inv H := inversion H; clear H; subst.
@@ -768,7 +770,7 @@ Proof.
   discriminate.
   rewrite list_length_z_cons. destruct (zeq n 0).
   generalize (list_length_z_pos l); omega.
-  exploit IHl; eauto. unfold Zpred. omega.
+  exploit IHl; eauto. omega.
 Qed.
 
 (** Properties of [List.incl] (list inclusion). *)
@@ -1431,4 +1433,3 @@ Lemma nlist_forall2_imply:
 Proof.
   induction 1; simpl; intros; constructor; auto.
 Qed.
-
-- 
cgit