diff options
| -rw-r--r-- | doc/changelog/07-commands-and-options/13301-master+fix13298-bad-env-search-primitive-projections.rst | 5 | ||||
| -rw-r--r-- | test-suite/output/Search_bug13298.out | 1 | ||||
| -rw-r--r-- | test-suite/output/Search_bug13298.v | 3 | ||||
| -rw-r--r-- | vernac/search.ml | 20 |
4 files changed, 18 insertions, 11 deletions
diff --git a/doc/changelog/07-commands-and-options/13301-master+fix13298-bad-env-search-primitive-projections.rst b/doc/changelog/07-commands-and-options/13301-master+fix13298-bad-env-search-primitive-projections.rst new file mode 100644 index 0000000000..97ea1b9aa9 --- /dev/null +++ b/doc/changelog/07-commands-and-options/13301-master+fix13298-bad-env-search-primitive-projections.rst @@ -0,0 +1,5 @@ +- **Fixed:** + Failures of :cmd:`Search` in the presence of primitive projections + (`#13301 <https://github.com/coq/coq/pull/13301>`_, + fixes `#13298 <https://github.com/coq/coq/issues/13298>`_, + by Hugo Herbelin). diff --git a/test-suite/output/Search_bug13298.out b/test-suite/output/Search_bug13298.out new file mode 100644 index 0000000000..18488c790f --- /dev/null +++ b/test-suite/output/Search_bug13298.out @@ -0,0 +1 @@ +snd: forall c : c, fst c = 0 diff --git a/test-suite/output/Search_bug13298.v b/test-suite/output/Search_bug13298.v new file mode 100644 index 0000000000..9a75321c64 --- /dev/null +++ b/test-suite/output/Search_bug13298.v @@ -0,0 +1,3 @@ +Set Primitive Projections. +Record c : Type := { fst : nat; snd : fst = 0 }. +Search concl:fst. diff --git a/vernac/search.ml b/vernac/search.ml index abefeab779..501e5b1a91 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -216,18 +216,16 @@ let name_of_reference ref = Id.to_string (Nametab.basename_of_global ref) let search_filter query gr kind env sigma typ = match query with | GlobSearchSubPattern (where,head,pat) -> let open Context.Rel.Declaration in - let collect_hyps ctx = - List.fold_left (fun acc d -> match get_value d with - | None -> get_type d :: acc - | Some b -> b :: get_type d :: acc) [] ctx in + let rec collect env hyps typ = + match Constr.kind typ with + | LetIn (na,b,t,c) -> collect (push_rel (LocalDef (na,b,t)) env) ((env,b) :: (env,t) :: hyps) c + | Prod (na,t,c) -> collect (push_rel (LocalAssum (na,t)) env) ((env,t) :: hyps) c + | _ -> (hyps,(env,typ)) in let typl= match where with - | InHyp -> collect_hyps (fst (Term.decompose_prod_assum typ)) - | InConcl -> [snd (Term.decompose_prod_assum typ)] - | Anywhere -> - if head then - let ctx, ccl = Term.decompose_prod_assum typ in ccl :: collect_hyps ctx - else [typ] in - List.exists (fun typ -> + | InHyp -> fst (collect env [] typ) + | InConcl -> [snd (collect env [] typ)] + | Anywhere -> if head then let hyps, ccl = collect env [] typ in ccl :: hyps else [env,typ] in + List.exists (fun (env,typ) -> let f = if head then Constr_matching.is_matching_head else Constr_matching.is_matching_appsubterm ~closed:false in |