diff options
| -rw-r--r-- | pretyping/constrMatching.ml | 53 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3561.v | 23 |
2 files changed, 55 insertions, 21 deletions
diff --git a/pretyping/constrMatching.ml b/pretyping/constrMatching.ml index 3a5431eed..e23a4e440 100644 --- a/pretyping/constrMatching.ml +++ b/pretyping/constrMatching.ml @@ -353,26 +353,32 @@ let authorized_occ env sigma partial_app closed pat c mk_ctx next = (* Tries to match a subterm of [c] with [pat] *) let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = - let rec aux c mk_ctx next = + let rec aux env c mk_ctx next = match kind_of_term c with | Cast (c1,k,c2) -> let next_mk_ctx lc = mk_ctx (mkCast (List.hd lc, k,c2)) in - let next () = try_aux [c1] next_mk_ctx next in + let next () = try_aux [env] [c1] next_mk_ctx next in authorized_occ env sigma partial_app closed pat c mk_ctx next | Lambda (x,c1,c2) -> let next_mk_ctx lc = mk_ctx (mkLambda (x,List.hd lc,List.nth lc 1)) in - let next () = try_aux [c1;c2] next_mk_ctx next in + let next () = + let env' = Environ.push_rel (x,None,c1) env in + try_aux [env;env'] [c1; c2] next_mk_ctx next in authorized_occ env sigma partial_app closed pat c mk_ctx next | Prod (x,c1,c2) -> let next_mk_ctx lc = mk_ctx (mkProd (x,List.hd lc,List.nth lc 1)) in - let next () = try_aux [c1;c2] next_mk_ctx next in + let next () = + let env' = Environ.push_rel (x,None,c1) env in + try_aux [env;env'] [c1;c2] next_mk_ctx next in authorized_occ env sigma partial_app closed pat c mk_ctx next | LetIn (x,c1,t,c2) -> let next_mk_ctx = function | [c1;c2] -> mkLetIn (x,c1,t,c2) | _ -> assert false in - let next () = try_aux [c1;c2] next_mk_ctx next in + let next () = + let env' = Environ.push_rel (x,Some c1,t) env in + try_aux [env;env'] [c1;c2] next_mk_ctx next in authorized_occ env sigma partial_app closed pat c mk_ctx next | App (c1,lc) -> let next () = @@ -384,24 +390,24 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = let mk_ctx = function | [app';c] -> mk_ctx (mkApp (app',[|c|])) | _ -> assert false in - try_aux [app;Array.last lc] mk_ctx next + try_aux [env] [app;Array.last lc] mk_ctx next else let rec aux2 app args next = match args with | [] -> let mk_ctx le = mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in - try_aux (c1::Array.to_list lc) mk_ctx next + try_aux [env] (c1::Array.to_list lc) mk_ctx next | arg :: args -> let app = mkApp (app,[|arg|]) in let next () = aux2 app args next in let mk_ctx ce = mk_ctx (mkApp (ce, Array.of_list args)) in - aux app mk_ctx next in + aux env app mk_ctx next in aux2 c1 (Array.to_list lc) next else let mk_ctx le = mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in - try_aux (c1::Array.to_list lc) mk_ctx next + try_aux [env] (c1::Array.to_list lc) mk_ctx next in authorized_occ env sigma partial_app closed pat c mk_ctx next | Case (ci,hd,c1,lc) -> @@ -409,7 +415,7 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = | [] -> assert false | c1 :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc)) in - let next () = try_aux (c1 :: Array.to_list lc) next_mk_ctx next in + let next () = try_aux [env] (c1 :: Array.to_list lc) next_mk_ctx next in authorized_occ env sigma partial_app closed pat c mk_ctx next | Fix (indx,(names,types,bodies)) -> let nb_fix = Array.length types in @@ -418,7 +424,7 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = mk_ctx (mkFix (indx,(names, Array.of_list ntypes, Array.of_list nbodies))) in let next () = try_aux - ((Array.to_list types)@(Array.to_list bodies)) next_mk_ctx next in + [env] ((Array.to_list types)@(Array.to_list bodies)) next_mk_ctx next in authorized_occ env sigma partial_app closed pat c mk_ctx next | CoFix (i,(names,types,bodies)) -> let nb_fix = Array.length types in @@ -426,26 +432,31 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = let (ntypes,nbodies) = CList.chop nb_fix le in mk_ctx (mkCoFix (i,(names, Array.of_list ntypes, Array.of_list nbodies))) in let next () = - try_aux ((Array.to_list types)@(Array.to_list bodies)) next_mk_ctx next in + try_aux [env] ((Array.to_list types)@(Array.to_list bodies)) next_mk_ctx next in authorized_occ env sigma partial_app closed pat c mk_ctx next | Proj (p,c') -> let next_mk_ctx le = mk_ctx (mkProj (p,List.hd le)) in - let next () = try_aux [c'] next_mk_ctx next in + let next () = try_aux [env] [c'] next_mk_ctx next in authorized_occ env sigma partial_app closed pat c mk_ctx next | Construct _| Ind _|Evar _|Const _ | Rel _|Meta _|Var _|Sort _ -> authorized_occ env sigma partial_app closed pat c mk_ctx next (* Tries [sub_match] for all terms in the list *) - and try_aux lc mk_ctx next = - let rec try_sub_match_rec lacc = function - | [] -> next () - | c::tl -> + and try_aux lenv lc mk_ctx next = + let rec try_sub_match_rec lacc lenv lc = + match lenv, lc with + | _, [] -> next () + | env :: tlenv, c::tl -> let mk_ctx ce = mk_ctx (List.rev_append lacc (ce::tl)) in - let next () = try_sub_match_rec (c::lacc) tl in - aux c mk_ctx next in - try_sub_match_rec [] lc in + let next () = + let env' = match tlenv with [] -> lenv | _ -> tlenv in + try_sub_match_rec (c::lacc) env' tl + in + aux env c mk_ctx next + | _ -> assert false in + try_sub_match_rec [] lenv lc in let lempty () = IStream.Nil in - let result () = aux c (fun x -> x) lempty in + let result () = aux env c (fun x -> x) lempty in IStream.thunk result let match_subterm env sigma pat c = sub_match env sigma pat c diff --git a/test-suite/bugs/closed/3561.v b/test-suite/bugs/closed/3561.v new file mode 100644 index 000000000..b4dfd17f5 --- /dev/null +++ b/test-suite/bugs/closed/3561.v @@ -0,0 +1,23 @@ +(* File reduced by coq-bug-finder from original input, then from 6343 lines to 2362 lines, then from 2115 lines to 303 lines, then from 321 lines to 90 lines, then from 95 lines to 41 lines *) +(* coqc version trunk (August 2014) compiled on Aug 31 2014 10:12:32 with OCaml 4.01.0 + coqtop version cagnode17:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (437b91a3ffd7327975a129b95b24d3f66ad7f3e4) *) +Set Primitive Projections. +Set Implicit Arguments. +Record prod (A B : Type) := pair { fst : A ; snd : B }. +Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope. +Arguments idpath {A a} , [A] a. +Axiom transport : forall {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x), P y. +Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing). +Lemma ap_transport {A} {P Q : A -> Type} {x y : A} (p : x = y) (f : forall x, P x -> Q x) (z : P x) : + f y (p # z) = (p # (f x z)). +Proof. admit. +Defined. +Lemma foo A B (f : A * B -> A) : f = f. +Admitted. +Goal forall (H0 H2 : Type) x p, + @transport (prod H0 H2) + (fun GO : prod H0 H2 => x (fst GO)) = p. + intros. + match goal with + | [ |- context[x (?f _)] ] => set(foo':=f) + end.
\ No newline at end of file |