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 | |
| parent | 9e585d7479af0db837528a2fe2ce1690e22a36cb (diff) | |
Fixing a bug with introduction patterns over inductive types containing let-ins.
| -rw-r--r-- | tactics/tactics.ml | 2 | ||||
| -rw-r--r-- | test-suite/success/intros.v | 7 |
2 files changed, 8 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 diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v index 69d66f1008..af5f994010 100644 --- a/test-suite/success/intros.v +++ b/test-suite/success/intros.v @@ -98,3 +98,10 @@ intros x ->. - reflexivity. - exact I. Qed. + +(* Fixing a bug when destructing a type with let-ins in the constructor *) + +Inductive I := C : let x:=1 in x=1 -> I. +Goal I -> True. +intros [x H]. (* Was failing in 8.5 *) +Abort. |