From 5c599bfa507a5586e1f481983a5a7d4a6e19dadf Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 7 Nov 2014 20:08:55 +0100
Subject: Fixing #3562 ("as" in "destruct" expects either a disjunctive
 intropattern or a bound ltac variable).

---
 tactics/tacintern.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 22951491b7..9ca8da9d35 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -268,9 +268,11 @@ and intern_intro_pattern_action lf ist = function
 and intern_or_and_intro_pattern lf ist =
   List.map (List.map (intern_intro_pattern lf ist))
 
-let intern_or_and_intro_pattern_loc lf ist l =
-  intern_or_var (fun (loc,l) -> (loc,intern_or_and_intro_pattern lf ist l))
-    ist l
+let intern_or_and_intro_pattern_loc lf ist = function
+  | ArgVar (_,id) as x ->
+      if find_var id ist then x
+      else error "Disjunctive/conjunctive introduction pattern expected."
+  | ArgArg (loc,l) -> ArgArg (loc,intern_or_and_intro_pattern lf ist l)
 
 let intern_intro_pattern_naming_loc lf ist (loc,pat) =
   (loc,intern_intro_pattern_naming lf ist pat)
-- 
cgit v1.2.3