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 +++++---
 test-suite/bugs/closed/3562.v | 6 ++++++
 2 files changed, 11 insertions(+), 3 deletions(-)
 create mode 100644 test-suite/bugs/closed/3562.v

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)
diff --git a/test-suite/bugs/closed/3562.v b/test-suite/bugs/closed/3562.v
new file mode 100644
index 0000000000..1a1410a3b1
--- /dev/null
+++ b/test-suite/bugs/closed/3562.v
@@ -0,0 +1,6 @@
+(* Should not be an anomaly as it was at some time in
+   September/October 2014 but some "Disjunctive/conjunctive
+   introduction pattern expected" error *)
+
+Theorem t: True.
+Fail destruct 0 as x.
-- 
cgit v1.2.3