From 1786ab98a94a69a88b14db588c942276e7341e66 Mon Sep 17 00:00:00 2001 From: Dario Halilovic Date: Sat, 11 Jul 2026 15:22:38 +0200 Subject: [PATCH 1/9] feat: support Rocq 9.2 --- .github/workflows/ci.yml | 2 +- dune-project | 3 ++- mltac2.opam | 3 ++- src/dune | 4 ++-- src/ltac2.ml | 24 ++++++++++++++++++++++++ src/ltac2.mli | 38 +++++++++++++++++++++++++++----------- 6 files changed, 58 insertions(+), 16 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 2fb4596..52b6e28 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -7,7 +7,7 @@ jobs: strategy: matrix: runs-on: [ ubuntu-latest ] - rocq_version: [ dev ] + rocq_version: [ "9.2", dev ] runs-on: ${{ matrix.runs-on }} steps: diff --git a/dune-project b/dune-project index 778f462..d773f99 100644 --- a/dune-project +++ b/dune-project @@ -17,4 +17,5 @@ (name mltac2) (synopsis "Ltac2 APIs in OCaml") (depends - rocq-runtime)) + (rocq-runtime (>= 9.2)) + ppx_optcomp)) diff --git a/mltac2.opam b/mltac2.opam index 16db60b..93e2146 100644 --- a/mltac2.opam +++ b/mltac2.opam @@ -8,7 +8,8 @@ homepage: "https://github.com/epfl-systemf/mltac2" bug-reports: "https://github.com/epfl-systemf/mltac2/issues" depends: [ "dune" {>= "3.21"} - "rocq-runtime" + "rocq-runtime" {>= "9.2"} + "ppx_optcomp" "odoc" {with-doc} ] build: [ diff --git a/src/dune b/src/dune index 35c18bc..bcd1e0c 100644 --- a/src/dune +++ b/src/dune @@ -1,5 +1,5 @@ (library (name mltac2) (public_name mltac2) - (libraries - rocq-runtime.plugins.ltac2)) + (libraries rocq-runtime.plugins.ltac2) + (preprocess (pps ppx_optcomp -- -cookie "ppx_optcomp.env=env ~rocq:(Defined \"%{rocq:version.major}.%{rocq:version.minor}\")"))) diff --git a/src/ltac2.ml b/src/ltac2.ml index 396cddd..e24d43b 100644 --- a/src/ltac2.ml +++ b/src/ltac2.ml @@ -454,9 +454,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 +492,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 +529,7 @@ module Ltac2Scheme = struct let case_nodep = "case_nodep" let case_dep = "case_dep" end +[%%endif] (** {2 Projection} *) @@ -540,10 +549,17 @@ 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 (Projection.constant p)) + [%%else] let print p = Nametab.pr_global_env Id.Set.empty (ConstRef (Environ.projection_repr_constant (Global.env ()) (Projection.repr p))) + [%%endif] end (** {2 Module} *) @@ -725,9 +741,13 @@ 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 @@ -794,7 +814,9 @@ 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"] let with_strategy level grs tac = Tac2tactics.with_strategy level grs (fun () -> tac) + [%%endif] end (** {2 Unification} *) @@ -1021,7 +1043,9 @@ module Module = Ltac2Module module Pattern = Ltac2Pattern module Proj = Ltac2Proj module Rewrite = Ltac2Rewrite +[%%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..f34bdf2 100644 --- a/src/ltac2.mli +++ b/src/ltac2.mli @@ -869,8 +869,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,7 +891,11 @@ 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 @@ -896,6 +903,8 @@ module Rewrite : sig [in_hyp] is [None]. *) end +[%%if rocq >= "9.3"] + (** {2 Schemes} *) module Scheme : sig @@ -997,6 +1006,7 @@ module Scheme : sig val eq_dec : kind (** Decidable equality scheme. *) end +[%%endif] (** {2 Standard tactics} *) @@ -1841,14 +1851,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 +1911,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} *) From eab1d23aa7effac533dc1fe56fa142fde848a472 Mon Sep 17 00:00:00 2001 From: Dario Halilovic Date: Sat, 11 Jul 2026 15:25:55 +0200 Subject: [PATCH 2/9] ci: disable fail-fast --- .github/workflows/ci.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 52b6e28..b2c72cb 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -5,6 +5,7 @@ on: [push, pull_request] jobs: build: strategy: + fail-fast: false matrix: runs-on: [ ubuntu-latest ] rocq_version: [ "9.2", dev ] From 130374553a6246007a4a289aeeb061d8698d35e6 Mon Sep 17 00:00:00 2001 From: Dario Halilovic Date: Sat, 11 Jul 2026 15:29:55 +0200 Subject: [PATCH 3/9] fix(ci): downgrade Dune to 3.17 --- dune-project | 2 +- mltac2.opam | 2 +- mltac2.opam.template | 1 + src/ltac2.ml | 3 +-- 4 files changed, 4 insertions(+), 4 deletions(-) create mode 100644 mltac2.opam.template diff --git a/dune-project b/dune-project index d773f99..aa3a46f 100644 --- a/dune-project +++ b/dune-project @@ -1,4 +1,4 @@ -(lang dune 3.21) +(lang dune 3.17) (name mltac2) diff --git a/mltac2.opam b/mltac2.opam index 93e2146..90dc2ca 100644 --- a/mltac2.opam +++ b/mltac2.opam @@ -7,7 +7,7 @@ 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"} + "dune" {>= "3.17"} "rocq-runtime" {>= "9.2"} "ppx_optcomp" "odoc" {with-doc} diff --git a/mltac2.opam.template b/mltac2.opam.template new file mode 100644 index 0000000..7a302d9 --- /dev/null +++ b/mltac2.opam.template @@ -0,0 +1 @@ +x-maintenance-intent: ["(latest)"] diff --git a/src/ltac2.ml b/src/ltac2.ml index e24d43b..fe07482 100644 --- a/src/ltac2.ml +++ b/src/ltac2.ml @@ -10,7 +10,6 @@ open Tac2types open Proofview.Notations let return = Proofview.tclUNIT -let throw = Tac2core.throw (** {1 Ltac2 APIs} *) @@ -757,7 +756,6 @@ end module Ltac2TransparentState = struct type t = TransparentState.t - type strategy_level = Conv_oracle.level open TransparentState @@ -815,6 +813,7 @@ module Ltac2TransparentState = struct 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 From aefd6acafd29897f392dd3344d2877b0a44f8988 Mon Sep 17 00:00:00 2001 From: Dario Halilovic Date: Sat, 11 Jul 2026 15:53:43 +0200 Subject: [PATCH 4/9] fix(ci): disable `dune subst` Same fix as https://github.com/epfl-systemf/ppx_rocq/commit/6df220d17bf3c4f5c0f9bc8e9611c4ef81fd5132 --- dune-project | 4 ++-- mltac2.opam | 2 -- mltac2.opam.template | 1 - 3 files changed, 2 insertions(+), 5 deletions(-) delete mode 100644 mltac2.opam.template diff --git a/dune-project b/dune-project index aa3a46f..f821a9b 100644 --- a/dune-project +++ b/dune-project @@ -1,9 +1,9 @@ (lang dune 3.17) -(name mltac2) - (generate_opam_files true) +(subst disabled) ;; Work-around for Dune 3.17 subst bug: https://github.com/ocaml/dune/issues/11045 +(name mltac2) (authors "Dario Halilovic" "Pierre-Marie Pédrot") (maintainers "Dario Halilovic") (license LGPL-2.1-only) diff --git a/mltac2.opam b/mltac2.opam index 90dc2ca..f8bbb3d 100644 --- a/mltac2.opam +++ b/mltac2.opam @@ -13,7 +13,6 @@ depends: [ "odoc" {with-doc} ] build: [ - ["dune" "subst"] {dev} [ "dune" "build" @@ -27,4 +26,3 @@ build: [ ] ] dev-repo: "git+https://github.com/epfl-systemf/mltac2.git" -x-maintenance-intent: ["(latest)"] diff --git a/mltac2.opam.template b/mltac2.opam.template deleted file mode 100644 index 7a302d9..0000000 --- a/mltac2.opam.template +++ /dev/null @@ -1 +0,0 @@ -x-maintenance-intent: ["(latest)"] From 4bfcacb810a013764ad3c7a45e43c909a70309d2 Mon Sep 17 00:00:00 2001 From: Dario Halilovic Date: Sat, 11 Jul 2026 17:01:00 +0200 Subject: [PATCH 5/9] fix: use tuples instead of strings for Rocq version numbers --- src/dune | 2 +- src/ltac2.ml | 14 +++++++------- src/ltac2.mli | 6 +++--- 3 files changed, 11 insertions(+), 11 deletions(-) diff --git a/src/dune b/src/dune index bcd1e0c..37a3e0c 100644 --- a/src/dune +++ b/src/dune @@ -2,4 +2,4 @@ (name mltac2) (public_name mltac2) (libraries rocq-runtime.plugins.ltac2) - (preprocess (pps ppx_optcomp -- -cookie "ppx_optcomp.env=env ~rocq:(Defined \"%{rocq:version.major}.%{rocq:version.minor}\")"))) + (preprocess (pps ppx_optcomp -- -cookie "ppx_optcomp.env=env ~rocq:(Defined (%{rocq:version.major}, %{rocq:version.minor}))"))) diff --git a/src/ltac2.ml b/src/ltac2.ml index fe07482..70c830a 100644 --- a/src/ltac2.ml +++ b/src/ltac2.ml @@ -453,7 +453,7 @@ module Ltac2Ind = struct let nparams_uniform (_, mib) = mib.Declarations.mind_nparams_rec - [%%if rocq = "9.2"] + [%%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) @@ -491,7 +491,7 @@ module Ltac2Constructor = struct Nametab.pr_global_env Id.Set.empty (ConstructRef ctor) end -[%%if rocq >= "9.3"] +[%%if rocq >= (9, 3)] (** {2 Schemes} *) @@ -548,7 +548,7 @@ module Ltac2Proj = struct let to_constant p = Some (Projection.repr p) - [%%if rocq = "9.2"] + [%%if rocq = (9, 2)] let print p = Nametab.pr_global_env Id.Set.empty @@ -740,11 +740,11 @@ module Ltac2Rewrite = struct let lemmas = Tac2tactics.RewriteStrats.lemmas let fold = Rewrite.Strategies.fold let eval = Rewrite.Strategies.reduce - [%%if rocq >= "9.3"] + [%%if rocq >= (9, 3)] let matches = Rewrite.Strategies.matches [%%endif] - [%%if rocq >= "9.3"] + [%%if rocq >= (9, 3)] let tactic = Tac2tactics.wrap_tactic_call [%%endif] end @@ -812,7 +812,7 @@ 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"] + [%%if rocq >= (9, 3)] type strategy_level = Conv_oracle.level let with_strategy level grs tac = Tac2tactics.with_strategy level grs (fun () -> tac) [%%endif] @@ -1042,7 +1042,7 @@ module Module = Ltac2Module module Pattern = Ltac2Pattern module Proj = Ltac2Proj module Rewrite = Ltac2Rewrite -[%%if rocq >= "9.3"] +[%%if rocq >= (9, 3)] module Scheme = Ltac2Scheme [%%endif] module Std = Ltac2Std diff --git a/src/ltac2.mli b/src/ltac2.mli index f34bdf2..c2f9746 100644 --- a/src/ltac2.mli +++ b/src/ltac2.mli @@ -869,7 +869,7 @@ module Rewrite : sig val eval : Redexpr.red_expr -> t (** Converts the term under consideration. *) - [%%if rocq >= "9.3"] + [%%if rocq >= (9, 3)] val matches : pattern -> t (** The identity if the pattern matching succeeds, fails otherwise. @@ -903,7 +903,7 @@ module Rewrite : sig [in_hyp] is [None]. *) end -[%%if rocq >= "9.3"] +[%%if rocq >= (9, 3)] (** {2 Schemes} *) @@ -1911,7 +1911,7 @@ module TransparentState : sig (** [mem_var v t] checks whether the local variable [v] is present in the transparency state [t]. *) - [%%if rocq >= "9.3"] + [%%if rocq >= (9, 3)] type strategy_level = Conv_oracle.level (** Strategy levels used by [with_strategy]: From 9f825f72c9650c4fd111bfa979444f95ef8fc6dd Mon Sep 17 00:00:00 2001 From: Dario Halilovic Date: Sat, 11 Jul 2026 17:01:56 +0200 Subject: [PATCH 6/9] fix(dune): recognize Rocq environment variables --- dune-project | 1 + 1 file changed, 1 insertion(+) diff --git a/dune-project b/dune-project index f821a9b..3f734bd 100644 --- a/dune-project +++ b/dune-project @@ -1,4 +1,5 @@ (lang dune 3.17) +(using coq 0.10) (generate_opam_files true) (subst disabled) ;; Work-around for Dune 3.17 subst bug: https://github.com/ocaml/dune/issues/11045 From 00b2ebc9032fb7dc2d757d9bd37ea216e9bddadc Mon Sep 17 00:00:00 2001 From: Dario Halilovic Date: Sun, 12 Jul 2026 15:54:21 +0200 Subject: [PATCH 7/9] fix(dune): use coq-core compatibility package for "coq:version" environment variables --- dune-project | 3 +-- mltac2.opam | 2 +- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/dune-project b/dune-project index 3f734bd..2d3feb6 100644 --- a/dune-project +++ b/dune-project @@ -1,5 +1,4 @@ (lang dune 3.17) -(using coq 0.10) (generate_opam_files true) (subst disabled) ;; Work-around for Dune 3.17 subst bug: https://github.com/ocaml/dune/issues/11045 @@ -18,5 +17,5 @@ (name mltac2) (synopsis "Ltac2 APIs in OCaml") (depends - (rocq-runtime (>= 9.2)) + (coq-core (>= 9.2)) ;; Use coq-core to obtain coqc compatibility binaries ppx_optcomp)) diff --git a/mltac2.opam b/mltac2.opam index f8bbb3d..6988459 100644 --- a/mltac2.opam +++ b/mltac2.opam @@ -8,7 +8,7 @@ homepage: "https://github.com/epfl-systemf/mltac2" bug-reports: "https://github.com/epfl-systemf/mltac2/issues" depends: [ "dune" {>= "3.17"} - "rocq-runtime" {>= "9.2"} + "coq-core" {>= "9.2"} "ppx_optcomp" "odoc" {with-doc} ] From 53f3722a400114c77051f9d08c1b50a5379b5869 Mon Sep 17 00:00:00 2001 From: Dario Halilovic Date: Sun, 12 Jul 2026 15:54:58 +0200 Subject: [PATCH 8/9] chore(build): document bumping to Dune 3.21 --- dune-project | 5 ++++- src/dune | 3 ++- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/dune-project b/dune-project index 2d3feb6..a708690 100644 --- a/dune-project +++ b/dune-project @@ -1,7 +1,10 @@ (lang dune 3.17) (generate_opam_files true) -(subst disabled) ;; Work-around for Dune 3.17 subst bug: https://github.com/ocaml/dune/issues/11045 + +;; 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") diff --git a/src/dune b/src/dune index 37a3e0c..e2011f3 100644 --- a/src/dune +++ b/src/dune @@ -2,4 +2,5 @@ (name mltac2) (public_name mltac2) (libraries rocq-runtime.plugins.ltac2) - (preprocess (pps ppx_optcomp -- -cookie "ppx_optcomp.env=env ~rocq:(Defined (%{rocq:version.major}, %{rocq:version.minor}))"))) + ;; 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}))"))) From 92b1bea674f00684221ea5342cdbc1e631d7ce58 Mon Sep 17 00:00:00 2001 From: Dario Halilovic Date: Thu, 23 Jul 2026 19:51:04 +0200 Subject: [PATCH 9/9] feat: support Rocq 9.0 and 9.1 --- .github/workflows/ci.yml | 2 +- dune-project | 2 +- mltac2.opam | 2 +- src/ltac2.ml | 132 ++++++++++++++++++++++--- src/ltac2.mli | 202 +++++++++++++++++++++++++++++---------- 5 files changed, 274 insertions(+), 66 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index b2c72cb..2e741ae 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -8,7 +8,7 @@ jobs: fail-fast: false matrix: runs-on: [ ubuntu-latest ] - rocq_version: [ "9.2", 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 a708690..0a1a015 100644 --- a/dune-project +++ b/dune-project @@ -20,5 +20,5 @@ (name mltac2) (synopsis "Ltac2 APIs in OCaml") (depends - (coq-core (>= 9.2)) ;; Use coq-core to obtain coqc compatibility binaries + (coq-core (>= 9.0)) ;; Use coq-core to obtain coqc compatibility binaries ppx_optcomp)) diff --git a/mltac2.opam b/mltac2.opam index 6988459..916c320 100644 --- a/mltac2.opam +++ b/mltac2.opam @@ -8,7 +8,7 @@ homepage: "https://github.com/epfl-systemf/mltac2" bug-reports: "https://github.com/epfl-systemf/mltac2/issues" depends: [ "dune" {>= "3.17"} - "coq-core" {>= "9.2"} + "coq-core" {>= "9.0"} "ppx_optcomp" "odoc" {with-doc} ] diff --git a/src/ltac2.ml b/src/ltac2.ml index 70c830a..5d85997 100644 --- a/src/ltac2.ml +++ b/src/ltac2.ml @@ -11,6 +11,35 @@ open Proofview.Notations let return = Proofview.tclUNIT +[%%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} *) (** {2 Printing} *) @@ -32,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 @@ -124,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 = @@ -160,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; @@ -171,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 } @@ -223,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 @@ -323,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 @@ -371,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 = @@ -398,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} *) @@ -548,21 +630,22 @@ module Ltac2Proj = struct let to_constant p = Some (Projection.repr p) - [%%if rocq = (9, 2)] + [%%if rocq > (9, 2)] let print p = Nametab.pr_global_env Id.Set.empty - (ConstRef (Projection.constant p)) + (ConstRef (Environ.projection_repr_constant (Global.env ()) (Projection.repr p))) [%%else] let print p = Nametab.pr_global_env Id.Set.empty - (ConstRef (Environ.projection_repr_constant (Global.env ()) (Projection.repr p))) + (ConstRef (Projection.constant p)) [%%endif] end (** {2 Module} *) +[%%if rocq >= (9, 2)] module Ltac2Module = struct type t = ModPath.t let equal = ModPath.equal @@ -709,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 @@ -751,6 +836,7 @@ module Ltac2Rewrite = struct let rewrite_strat ?in_hyp s = Tac2tactics.rewrite_strat s in_hyp end +[%%endif] (** {2 Transparent state} *) @@ -842,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 @@ -864,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 @@ -897,6 +987,7 @@ module Ltac2Std = struct let exfalso = Tactics.exfalso + [%%if rocq >= (9, 1)] module Red = struct type t = Redexpr.red_expr @@ -916,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 @@ -966,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 @@ -980,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 () = @@ -1004,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} *) @@ -1038,10 +1138,14 @@ 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] diff --git a/src/ltac2.mli b/src/ltac2.mli index c2f9746..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]. *) @@ -900,111 +935,173 @@ module Rewrite : sig 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]. *) -end + [in_hyp] is [None]. -[%%if rocq >= (9, 3)] + @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. - (** {3 Case analysis schemes} *) + @since 9.3 *) + + (** {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] @@ -1019,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 @@ -1427,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 @@ -1522,6 +1624,8 @@ module Std : sig @see Reference manual *) + [%%endif] + (** {3 Reasoning with inductive types} *) (** {4 Applying constructors} *)