diff options
| author | Hugo Herbelin | 2016-02-18 19:55:35 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2016-02-18 19:58:08 +0100 |
| commit | e28be21112c174a4c1a84d45a50745f0ad4e646a (patch) | |
| tree | f24c4886d2ae4942092abb945a6adc81ffbcc563 /tactics | |
| parent | 9e585d7479af0db837528a2fe2ce1690e22a36cb (diff) | |
Fixing a bug with introduction patterns over inductive types containing let-ins.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |