diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 2fb4596..2e741ae 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -5,9 +5,10 @@ on: [push, pull_request] jobs: build: strategy: + fail-fast: false matrix: runs-on: [ ubuntu-latest ] - rocq_version: [ dev ] + rocq_version: [ "9.0", "9.1", "9.2", dev ] runs-on: ${{ matrix.runs-on }} steps: diff --git a/dune-project b/dune-project index 778f462..0a1a015 100644 --- a/dune-project +++ b/dune-project @@ -1,9 +1,12 @@ -(lang dune 3.21) - -(name mltac2) +(lang dune 3.17) (generate_opam_files true) +;; Work-around for Dune 3.17 subst bug: https://github.com/ocaml/dune/issues/11045 +;; LATER: bump to Dune 3.21 once we no longer use Rocq 9.2 in CI +(subst disabled) + +(name mltac2) (authors "Dario Halilovic" "Pierre-Marie Pédrot") (maintainers "Dario Halilovic") (license LGPL-2.1-only) @@ -17,4 +20,5 @@ (name mltac2) (synopsis "Ltac2 APIs in OCaml") (depends - rocq-runtime)) + (coq-core (>= 9.0)) ;; Use coq-core to obtain coqc compatibility binaries + ppx_optcomp)) diff --git a/mltac2.opam b/mltac2.opam index 16db60b..916c320 100644 --- a/mltac2.opam +++ b/mltac2.opam @@ -7,12 +7,12 @@ license: "LGPL-2.1-only" homepage: "https://github.com/epfl-systemf/mltac2" bug-reports: "https://github.com/epfl-systemf/mltac2/issues" depends: [ - "dune" {>= "3.21"} - "rocq-runtime" + "dune" {>= "3.17"} + "coq-core" {>= "9.0"} + "ppx_optcomp" "odoc" {with-doc} ] build: [ - ["dune" "subst"] {dev} [ "dune" "build" @@ -26,4 +26,3 @@ build: [ ] ] dev-repo: "git+https://github.com/epfl-systemf/mltac2.git" -x-maintenance-intent: ["(latest)"] diff --git a/src/dune b/src/dune index 35c18bc..e2011f3 100644 --- a/src/dune +++ b/src/dune @@ -1,5 +1,6 @@ (library (name mltac2) (public_name mltac2) - (libraries - rocq-runtime.plugins.ltac2)) + (libraries rocq-runtime.plugins.ltac2) + ;; LATER: Replace coq: by rocq: once Dune >= 3.21 + (preprocess (pps ppx_optcomp -- -cookie "ppx_optcomp.env=env ~rocq:(Defined (%{coq:version.major}, %{coq:version.minor}))"))) diff --git a/src/ltac2.ml b/src/ltac2.ml index 396cddd..5d85997 100644 --- a/src/ltac2.ml +++ b/src/ltac2.ml @@ -10,7 +10,35 @@ open Tac2types open Proofview.Notations let return = Proofview.tclUNIT -let throw = Tac2core.throw + +[%%if rocq >= (9, 1)] +let to_fun1 _ _ (f : 'a -> 'b) : ('a, 'b) Tac2ffi.fun1 = + fun x -> return (f x) + +let to_fun1' _ _ (f : 'a -> 'b Proofview.tactic) : ('a, 'b) Tac2ffi.fun1 = + f +[%%else] +let to_fun1 (from_t : 'a Tac2ffi.repr) (to_t : 'b Tac2ffi.repr) (f : 'a -> 'b): ('a, 'b) Tac2ffi.fun1 = + let f = Tac2val.mk_closure_val Tac2val.arity_one (fun x -> + let x = Tac2ffi.repr_to from_t x in + return (Tac2ffi.repr_of to_t (f x))) + in + Tac2ffi.to_fun1 from_t to_t f + +let to_fun1' (from_t : 'a Tac2ffi.repr) (to_t : 'b Tac2ffi.repr) (f : 'a -> 'b Proofview.tactic): ('a, 'b) Tac2ffi.fun1 = + let f = Tac2val.mk_closure_val Tac2val.arity_one (fun x -> + let x = Tac2ffi.repr_to from_t x in + f x >>= fun y -> + return (Tac2ffi.repr_of to_t y)) + in + Tac2ffi.to_fun1 from_t to_t f +[%%endif] + +let thunk ret_t (x : 'a) : (unit, 'a) Tac2ffi.fun1 = + to_fun1 Tac2ffi.unit ret_t (fun () -> x) + +let thunk' ret_t (x : 'a Proofview.tactic) : (unit, 'a) Tac2ffi.fun1 = + to_fun1' Tac2ffi.unit ret_t (fun () -> x) (** {1 Ltac2 APIs} *) @@ -33,15 +61,19 @@ module Ltac2Message = struct let of_lconstr env sigma c = Printer.pr_leconstr_env env sigma c + [%%if rocq >= (9, 2)] let of_preterm env sigma c = Printer.pr_closed_glob_env env sigma c let of_lpreterm env sigma c = Printer.pr_closed_lglob_env env sigma c + [%%endif] let of_ident = Id.print + [%%if rocq >= (9, 2)] let of_exninfo = CErrors.print_extra + [%%endif] let concat = Pp.app @@ -125,7 +157,11 @@ module Ltac2Constr = struct end module Binder = struct + [%%if rocq >= (9, 1)] type t = Tac2ffi.binder + [%%else] + type t = (Names.Name.t EConstr.binder_annot * EConstr.types) + [%%endif] type relevance = Sorts.relevance let make env sigma na ty = @@ -161,6 +197,7 @@ module Ltac2Constr = struct module Flags = struct type t = Pretyping.inference_flags + [%%if rocq >= (9, 2)] let constr_flags = { use_coercions = true; use_typeclasses = Pretyping.UseTC; @@ -172,6 +209,20 @@ module Ltac2Constr = struct undeclared_evars_rr = false; unconstrained_sorts = false; } + [%%else] + let constr_flags = { + use_coercions = true; + use_typeclasses = Pretyping.UseTC; + solve_unification_constraints = true; + fail_evar = true; + expand_evars = true; + program_mode = false; + polymorphic = false; + undeclared_evars_patvars = false; + patvars_abstract = false; + unconstrained_sorts = false; + } + [%%endif] let set_use_coercion b (flags: t) = { flags with use_coercions = b } @@ -224,20 +275,28 @@ module Ltac2Pattern = struct type context = Constr_matching.context let empty_context = Constr_matching.empty_context + [%%if rocq >= (9, 2)] + let instantiate_pattern _ _ pat = + pat + [%%else] + let instantiate_pattern env sigma pat = + Constr_matching.instantiate_pattern env sigma Id.Map.empty pat + [%%endif] + let matches env sigma pat c = try Some (Constr_matching.matches env sigma pat c) with Constr_matching.PatternMatchingFailure -> None let matches_subterm pat c = - let open Constr_matching in let rec of_ans s = match IStream.peek s with | IStream.Nil -> Proofview.tclZERO Constr_matching.PatternMatchingFailure - | IStream.Cons ({ m_sub = (_, sub); m_ctx }, s) -> + | IStream.Cons (Constr_matching.{ m_sub = (_, sub); m_ctx }, s) -> Proofview.tclOR (return (m_ctx, sub)) (fun _ -> of_ans s) in (* Use pf_apply to match in the current goal *) Tac2core.pf_apply begin fun env sigma -> - let ans = Constr_matching.match_subterm env sigma (Id.Set.empty,pat) c in + let pat = instantiate_pattern env sigma pat in + let ans = Constr_matching.match_subterm env sigma (Id.Set.empty, pat) c in of_ans ans end @@ -324,9 +383,16 @@ module Ltac2Control = struct let goal = Proofview.Goal.enter_one (fun goal -> return (Proofview.Goal.concl goal)) + [%%if rocq >= (9, 2)] let hyp env id = if Environ.mem_named id env then Ok (EConstr.mkVar id) else Error () + [%%else] + let hyp env id = + let has_hyp = try ignore (Environ.lookup_named id env); true with Not_found -> false in + if has_hyp then Ok (EConstr.mkVar id) + else Error () + [%%endif] let hyp_value env id = match EConstr.lookup_named id env with @@ -372,24 +438,35 @@ end module Ltac2Fresh = struct module Free = struct + [%%if rocq >= (9, 1)] type t = Nameops.Fresh.t let empty = Nameops.Fresh.empty let add = Nameops.Fresh.add let union = Nameops.Fresh.union + [%%else] + type t = Id.Set.t - let of_ids ids = List.fold_right Nameops.Fresh.add ids Nameops.Fresh.empty + let empty = Id.Set.empty + + let add = Id.Set.add + + let union = Id.Set.union + [%%endif] + + let of_ids ids = List.fold_right add ids empty let of_constr sigma c = let rec fold accu c = match EConstr.kind sigma c with - | Constr.Var id -> Nameops.Fresh.add id accu + | Constr.Var id -> add id accu | _ -> EConstr.fold sigma fold accu c in - fold Nameops.Fresh.empty c + fold empty c end + [%%if rocq >= (9, 1)] (* for backwards compat reasons the ocaml and ltac2 APIs exchange the meaning of "fresh" and "next" *) let next avoid id = @@ -399,6 +476,10 @@ module Ltac2Fresh = struct let fresh avoid id = let id = Namegen.mangle_id id in Nameops.Fresh.next id avoid + [%%else] + let fresh avoid id = + Namegen.next_ident_away_from id (fun id -> Id.Set.mem id avoid) + [%%endif] end (** {2 Environment} *) @@ -454,9 +535,15 @@ module Ltac2Ind = struct let nparams_uniform (_, mib) = mib.Declarations.mind_nparams_rec + [%%if rocq = (9, 2)] + let get_projections (ind,mib) = + Declareops.inductive_make_projections ind mib + |> Option.map (fun (x, _) -> Array.map (fun (p,_) -> Projection.make p false) x) + [%%else] let get_projections (ind,mib) = Declareops.inductive_make_projections ind mib |> Option.map (Array.map (fun (p,_) -> Projection.make p false)) + [%%endif] let constructor_nargs ((_,i),mib) = let open Declarations in @@ -486,6 +573,8 @@ module Ltac2Constructor = struct Nametab.pr_global_env Id.Set.empty (ConstructRef ctor) end +[%%if rocq >= (9, 3)] + (** {2 Schemes} *) module Ltac2Scheme = struct @@ -521,6 +610,7 @@ module Ltac2Scheme = struct let case_nodep = "case_nodep" let case_dep = "case_dep" end +[%%endif] (** {2 Projection} *) @@ -540,14 +630,22 @@ module Ltac2Proj = struct let to_constant p = Some (Projection.repr p) + [%%if rocq > (9, 2)] let print p = Nametab.pr_global_env Id.Set.empty (ConstRef (Environ.projection_repr_constant (Global.env ()) (Projection.repr p))) + [%%else] + let print p = + Nametab.pr_global_env + Id.Set.empty + (ConstRef (Projection.constant p)) + [%%endif] end (** {2 Module} *) +[%%if rocq >= (9, 2)] module Ltac2Module = struct type t = ModPath.t let equal = ModPath.equal @@ -694,9 +792,11 @@ module Ltac2Module = struct in Option.map (List.map to_field) body end +[%%endif] (** {2 Rewriting} *) +[%%if rocq >= (9, 1)] module Ltac2Rewrite = struct module Strategy = struct type t = Rewrite.strategy @@ -725,19 +825,23 @@ module Ltac2Rewrite = struct let lemmas = Tac2tactics.RewriteStrats.lemmas let fold = Rewrite.Strategies.fold let eval = Rewrite.Strategies.reduce + [%%if rocq >= (9, 3)] let matches = Rewrite.Strategies.matches + [%%endif] + [%%if rocq >= (9, 3)] let tactic = Tac2tactics.wrap_tactic_call + [%%endif] end let rewrite_strat ?in_hyp s = Tac2tactics.rewrite_strat s in_hyp end +[%%endif] (** {2 Transparent state} *) module Ltac2TransparentState = struct type t = TransparentState.t - type strategy_level = Conv_oracle.level open TransparentState @@ -794,7 +898,10 @@ module Ltac2TransparentState = struct let mem_proj p ts = PRpred.mem (Projection.repr p) ts.tr_prj let mem_var v ts = Id.Pred.mem v ts.tr_var + [%%if rocq >= (9, 3)] + type strategy_level = Conv_oracle.level let with_strategy level grs tac = Tac2tactics.with_strategy level grs (fun () -> tac) + [%%endif] end (** {2 Unification} *) @@ -821,7 +928,11 @@ module Ltac2Std = struct type clause = Tac2types.clause type reference = GlobRef.t type strength = Genredexpr.strength + [%%if rocq >= (9, 2)] type red_flags = Tac2types.red_flag + [%%else] + type red_flags = reference Genredexpr.glob_red_flag + [%%endif] type intro_pattern = Tac2types.intro_pattern and intro_pattern_naming = Tac2types.intro_pattern_naming and intro_pattern_action = Tac2types.intro_pattern_action @@ -843,7 +954,7 @@ module Ltac2Std = struct let intros ?(e = false) ?(patterns = []) () = Tac2tactics.intros_patterns e patterns let apply ?(e = false) ?in_hyp_as bindings = - let bindings = List.map (fun c -> fun () -> return c) bindings in + let bindings = List.map (thunk Tac2extffi.constr_with_bindings) bindings in Tac2tactics.apply true e bindings in_hyp_as let elim ?(e = false) ?using c = Tac2tactics.elim e c using @@ -876,6 +987,7 @@ module Ltac2Std = struct let exfalso = Tactics.exfalso + [%%if rocq >= (9, 1)] module Red = struct type t = Redexpr.red_expr @@ -895,13 +1007,14 @@ module Ltac2Std = struct let eval_in = Tac2tactics.reduce_in let eval = Tac2tactics.reduce_constr + [%%endif] let change ?pattern ?(where = default_on_conclusion) f = + let f = to_fun1' Tac2ffi.(array constr) Tac2ffi.constr f in Tac2tactics.change pattern f where let rewrite ?(e = false) ?(where = default_on_conclusion) ?by rewrites = - (* Thunk the tactic. *) - let by = Option.map (fun by -> fun () -> by) by in + let by = Option.map (thunk' Tac2ffi.unit) by in Tac2tactics.rewrite e rewrites where by let setoid_rewrite ?(ltr = true) ?in_hyp t where = Tac2tactics.setoid_rewrite ltr (return t) where in_hyp @@ -945,8 +1058,13 @@ module Ltac2Std = struct let revert = Generalize.revert let admit = Proofview.give_up + [%%if rocq >= (9, 2)] let fix = FixTactics.fix let cofix = FixTactics.cofix + [%%else] + let fix = Tactics.fix + let cofix = Tactics.cofix + [%%endif] let clear = Tactics.clear let keep = Tactics.keep @@ -959,8 +1077,7 @@ module Ltac2Std = struct let contradiction ?witness () = Tac2tactics.contradiction witness let autorewrite ~all ?(where = default_on_conclusion) ?using dbs = - (* Thunk the tactic *) - let using = Option.map (fun using -> fun () -> using) using in + let using = Option.map (thunk' Tac2ffi.unit) using in Tac2tactics.autorewrite ~all using dbs where let subst ?hyps () = @@ -983,7 +1100,11 @@ module Ltac2Std = struct let congruence ?n ?hints () = Tac2tactics.congruence n hints let simple_congruence ?n ?hints () = Tac2tactics.simple_congruence n hints + [%%if rocq >= (9, 1)] let f_equal = Tac2tactics.f_equal + [%%else] + let f_equal = Cc_core_plugin.Cctac.f_equal + [%%endif] end (** {1 Ltac2 API} *) @@ -1017,11 +1138,17 @@ module Fresh = Ltac2Fresh module Ident = Ltac2Ident module Ind = Ltac2Ind module Message = Ltac2Message +[%%if rocq >= (9, 2)] module Module = Ltac2Module +[%%endif] module Pattern = Ltac2Pattern module Proj = Ltac2Proj +[%%if rocq >= (9, 1)] module Rewrite = Ltac2Rewrite +[%%endif] +[%%if rocq >= (9, 3)] module Scheme = Ltac2Scheme +[%%endif] module Std = Ltac2Std module TransparentState = Ltac2TransparentState module Unification = Ltac2Unification diff --git a/src/ltac2.mli b/src/ltac2.mli index 968c28c..d0962f6 100644 --- a/src/ltac2.mli +++ b/src/ltac2.mli @@ -102,10 +102,10 @@ module Constr : sig (** Low-level access to kernel terms. Use with care! *) module Unsafe : sig - val kind : Evd.evar_map -> t -> (t, t, Evd.esorts, Evd.einstance, Evd.erelevance) Constr.kind_of_term + val kind : Evd.evar_map -> t -> (t, t, EConstr.ESorts.t, EConstr.EInstance.t, EConstr.ERelevance.t) Constr.kind_of_term (** [kind sigma t] returns the kind view of [t]. *) - val make : (t, t, Evd.esorts, Evd.einstance, Evd.erelevance) Constr.kind_of_term -> t + val make : (t, t, EConstr.ESorts.t, EConstr.EInstance.t, EConstr.ERelevance.t) Constr.kind_of_term -> t (** [make kind] constructs a term from the given kind. *) val check : Environ.env -> Evd.evar_map -> t -> Evd.evar_map * t @@ -432,7 +432,7 @@ end module Fresh : sig module Free : sig - type t = Nameops.Fresh.t + type t (** Type of sets of free variables. *) val empty : t @@ -455,10 +455,13 @@ module Fresh : sig (** [fresh free id] generates a fresh identifier with the given base name which is not a member of [free]. *) + [%%if rocq >= (9, 1)] val next : Free.t -> ident -> ident * Free.t (** [next free id] generates a fresh identifier with the given base name which is not a member of [free], and returns the updated set. More efficient than composing [fresh] and [Free.add]. *) + + [%%endif] end (** {2 Identifiers} *) @@ -585,6 +588,7 @@ module Message : sig (** [of_lconstr env sigma t] prints [t] at level 200 (no surrounding parentheses). *) + [%%if rocq >= (9, 2)] val of_preterm : Environ.env -> Evd.evar_map -> preterm -> message (** [of_preterm env sigma t] prints [t] at level 8 (surrounding with parentheses to print syntax above that level such as applications). *) @@ -597,6 +601,8 @@ module Message : sig (** [of_exninfo exninfo] prints the (Ltac2 and OCaml) backtrace info if it was recorded. *) + [%%endif] + val concat : message -> message -> message (** [concat m1 m2] concats two messages. *) @@ -639,49 +645,74 @@ end (** {2 Module} *) +[%%if rocq >= (9, 2)] module Module : sig type t = ModPath.t (** The name of a module or module type. It may be a functor. It may also be - currently open. *) + currently open. + + @since 9.2 *) val equal : t -> t -> bool - (** [equal m1 m2] tests equality of module names. *) + (** [equal m1 m2] tests equality of module names. + + @since 9.2 *) val to_message : t -> message - (** [to_message m] prints a module name. *) + (** [to_message m] prints a module name. + + @since 9.2 *) val is_modtype : Environ.env -> t -> bool - (** [is_modtype env m] returns [true] if [m] is a module type or module type functor. *) + (** [is_modtype env m] returns [true] if [m] is a module type or module type functor. + + @since 9.2 *) val is_functor : Environ.env -> t -> bool - (** [is_modtype env m] returns [true] if [m] is a module functor or module type functor. *) + (** [is_functor env m] returns [true] if [m] is a module functor or module type functor. + + @since 9.2 *) val is_bound_module : t -> bool (** [is_bound_module m] returns [true] for modules which are arguments of a - currently open functor ([false] for submodules of bound modules). *) + currently open functor ([false] for submodules of bound modules). + + @since 9.2 *) val is_library : t -> bool - (** [is_library m] returns [true] for modules which are libraries (i.e. files). *) + (** [is_library m] returns [true] for modules which are libraries (i.e. files). + + @since 9.2 *) val is_open : t -> bool (** [is_open m] returns [true] if [m] refers to a currently open interactive - module (or module type or functor). *) + module (or module type or functor). + + @since 9.2 *) val parent_module : t -> t option (** [parent_module m] returns the parent module, i.e., [A] for [A.B]. Toplevel - modules (libraries) and bound modules (functor arguments) return None. *) + modules (libraries) and bound modules (functor arguments) return [None]. + + @since 9.2 *) val module_of_reference : GlobRef.t -> t (** [module_of_reference ref] returns the module of the reference. - Throws if [ref] is a [VarRef]. *) + Throws if [ref] is a [VarRef]. + + @since 9.2 *) val current_module : unit -> t (** [current_module ()] returns a reference to the current innermost open - interactive module. *) + interactive module. + + @since 9.2 *) val loaded_libraries : unit -> t list - (** [loaded_libraries ()] returns the list of loaded library modules. *) + (** [loaded_libraries ()] returns the list of loaded library modules. + + @since 9.2 *) module Field : sig type t = Tac2ffi.ModField.t @@ -690,8 +721,11 @@ module Module : sig val contents : t -> Field.t list option (** [contents m] returns the contents of the given module ([None] on closed functors and module types). Inductives are represented only by the first - inductive of each mutual block (and no constructors). *) + inductive of each mutual block (and no constructors). + + @since 9.2 *) end +[%%endif] (** {2 Pattern} *) @@ -782,6 +816,7 @@ end (** {2 Rewriting} *) +[%%if rocq >= (9, 1)] module Rewrite : sig (** Module for rewrite strategies used by [rewrite_strat]. *) @@ -869,8 +904,11 @@ module Rewrite : sig val eval : Redexpr.red_expr -> t (** Converts the term under consideration. *) + [%%if rocq >= (9, 3)] val matches : pattern -> t - (** The identity if the pattern matching succeeds, fails otherwise. *) + (** The identity if the pattern matching succeeds, fails otherwise. + + @since 9.3 *) val tactic : (constr -> constr -> constr option -> Rewrite.Result.t Proofview.tactic) -> t (** The [tactic f] strategy applies [f] to arguments [ty], [lhs] and [rel], @@ -888,115 +926,184 @@ module Rewrite : sig If the proof [prf] is syntactically [eq_refl _], then the witness of the rewriting is simply a *conversion* requiring no explicit proof and no congruence lemmas - for the context of the rewrite. *) + for the context of the rewrite. + + @since 9.3 *) + + [%%endif] end val rewrite_strat : ?in_hyp:ident -> Strategy.t -> unit Proofview.tactic (** Runs rewrite strategy on the type of a hypothesis or the goal if the - [in_hyp] is [None]. *) + [in_hyp] is [None]. + + @since 9.1 *) end +[%%endif] (** {2 Schemes} *) +[%%if rocq >= (9, 3)] module Scheme : sig type kind (** An abstract type representing a scheme kind. Use the predefined values - below to refer to specific scheme kinds. *) + below to refer to specific scheme kinds. + + @since 9.3 *) val lookup : kind -> GlobRef.t -> GlobRef.t option (** [lookup kind ref] looks up the scheme registered under [kind] for the reference [ref]. Returns [None] if [ref] is not an inductive type or if no such - scheme is registered. *) + scheme is registered. + + @since 9.3 *) (** {3 Elimination schemes} *) val rect_dep : kind - (** Dependent recursion scheme for Type. *) + (** Dependent recursion scheme for Type. + + @since 9.3 *) val rec_dep : kind - (** Dependent recursion scheme for Set. *) + (** Dependent recursion scheme for Set. + + @since 9.3 *) val ind_dep : kind - (** Dependent induction scheme for Prop. *) + (** Dependent induction scheme for Prop. + + @since 9.3 *) val sind_dep : kind - (** Dependent induction scheme for SProp. *) + (** Dependent induction scheme for SProp. + + @since 9.3 *) val rect_nodep : kind - (** Non-dependent recursion scheme for Type. *) + (** Non-dependent recursion scheme for Type. + + @since 9.3 *) val rec_nodep : kind - (** Non-dependent recursion scheme for Set. *) + (** Non-dependent recursion scheme for Set. + + @since 9.3 *) val ind_nodep : kind - (** Non-dependent induction scheme for Prop. *) + (** Non-dependent induction scheme for Prop. + + @since 9.3 *) val sind_nodep : kind - (** Non-dependent induction scheme for SProp. *) + (** Non-dependent induction scheme for SProp. + + @since 9.3 *) - (** {3 Case analysis schemes} *) + (** {3 Case analysis schemes} + + @since 9.3 *) val case_dep : kind - (** Dependent case analysis scheme for Type. *) + (** Dependent case analysis scheme for Type. + + @since 9.3 *) val case_nodep : kind - (** Non-dependent case analysis scheme for Type. *) + (** Non-dependent case analysis scheme for Type. + + @since 9.3 *) val casep_dep : kind - (** Dependent case analysis scheme for Prop. *) + (** Dependent case analysis scheme for Prop. + + @since 9.3 *) val casep_nodep : kind - (** Non-dependent case analysis scheme for Prop. *) + (** Non-dependent case analysis scheme for Prop. + + @since 9.3 *) val scase_nodep : kind - (** Dependent case analysis scheme for SProp. *) + (** Dependent case analysis scheme for SProp. + + @since 9.3 *) val scase_dep : kind - (** Non-dependent case analysis scheme for SProp. *) + (** Non-dependent case analysis scheme for SProp. + + @since 9.3 *) (** {3 Equality schemes} *) val sym : kind - (** Symmetry scheme. *) + (** Symmetry scheme. + + @since 9.3 *) val sym_involutive : kind - (** Involutive symmetry scheme. *) + (** Involutive symmetry scheme. + + @since 9.3 *) val rew : kind - (** Right-to-left rewriting scheme. *) + (** Right-to-left rewriting scheme. + + @since 9.3 *) val rew_dep : kind - (** Right-to-left dependent rewriting scheme. *) + (** Right-to-left dependent rewriting scheme. + + @since 9.3 *) val rew_fwd_dep : kind - (** Right-to-left forward dependent rewriting scheme. *) + (** Right-to-left forward dependent rewriting scheme. + + @since 9.3 *) val rew_r : kind - (** Left-to-right rewriting scheme. *) + (** Left-to-right rewriting scheme. + + @since 9.3 *) val rew_r_dep : kind - (** Left-to-right dependent rewriting scheme. *) + (** Left-to-right dependent rewriting scheme. + + @since 9.3 *) val rew_fwd_r_dep : kind - (** Left-to-right forward dependent rewriting scheme. *) + (** Left-to-right forward dependent rewriting scheme. + + @since 9.3 *) val congr : kind - (** Congruence scheme. *) + (** Congruence scheme. + + @since 9.3 *) (** {3 Boolean equality and decidability schemes} *) val beq : kind - (** Boolean equality scheme. *) + (** Boolean equality scheme. + + @since 9.3 *) val dec_bl : kind - (** Boolean to Leibniz equality scheme. *) + (** Boolean to Leibniz equality scheme. + + @since 9.3 *) val dec_lb : kind - (** Leibniz to Boolean equality scheme. *) + (** Leibniz to Boolean equality scheme. + + @since 9.3 *) val eq_dec : kind - (** Decidable equality scheme. *) +(** Decidable equality scheme. + + @since 9.3 *) end +[%%endif] (** {2 Standard tactics} *) @@ -1009,7 +1116,11 @@ module Std : sig type clause = Tac2types.clause type reference = GlobRef.t type strength = Genredexpr.strength + [%%if rocq >= (9, 2)] type red_flags = Tac2types.red_flag + [%%else] + type red_flags = reference Genredexpr.glob_red_flag + [%%endif] type intro_pattern = Tac2types.intro_pattern and intro_pattern_naming = Tac2types.intro_pattern_naming and intro_pattern_action = Tac2types.intro_pattern_action @@ -1417,6 +1528,7 @@ module Std : sig (** {3 Applying conversion rules} *) + [%%if rocq >= (9, 1)] module Red : sig type t = Redexpr.red_expr (** Type representing a reduction expression. Red expressions describe @@ -1512,6 +1624,8 @@ module Std : sig @see Reference manual *) + [%%endif] + (** {3 Reasoning with inductive types} *) (** {4 Applying constructors} *) @@ -1841,14 +1955,6 @@ module TransparentState : sig (** Type representing a transparency state. A transparency state is a set of variables, constants, and primitive projections. *) - type strategy_level = Conv_oracle.level - (** Strategy levels used by [with_strategy]: - - - [Expand] corresponds to the [-oo] level (always unfold) - - [Opaque] corresponds to the [+oo] level (never unfold) - - [Level n] corresponds to integer level [n] (where [Level 0] is - transparent). *) - val empty : t (** [empty] is the empty transparency state (all constants are opaque). *) @@ -1909,11 +2015,25 @@ module TransparentState : sig (** [mem_var v t] checks whether the local variable [v] is present in the transparency state [t]. *) + [%%if rocq >= (9, 3)] + type strategy_level = Conv_oracle.level + (** Strategy levels used by [with_strategy]: + + - [Expand] corresponds to the [-oo] level (always unfold) + - [Opaque] corresponds to the [+oo] level (never unfold) + - [Level n] corresponds to integer level [n] (where [Level 0] is + transparent). *) + val with_strategy : strategy_level -> GlobRef.t list -> 'a Proofview.tactic -> 'a Proofview.tactic (** [with_strategy lvl refs tac] temporarily sets the strategy level of all references in [refs] to [lvl], executes [tac], and then restores the original strategy levels. This is the Ltac2 analogue of the - [with_strategy] Ltac tactic and the [Strategy] vernacular command. *) + [with_strategy] Ltac tactic and the [Strategy] vernacular command. + + @since 9.3 + *) + + [%%endif] end (** {2 Unification} *)