From 4395637a6471fc95934fe93da671bda68d415a77 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 26 Jul 2017 17:53:04 +0200
Subject: Ensuring that inductive constructors are always capitalized.

---
 tests/stuff/ltac2.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tests')

diff --git a/tests/stuff/ltac2.v b/tests/stuff/ltac2.v
index 770d385406..36ea1ef4c1 100644
--- a/tests/stuff/ltac2.v
+++ b/tests/stuff/ltac2.v
@@ -18,7 +18,7 @@ Ltac2 foo' _ := ident:(bla).
 
 Print Ltac2 foo'.
 
-Ltac2 bar x H := match x with
+Ltac2 bar x h := match x with
 | None => constr:(fun H => ltac2:(exact (hyp ident:(H))) -> nat)
 | Some x => x
 end.
-- 
cgit v1.2.3