From 9bdd8aff92829aaa7c5a45b6e4e5adfa9e8789df Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Sat, 8 Oct 2016 00:10:55 +0200
Subject: Fix bug #5098: Symmetry broken in HoTT.

We defactorize the in_clause grammar entry to allow parsing of the "symmetry"
tactic when it has no arguments. Beforehand, the clause_dft_concl entry
accepted the empty stream, preventing the definition of symmetry as a mere
identifier.
---
 parsing/pcoq.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'parsing/pcoq.ml')

diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 4e069c9e3..9e9a7e723 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -350,6 +350,7 @@ module Tactic =
     let red_expr = make_gen_entry utactic "red_expr"
     let simple_intropattern =
       make_gen_entry utactic "simple_intropattern"
+    let in_clause = make_gen_entry utactic "in_clause"
     let clause_dft_concl = 
       make_gen_entry utactic "clause"
 
-- 
cgit v1.2.3