From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- test-suite/bugs/opened/3343.v | 46 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 46 insertions(+) create mode 100644 test-suite/bugs/opened/3343.v (limited to 'test-suite/bugs/opened/3343.v') diff --git a/test-suite/bugs/opened/3343.v b/test-suite/bugs/opened/3343.v new file mode 100644 index 00000000..6c5a85f9 --- /dev/null +++ b/test-suite/bugs/opened/3343.v @@ -0,0 +1,46 @@ +(* File reduced by coq-bug-finder from original input, then from 13699 lines to 656 lines, then from 584 lines to 200 lines *) +Set Asymmetric Patterns. +Require Export Coq.Lists.List. +Export List.ListNotations. + +Record CFGV := { Terminal : Type; VarSym : Type }. + +Section Gram. + Context {G : CFGV}. + + Inductive Pattern : (Terminal G) -> Type := + | ptleaf : forall (T : Terminal G), + nat -> Pattern T + with Mixture : list (Terminal G) -> Type := + | mtcons : forall {h: Terminal G} + {tl: list (Terminal G)}, + Pattern h -> Mixture tl -> Mixture (h::tl). + + Variable vc : VarSym G. + + Fixpoint pBVars {gs} (p : Pattern gs) : (list nat) := + match p with + | ptleaf _ _ => [] + end + with mBVars {lgs} (pts : Mixture lgs) : (list nat) := + match pts with + | mtcons _ _ _ tl => mBVars tl + end. + + Lemma mBndngVarsAsNth : + forall mp (m : @Mixture mp), + mBVars m = [2]. + Proof. + intros. + induction m. progress simpl. + Admitted. +End Gram. + +Lemma mBndngVarsAsNth' {G : CFGV} { vc : VarSym G} : + forall mp (m : @Mixture G mp), + mBVars m = [2]. +Proof. + intros. + induction m. + Fail progress simpl. + (* simpl did nothing here, while it does something inside the section; this is probably a bug*) -- cgit v1.2.3