From 044d309d40bba56e49512c1d99ad64fa1a593e72 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 2 Oct 2014 22:56:24 -0400
Subject: [PATCH] Completeness of constant expression evaluation.

Also better error messages if a constant expression is expected.
---
 theories/ars.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/theories/ars.v b/theories/ars.v
index 558a17c9..43d18c23 100644
--- a/theories/ars.v
+++ b/theories/ars.v
@@ -68,6 +68,10 @@ Section rtc.
   Proof. intros. etransitivity; eauto. Qed.
   Lemma rtc_inv x z : rtc R x z → x = z ∨ ∃ y, R x y ∧ rtc R y z.
   Proof. inversion_clear 1; eauto. Qed.
+  Lemma rtc_ind_l (P : A → Prop) (z : A)
+    (Prefl : P z) (Pstep : ∀ x y, R x y → rtc R y z → P y → P x) :
+    ∀ x, rtc R x z → P x.
+  Proof. induction 1; eauto. Qed.
   Lemma rtc_ind_r_weak (P : A → A → Prop)
     (Prefl : ∀ x, P x x) (Pstep : ∀ x y z, rtc R x y → R y z → P x y → P x z) :
     ∀ x z, rtc R x z → P x z.
-- 
GitLab