Skip to content

Commit

Permalink
Merge pull request #702 from SkySkimmer/keep-force
Browse files Browse the repository at this point in the history
Adapt to coq/coq#19709 (libobject requires explicit classification)
  • Loading branch information
gares authored Oct 22, 2024
2 parents 4b55e8e + d6fbdeb commit c7fcee1
Showing 1 changed file with 5 additions and 0 deletions.
5 changes: 5 additions & 0 deletions src/coq_elpi_programs.ml
Original file line number Diff line number Diff line change
Expand Up @@ -304,6 +304,7 @@ let in_source : Names.Id.t -> string option * EC.compilation_unit * EC.flags ->
cache_function = cache;
open_function = simple_open import;
discharge_function = (fun o -> Some o);
classify_function = (fun _ -> Keep);
}
;;

Expand Down Expand Up @@ -495,6 +496,7 @@ let get ?(fail_if_not_exists=false) p =
let open Libobject in
declare_object { (default_object "ELPI-LP-COMMAND") with
load_function = (fun _ x -> lp_command_ast := Some x);
classify_function = (fun _ -> Keep);
}
let load_command s =
let elpi = ensure_initialized () in
Expand All @@ -514,6 +516,7 @@ let get ?(fail_if_not_exists=false) p =
let open Libobject in
declare_object { (default_object "ELPI-LP-TACTIC") with
load_function = (fun _ x -> lp_tactic_ast := Some x);
classify_function = (fun _ -> Keep);
}
let load_tactic s =
let elpi = ensure_initialized () in
Expand Down Expand Up @@ -548,6 +551,7 @@ let get ?(fail_if_not_exists=false) p =
let open Libobject in
declare_object { (default_object "ELPI-LP-CHECKER") with
load_function = (fun _ x -> lp_checker_ast := Some x);
classify_function = (fun _ -> Keep);
}

let load_checker s =
Expand All @@ -566,6 +570,7 @@ let get ?(fail_if_not_exists=false) p =
let open Libobject in
declare_object { (default_object "ELPI-LP-PRINTER") with
load_function = (fun _ x -> lp_printer_ast := Some x);
classify_function = (fun _ -> Keep);
}
let load_printer s =
let elpi = ensure_initialized () in
Expand Down

0 comments on commit c7fcee1

Please sign in to comment.