From e28be21112c174a4c1a84d45a50745f0ad4e646a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 18 Feb 2016 19:55:35 +0100
Subject: Fixing a bug with introduction patterns over inductive types
 containing let-ins.

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

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c949a58b1d..f0f46c14db 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2090,7 +2090,7 @@ let intro_or_and_pattern loc bracketed ll thin tac id =
   let c = mkVar id in
   let t = Tacmach.New.pf_unsafe_type_of gl c in
   let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl t in
-  let nv = constructors_nrealargs ind in
+  let nv = constructors_nrealdecls ind in
   let ll = fix_empty_or_and_pattern (Array.length nv) ll in
   check_or_and_pattern_size loc ll (Array.length nv);
   Tacticals.New.tclTHENLASTn
-- 
cgit v1.2.3