From 793cf771e18be3d44d3fcf89998dec50fb8229f3 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 16 Dec 2015 21:33:03 +0100
Subject: FIx parsing of tactic "simple refine".

---
 tactics/extratactics.ml4 | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index e06997029d..1d594aa7c9 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -366,6 +366,9 @@ let refine_tac simple {Glob_term.closure=closure;term=term} =
 
 TACTIC EXTEND refine
 | [ "refine" uconstr(c) ] -> [ refine_tac false c ]
+END
+
+TACTIC EXTEND simple_refine
 | [ "simple" "refine" uconstr(c) ] -> [ refine_tac true c ]
 END
 
-- 
cgit v1.2.3