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/micromega/EnvRing.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/micromega')

diff --git a/plugins/micromega/EnvRing.v b/plugins/micromega/EnvRing.v
index 36ed0210e3..b20f45af3e 100644
--- a/plugins/micromega/EnvRing.v
+++ b/plugins/micromega/EnvRing.v
@@ -925,7 +925,7 @@ Qed.
  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