diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/egramcoq.ml | 4 | ||||
| -rw-r--r-- | vernac/search.ml | 20 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 10 |
3 files changed, 19 insertions, 15 deletions
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index 123ea2c24e..efe4e17d0b 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -408,8 +408,8 @@ match e with | TTClosedBinderList _ -> { subst with binderlists = List.flatten v :: subst.binderlists } | TTBigint -> begin match forpat with - | ForConstr -> push_constr subst (CAst.make @@ CPrim (Numeral (NumTok.Signed.of_int_string v))) - | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (Numeral (NumTok.Signed.of_int_string v))) + | ForConstr -> push_constr subst (CAst.make @@ CPrim (Number (NumTok.Signed.of_int_string v))) + | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (Number (NumTok.Signed.of_int_string v))) end | TTReference -> begin match forpat with 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 diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index bc03994ca6..ef8631fbb6 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -985,9 +985,15 @@ let interp_filter_in m = function let vernac_import export refl = let import_mod (qid,f) = - let m = try Nametab.locate_module qid + let loc = qid.loc in + let m = try + let m = Nametab.locate_module qid in + let () = if Modops.is_functor (Global.lookup_module m).Declarations.mod_type + then CErrors.user_err ?loc Pp.(str "Cannot import functor " ++ pr_qualid qid ++ str".") + in + m with Not_found -> - CErrors.user_err Pp.(str "Cannot find module " ++ pr_qualid qid) + CErrors.user_err ?loc Pp.(str "Cannot find module " ++ pr_qualid qid) in let f = interp_filter_in m f in Declaremods.import_module f ~export m |