From 7050ceaa09a29c3f50620a8d3f8439c3d69a10d0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 26 Dec 2018 23:46:19 +0100
Subject: Documenting syntax "injection ... as [= pat1 ... patn ]".

To prevent confusion, forbidding a mix of the "injection term as pat1
... patn" and of the "injection term as [= pat1 ... patn]" syntax: If
a "[= ...]" occurs, this should be a singleton list of patterns.
---
 plugins/setoid_ring/InitialRing.v  | 2 +-
 plugins/setoid_ring/Ring_polynom.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/setoid_ring')

diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v
index 4886c8b9aa..9be2535a3f 100644
--- a/plugins/setoid_ring/InitialRing.v
+++ b/plugins/setoid_ring/InitialRing.v
@@ -105,7 +105,7 @@ Section ZMORPHISM.
  Proof.
   constructor.
   destruct c;intros;try discriminate.
-  injection H as <-.
+  injection H as [= <-].
   simpl. unfold Zeq_bool. rewrite Z.compare_refl. trivial.
  Qed.
 
diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v
index f7cb6b688b..c5d396427b 100644
--- a/plugins/setoid_ring/Ring_polynom.v
+++ b/plugins/setoid_ring/Ring_polynom.v
@@ -894,7 +894,7 @@ Section MakeRingPol.
  revert P1. induction LM1 as [|(M2,P2') LM2 IH]; simpl; intros.
  - discriminate.
  - assert (H':=PNSubst_ok n P3 M2 P2'). destruct PNSubst.
-   * injection H as <-. rewrite <- PSubstL1_ok; intuition.
+   * injection H as [= <-]. rewrite <- PSubstL1_ok; intuition.
    * now apply IH.
  Qed.
 
-- 
cgit v1.2.3