diff options
| author | Hugo Herbelin | 2020-11-03 02:11:33 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-04 17:33:43 +0100 |
| commit | 091bfff6ce37a303550e79abb23fdc992a28f7e3 (patch) | |
| tree | 1c58695f2aa1d658fde2ff09a90c267cb0e2dc9a | |
| parent | 7f90e6e0aa8dd27c64bac0dbc4b247ebb33d4aca (diff) | |
Fixes #13298: primitive projections needs a correct typing environment.
| -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 |
3 files changed, 13 insertions, 11 deletions
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 |