aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/classes.ml2
-rw-r--r--vernac/comHints.ml30
-rw-r--r--vernac/comSearch.ml11
-rw-r--r--vernac/declare.ml7
-rw-r--r--vernac/declaremods.mli2
-rw-r--r--vernac/egramcoq.ml4
-rw-r--r--vernac/library.ml4
-rw-r--r--vernac/search.ml20
-rw-r--r--vernac/vernacentries.ml10
9 files changed, 55 insertions, 35 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 3b69273570..054addc542 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -57,7 +57,7 @@ let is_local_for_hint i =
let add_instance_base inst =
let locality = if is_local_for_hint inst then Goptions.OptLocal else Goptions.OptGlobal in
- add_instance_hint (Hints.IsGlobRef inst.is_impl) [inst.is_impl] ~locality
+ add_instance_hint (Hints.hint_globref inst.is_impl) [inst.is_impl] ~locality
inst.is_info
let mk_instance cl info glob impl =
diff --git a/vernac/comHints.ml b/vernac/comHints.ml
index 9eac558908..f642411fa4 100644
--- a/vernac/comHints.ml
+++ b/vernac/comHints.ml
@@ -62,7 +62,7 @@ let project_hint ~poly pri l2r r =
cb
in
let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in
- (info, true, Hints.PathAny, Hints.IsGlobRef (GlobRef.ConstRef c))
+ (info, true, Hints.PathAny, Hints.hint_globref (GlobRef.ConstRef c))
let warn_deprecated_hint_constr =
CWarnings.create ~name:"fragile-hint-constr" ~category:"automation"
@@ -84,16 +84,6 @@ let soft_evaluable =
let interp_hints ~poly h =
let env = Global.env () in
let sigma = Evd.from_env env in
- let f poly c =
- let evd, c = Constrintern.interp_open_constr env sigma c in
- let env = Global.env () in
- let sigma = Evd.from_env env in
- let c, diff = Hints.prepare_hint true env sigma (evd, c) in
- if poly then (Hints.IsConstr (c, Some diff) [@ocaml.warning "-3"])
- else
- let () = DeclareUctx.declare_universe_context ~poly:false diff in
- (Hints.IsConstr (c, None) [@ocaml.warning "-3"])
- in
let fref r =
let gr = Smartlocate.global_with_alias r in
Dumpglob.add_glob ?loc:r.CAst.loc gr;
@@ -106,10 +96,22 @@ let interp_hints ~poly h =
match c with
| HintsReference c ->
let gr = Smartlocate.global_with_alias c in
- (PathHints [gr], IsGlobRef gr)
+ (PathHints [gr], hint_globref gr)
| HintsConstr c ->
let () = warn_deprecated_hint_constr () in
- (PathAny, f poly c)
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ let c, uctx = Constrintern.interp_constr env sigma c in
+ let subst, uctx = UState.normalize_variables uctx in
+ let c = EConstr.Vars.subst_univs_constr subst c in
+ let diff = UState.context_set uctx in
+ let c =
+ if poly then (c, Some diff)
+ else
+ let () = DeclareUctx.declare_universe_context ~poly:false diff in
+ (c, None)
+ in
+ (PathAny, Hints.hint_constr c) [@ocaml.warning "-3"]
in
let fp = Constrintern.intern_constr_pattern env sigma in
let fres (info, b, r) =
@@ -149,7 +151,7 @@ let interp_hints ~poly h =
( empty_hint_info
, true
, PathHints [gr]
- , IsGlobRef gr ))
+ , hint_globref gr ))
in
HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid))
| HintsExtern (pri, patcom, tacexp) ->
diff --git a/vernac/comSearch.ml b/vernac/comSearch.ml
index 9de8d6fbc3..f3b21eb813 100644
--- a/vernac/comSearch.ml
+++ b/vernac/comSearch.ml
@@ -53,7 +53,16 @@ let kind_searcher = Decls.(function
let interp_search_item env sigma =
function
| SearchSubPattern ((where,head),pat) ->
- let _,pat = Constrintern.intern_constr_pattern env sigma pat in
+ let expected_type = Pretyping.(if head then IsType else WithoutTypeConstraint) in
+ let pat =
+ try Constrintern.interp_constr_pattern env sigma ~expected_type pat
+ with e when CErrors.noncritical e ->
+ (* We cannot ensure (yet?) that a typable pattern will
+ actually be typed, consider e.g. (forall A, A -> A /\ A)
+ which fails, not seeing that A can be Prop; so we use an
+ untyped pattern as a fallback (i.e w/o no insertion of
+ coercions, no compilation of pattern-matching) *)
+ snd (Constrintern.intern_constr_pattern env sigma ~as_type:head pat) in
GlobSearchSubPattern (where,head,pat)
| SearchString ((Anywhere,false),s,None) when Id.is_valid s ->
GlobSearchString s
diff --git a/vernac/declare.ml b/vernac/declare.ml
index a97081ea02..1e8771b641 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -2499,7 +2499,12 @@ let admit_obligations ~pm n =
let next_obligation ~pm n tac =
let prg = match n with
- | None -> State.first_pending pm |> Option.get
+ | None ->
+ begin match State.first_pending pm with
+ | Some prg -> prg
+ | None ->
+ Error.no_obligations None
+ end
| Some _ -> get_unique_prog ~pm n
in
let {obls; remaining} = Internal.get_obligations prg in
diff --git a/vernac/declaremods.mli b/vernac/declaremods.mli
index 9ca2ca5593..a1b98e4d9c 100644
--- a/vernac/declaremods.mli
+++ b/vernac/declaremods.mli
@@ -86,7 +86,7 @@ val start_library : library_name -> unit
val end_library :
?except:Future.UUIDSet.t -> output_native_objects:bool -> library_name ->
- Safe_typing.compiled_library * library_objects * Safe_typing.native_library
+ Safe_typing.compiled_library * library_objects * Nativelib.native_library
(** append a function to be executed at end_library *)
val append_end_library_hook : (unit -> unit) -> unit
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/library.ml b/vernac/library.ml
index e580927bfd..8a9b1fd68d 100644
--- a/vernac/library.ml
+++ b/vernac/library.ml
@@ -160,7 +160,7 @@ let register_loaded_library m =
let prefix = Nativecode.mod_uid_of_dirpath libname ^ "." in
let f = prefix ^ "cmo" in
let f = Dynlink.adapt_filename f in
- Nativelib.link_library (Global.env()) ~prefix ~dirname ~basename:f
+ Nativelib.link_library ~prefix ~dirname ~basename:f
in
let rec aux = function
| [] ->
@@ -502,7 +502,7 @@ let save_library_to todo_proofs ~output_native_objects dir f otab =
(* Writing native code files *)
if output_native_objects then
let fn = Filename.dirname f ^"/"^ Nativecode.mod_uid_of_dirpath dir in
- Nativelib.compile_library dir ast fn
+ Nativelib.compile_library ast fn
let save_library_raw f sum lib univs proofs =
save_library_base f sum lib (Some univs) None proofs
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 2ca414b453..824bf35b1d 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 16:52:57 +0000