Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Adapt to coq/coq#18624 (Tac2ffi / Tac2val split) #23

Merged
merged 1 commit into from
Feb 7, 2024
Merged

Adapt to coq/coq#18624 (Tac2ffi / Tac2val split) #23

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 8 additions & 8 deletions src/tac2compile.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -60,7 +60,7 @@ let rawstr s = quote (str (String.escaped s))
so instead of eg "Some 1" we have "ValBlk (0, [|ValInt 1|])"

All other names are user names. As such to access coq-core values we must qualify them,
eg "Tac2ffi.mk_closure_val" etc
eg "Tac2val.mk_closure_val" etc
*)

let keywords =
Expand Down Expand Up @@ -223,7 +223,7 @@ let rec pp_arity n =

let pp_arity n =
assert (n >= 1);
str "Tac2ffi.(" ++ pp_arity n ++ str ")"
str "Tac2val.(" ++ pp_arity n ++ str ")"

let rec pp_binders = function
| [] -> mt()
Expand Down Expand Up @@ -732,7 +732,7 @@ let pp_when_clauses w =

let pp_mk_closure_val arity f =
surround
(str "Tac2ffi.mk_closure_val" ++ spc() ++
(str "Tac2val.mk_closure_val" ++ spc() ++
pp_arity arity ++ spc() ++ f)

let pp_var x = function
Expand Down Expand Up @@ -777,7 +777,7 @@ let rec pp_nontac_expr = function
| Ctor (i, es) -> str "(ValBlk (" ++ int i ++ str ", [|" ++ pp_val_list es ++ str "|]))"
| PrjV (e, i) ->
surround
(str "Tac2ffi.Valexpr.field" ++ spc() ++ pp_nontac_expr e ++ spc() ++ int i)
(str "Tac2val.Valexpr.field" ++ spc() ++ pp_nontac_expr e ++ spc() ++ int i)
| Opn (kn, es) ->
surround
(str "Tac2ffi.of_open" ++ spc() ++
Expand Down Expand Up @@ -837,7 +837,7 @@ and pp_head_expr = function
begin match hinfo with
| None ->
surround
(str "Tac2ffi.apply_val" ++ spc() ++ pp_nontac_expr h ++ spc() ++
(str "Tac2val.apply_val" ++ spc() ++ pp_nontac_expr h ++ spc() ++
surround (str "[" ++ pp_val_list args ++ str "]"))
| Some x ->
surround
Expand Down Expand Up @@ -920,10 +920,10 @@ and pp_head_expr = function
| PrjMut (e, i) ->
str "PV.tclUNIT" ++ spc() ++
surround
(str "Tac2ffi.Valexpr.field" ++ spc() ++ pp_nontac_expr e ++ spc() ++ int i)
(str "Tac2val.Valexpr.field" ++ spc() ++ pp_nontac_expr e ++ spc() ++ int i)

| Set (e1,i,e2) ->
h (str "let () = Tac2ffi.Valexpr.set_field" ++ spc() ++
h (str "let () = Tac2val.Valexpr.set_field" ++ spc() ++
pp_nontac_expr e1 ++ spc() ++ int i ++ spc() ++
pp_nontac_expr e2 ++ spc()) ++
str "in" ++ spc() ++
Expand Down Expand Up @@ -969,7 +969,7 @@ let prelude prefix =
str "open Names" ++ fnl() ++
str "open Ltac2_plugin" ++ fnl() ++
str "open Ltac2_compiler" ++ fnl() ++
str "open Tac2ffi" ++ fnl() ++
str "open Tac2val" ++ fnl() ++
str "module PV = Proofview" ++ fnl() ++
str "open PV.Notations" ++ fnl()

Expand Down
1 change: 1 addition & 0 deletions src/tac2compiledPrim.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@

open Names
open Ltac2_plugin
open Tac2val
open Tac2ffi
open Proofview.Notations

Expand Down
2 changes: 1 addition & 1 deletion src/tac2compiledPrim.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)

open Ltac2_plugin.Tac2ffi
open Ltac2_plugin.Tac2val
open Proofview

val array_empty : valexpr -> valexpr tactic
Expand Down
Loading