From 1f2cc4026cd5e977979ff1507fd5fa0d96e1a92f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 25 Dec 2015 06:08:29 +0100
Subject: Moving the ad hoc interpretation of "intros" as "intros **" from
 tacinterp.ml to g_tactic.ml4 so as to leave room for "IntroPattern []" to
 mean "no introduction".

---
 tactics/tacinterp.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 8c8861fd99..d96c8f98a2 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1775,7 +1775,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
           (TacIntroPattern l)
           (* spiwack: print uninterpreted, not sure if it is the
              expected behaviour. *)
-          (Tactics.intros_patterns l')) sigma
+          (Tactics.intro_patterns l')) sigma
       end }
   | TacIntroMove (ido,hto) ->
       Proofview.Goal.enter { enter = begin fun gl ->
-- 
cgit v1.2.3