From 2367d5a90e348a12a52f3aaa66f4e504d7109d67 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Fri, 9 Oct 2020 20:21:08 -0700
Subject: Modify micromega/Ztac.v to compile with -mangle-names

---
 theories/micromega/Ztac.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/theories/micromega/Ztac.v b/theories/micromega/Ztac.v
index 5fb92aba44..a97ea85ceb 100644
--- a/theories/micromega/Ztac.v
+++ b/theories/micromega/Ztac.v
@@ -26,7 +26,7 @@ Qed.
 Lemma elim_concl_eq :
   forall x y, (x < y \/ y < x -> False) -> x = y.
 Proof.
-  intros.
+  intros x y H.
   destruct (Z_lt_le_dec x y).
   exfalso. apply H ; auto.
   destruct (Zle_lt_or_eq y x);auto.
@@ -37,7 +37,7 @@ Qed.
 Lemma elim_concl_le :
   forall x y, (y < x -> False) -> x <= y.
 Proof.
-  intros.
+  intros x y H.
   destruct (Z_lt_le_dec y x).
   exfalso ; auto.
   auto.
@@ -46,7 +46,7 @@ Qed.
 Lemma elim_concl_lt :
   forall x y, (y <= x -> False) -> x < y.
 Proof.
-  intros.
+  intros x y H.
   destruct (Z_lt_le_dec x y).
   auto.
   exfalso ; auto.
@@ -93,7 +93,7 @@ Qed.
 
 Lemma mul_le : forall e1 e2, 0 <= e1 -> 0 <= e2 -> 0 <= e1*e2.
 Proof.
-  intros.
+  intros e1 e2 H H0.
   change 0 with (0* e2).
   apply Zmult_le_compat_r; auto.
 Qed.
-- 
cgit v1.2.3