From c3efcc501e140a74a948513a0e45223e4d5b521c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 8 Jun 2019 15:08:51 +0200
Subject: Adding the ability to transfer Ltac2 variables to Ltac1 quotations.

---
 test-suite/ltac2/compat.v         | 16 +++++++++
 user-contrib/Ltac2/g_ltac2.mlg    | 19 +++++++++--
 user-contrib/Ltac2/tac2core.ml    | 68 ++++++++++++++++++++++++++++++---------
 user-contrib/Ltac2/tac2intern.ml  | 17 ++++++++++
 user-contrib/Ltac2/tac2intern.mli |  1 +
 user-contrib/Ltac2/tac2quote.mli  |  4 +--
 6 files changed, 105 insertions(+), 20 deletions(-)

diff --git a/test-suite/ltac2/compat.v b/test-suite/ltac2/compat.v
index 489fa638e4..a24c9af10d 100644
--- a/test-suite/ltac2/compat.v
+++ b/test-suite/ltac2/compat.v
@@ -27,6 +27,22 @@ Fail Ltac2 bar nay := ltac1:(discriminate nay).
 Fail Ltac2 pose1 (v : constr) :=
   ltac1:(pose $v).
 
+(** Variables explicitly crossing the boundary must satisfy typing properties *)
+Goal True.
+Proof.
+(* Missing variable *)
+Fail ltac1:(x |- idtac).
+(* Wrong type *)
+Fail let x := 0 in ltac1:(x |- idtac).
+(* OK, and runtime has access to variable *)
+let x := Ltac1.of_constr constr:(Type) in ltac1:(x |- idtac x).
+
+(* Same for ltac1val *)
+Fail Ltac1.run ltac1val:(x |- idtac).
+Fail let x := 0 in Ltac1.run ltac1val:(x |- idtac).
+let x := Ltac1.of_constr constr:(Type) in Ltac1.run ltac1val:(x |- idtac x).
+Abort.
+
 (** Test calls to Ltac2 from Ltac1 *)
 
 Set Default Proof Mode "Classic".
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index e348396aad..23b5f4daef 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -37,6 +37,8 @@ let (<+>) (lk1 : lookahead) lk2 n strm = match lk1 n strm with
 | None -> lk2 n strm
 | Some n -> Some n
 
+let lk_empty n strm = Some n
+
 let lk_kw kw n strm = match stream_nth n strm with
 | KEYWORD kw' | IDENT kw' -> if String.equal kw kw' then Some (n + 1) else None
 | _ -> None
@@ -51,6 +53,9 @@ let lk_int n strm = match stream_nth n strm with
 
 let lk_ident_or_anti = lk_ident <+> (lk_kw "$" >> lk_ident)
 
+let rec lk_ident_list n strm =
+  ((lk_ident >> lk_ident_list) <+> lk_empty) n strm
+
 (* lookahead for (x:=t), (?x:=t) and (1:=t) *)
 let test_lpar_idnum_coloneq =
   entry_of_lookahead "test_lpar_idnum_coloneq" begin
@@ -85,6 +90,11 @@ let test_dollar_ident =
     lk_kw "$" >> lk_ident
   end
 
+let test_ltac1_env =
+  entry_of_lookahead "test_ltac1_env" begin
+    lk_ident_list >> lk_kw "|-"
+  end
+
 let tac2expr = Tac2entries.Pltac.tac2expr
 let tac2type = Entry.create "tactic:tac2type"
 let tac2def_val = Entry.create "tactic:tac2def_val"
@@ -225,8 +235,13 @@ GRAMMAR EXTEND Gram
       | IDENT "ident"; ":"; "("; c = lident; ")" -> { Tac2quote.of_ident c }
       | IDENT "pattern"; ":"; "("; c = Constr.lconstr_pattern; ")" -> { inj_pattern loc c }
       | IDENT "reference"; ":"; "("; c = globref; ")" -> { inj_reference loc c }
-      | IDENT "ltac1"; ":"; "("; qid = ltac1_expr; ")" -> { inj_ltac1 loc qid }
-      | IDENT "ltac1val"; ":"; "("; qid = ltac1_expr; ")" -> { inj_ltac1val loc qid }
+      | IDENT "ltac1"; ":"; "("; qid = ltac1_expr_in_env; ")" -> { inj_ltac1 loc qid }
+      | IDENT "ltac1val"; ":"; "("; qid = ltac1_expr_in_env; ")" -> { inj_ltac1val loc qid }
+    ] ]
+  ;
+  ltac1_expr_in_env:
+    [ [ test_ltac1_env; ids = LIST0 locident; "|-"; e = ltac1_expr -> { ids, e }
+      | e = ltac1_expr -> { [], e }
     ] ]
   ;
   let_clause:
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index 2eb199633d..781f8cd25c 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -1118,16 +1118,30 @@ let () =
   define_ml_object Tac2quote.wit_reference obj
 
 let () =
-  let intern self ist tac =
+  let intern self ist (ids, tac) =
+    (* Check that variables have the Ltac1 type *)
+    let t_ltac1 = gtypref t_ltac1 in
+    let check { CAst.loc; v = id } =
+      let () = Tac2intern.check_ltac2_var ist.Genintern.extra ?loc id t_ltac1 in
+      id
+    in
+    let ids = List.map check ids in
     (* Prevent inner calls to Ltac2 values *)
     let extra = Tac2intern.drop_ltac2_env ist.Genintern.extra in
-    let ist = { ist with Genintern.extra } in
+    let ltacvars = List.fold_right Id.Set.add ids ist.Genintern.ltacvars in
+    let ist = { ist with Genintern.extra; ltacvars } in
     let _, tac = Genintern.intern Ltac_plugin.Tacarg.wit_tactic ist tac in
-    GlbVal tac, gtypref t_unit
+    GlbVal (ids, tac), gtypref t_unit
   in
-  let interp ist tac =
+  let interp ist (ids, tac) =
+    let add lfun id =
+      let v = Id.Map.find id ist.env_ist in
+      let v = Tac2ffi.to_ext val_ltac1 v in
+      Id.Map.add id v lfun
+    in
+    let lfun = List.fold_left add Id.Map.empty ids in
     let ist = { env_ist = Id.Map.empty } in
-    let lfun = Tac2interp.set_env ist Id.Map.empty in
+    let lfun = Tac2interp.set_env ist lfun in
     let ist = Ltac_plugin.Tacinterp.default_ist () in
     let ist = { ist with Geninterp.lfun = lfun } in
     let tac = (Ltac_plugin.Tacinterp.eval_tactic_ist ist tac : unit Proofview.tactic) in
@@ -1135,9 +1149,13 @@ let () =
     Proofview.tclOR tac wrap >>= fun () ->
     return v_unit
   in
-  let subst s tac = Genintern.substitute Ltac_plugin.Tacarg.wit_tactic s tac in
-  let print env tac =
-    str "ltac1:(" ++ Ltac_plugin.Pptactic.pr_glob_tactic env tac ++ str ")"
+  let subst s (ids, tac) = (ids, Genintern.substitute Ltac_plugin.Tacarg.wit_tactic s tac) in
+  let print env (ids, tac) =
+    let ids =
+      if List.is_empty ids then mt ()
+      else pr_sequence Id.print ids ++ spc () ++ str "|-" ++ spc ()
+    in
+    str "ltac1:(" ++ ids ++ Ltac_plugin.Pptactic.pr_glob_tactic env tac ++ str ")"
   in
   let obj = {
     ml_intern = intern;
@@ -1149,23 +1167,41 @@ let () =
 
 let () =
   let open Ltac_plugin in
-  let intern self ist tac =
+  let intern self ist (ids, tac) =
+    (* Check that variables have the Ltac1 type *)
+    let t_ltac1 = gtypref t_ltac1 in
+    let check { CAst.loc; v = id } =
+      let () = Tac2intern.check_ltac2_var ist.Genintern.extra ?loc id t_ltac1 in
+      id
+    in
+    let ids = List.map check ids in
     (* Prevent inner calls to Ltac2 values *)
     let extra = Tac2intern.drop_ltac2_env ist.Genintern.extra in
-    let ist = { ist with Genintern.extra } in
+    let ltacvars = List.fold_right Id.Set.add ids ist.Genintern.ltacvars in
+    let ist = { ist with Genintern.extra; ltacvars } in
     let _, tac = Genintern.intern Ltac_plugin.Tacarg.wit_tactic ist tac in
-    GlbVal tac, gtypref t_ltac1
+    GlbVal (ids, tac), t_ltac1
   in
-  let interp ist tac =
+  let interp ist (ids, tac) =
+    let add lfun id =
+      let v = Id.Map.find id ist.env_ist in
+      let v = Tac2ffi.to_ext val_ltac1 v in
+      Id.Map.add id v lfun
+    in
+    let lfun = List.fold_left add Id.Map.empty ids in
     let ist = { env_ist = Id.Map.empty } in
-    let lfun = Tac2interp.set_env ist Id.Map.empty in
+    let lfun = Tac2interp.set_env ist lfun in
     let ist = Ltac_plugin.Tacinterp.default_ist () in
     let ist = { ist with Geninterp.lfun = lfun } in
     return (Value.of_ext val_ltac1 (Tacinterp.Value.of_closure ist tac))
   in
-  let subst s tac = Genintern.substitute Tacarg.wit_tactic s tac in
-  let print env tac =
-    str "ltac1val:(" ++ Ltac_plugin.Pptactic.pr_glob_tactic env tac ++ str ")"
+  let subst s (ids, tac) = (ids, Genintern.substitute Tacarg.wit_tactic s tac) in
+  let print env (ids, tac) =
+    let ids =
+      if List.is_empty ids then mt ()
+      else pr_sequence Id.print ids ++ str " |- "
+    in
+    str "ltac1val:(" ++ ids++ Ltac_plugin.Pptactic.pr_glob_tactic env tac ++ str ")"
   in
   let obj = {
     ml_intern = intern;
diff --git a/user-contrib/Ltac2/tac2intern.ml b/user-contrib/Ltac2/tac2intern.ml
index 0961e9c9c9..9538943635 100644
--- a/user-contrib/Ltac2/tac2intern.ml
+++ b/user-contrib/Ltac2/tac2intern.ml
@@ -1191,6 +1191,23 @@ let intern_open_type t =
   let t = normalize env (count, vars) t in
   (!count, t)
 
+let rec get_closed = function
+| GTypVar _ -> assert false
+| GTypArrow (t, u) -> GTypArrow (get_closed t, get_closed u)
+| GTypRef (t, args) -> GTypRef (t, List.map get_closed args)
+
+let check_ltac2_var ?loc store id t =
+  let env = match Genintern.Store.get store ltac2_env with
+  | None -> empty_env ()
+  | Some env -> env
+  in
+  match Id.Map.find id env.env_var with
+  | sch ->
+    let t' = fresh_mix_type_scheme env sch in
+    unify ?loc env t' (get_closed t)
+  | exception Not_found ->
+    CErrors.user_err ?loc (Id.print id ++ str " is not a bound variable")
+
 (** Subtyping *)
 
 let check_subtype t1 t2 =
diff --git a/user-contrib/Ltac2/tac2intern.mli b/user-contrib/Ltac2/tac2intern.mli
index 5e282a386a..1caca3a411 100644
--- a/user-contrib/Ltac2/tac2intern.mli
+++ b/user-contrib/Ltac2/tac2intern.mli
@@ -46,3 +46,4 @@ val error_nparams_mismatch : ?loc:Loc.t -> int -> int -> 'a
 (** Misc *)
 
 val drop_ltac2_env : Genintern.Store.t -> Genintern.Store.t
+val check_ltac2_var : ?loc:Loc.t -> Genintern.Store.t -> Id.t -> 'a glb_typexpr -> unit
diff --git a/user-contrib/Ltac2/tac2quote.mli b/user-contrib/Ltac2/tac2quote.mli
index 0cef0e3a2b..da28e04df0 100644
--- a/user-contrib/Ltac2/tac2quote.mli
+++ b/user-contrib/Ltac2/tac2quote.mli
@@ -97,8 +97,8 @@ val wit_constr : (Constrexpr.constr_expr, Glob_term.glob_constr) Arg.tag
 
 val wit_open_constr : (Constrexpr.constr_expr, Glob_term.glob_constr) Arg.tag
 
-val wit_ltac1 : (Ltac_plugin.Tacexpr.raw_tactic_expr, Ltac_plugin.Tacexpr.glob_tactic_expr) Arg.tag
+val wit_ltac1 : (Id.t CAst.t list * Ltac_plugin.Tacexpr.raw_tactic_expr, Id.t list * Ltac_plugin.Tacexpr.glob_tactic_expr) Arg.tag
 (** Ltac1 AST quotation, seen as a 'tactic'. Its type is unit in Ltac2. *)
 
-val wit_ltac1val : (Ltac_plugin.Tacexpr.raw_tactic_expr, Ltac_plugin.Tacexpr.glob_tactic_expr) Arg.tag
+val wit_ltac1val : (Id.t CAst.t list * Ltac_plugin.Tacexpr.raw_tactic_expr, Id.t list * Ltac_plugin.Tacexpr.glob_tactic_expr) Arg.tag
 (** Ltac1 AST quotation, seen as a value-returning expression, with type Ltac1.t. *)
-- 
cgit v1.2.3


From 3d9f2d1cbc6256c48523db00fa2cc9743a843dfe Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 8 Jun 2019 21:10:12 +0200
Subject: Documenting the Ltac2 change.

---
 doc/sphinx/proof-engine/ltac2.rst | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index 36eeff6192..3812fd7631 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -850,8 +850,15 @@ a Ltac1 expression, and semantics of this quotation is the evaluation of the
 corresponding code for its side effects. In particular, it cannot return values,
 and the quotation has type :n:`unit`.
 
-Beware, Ltac1 **cannot** access variables from the Ltac2 scope. One is limited
-to the use of standalone function calls.
+Ltac1 **cannot** implicitly access variables from the Ltac2 scope, but this can
+be done via an explicit annotation to the :n:`ltac1` quotation.
+
+.. productionlist:: coq
+  ltac2_term : ltac1 : ( `ident` ... `ident` |- `ltac_expr` )
+
+The identifiers must be bound in the surrounding Ltac2 environment to values of
+type `Ltac2.Ltac1.t` (see below). This syntax will make them available to the
+quoted Ltac1 code as if they had been bound from Ltac1 itself.
 
 Low-level API
 +++++++++++++
@@ -869,6 +876,9 @@ focus is very hard. This is why some functions return a continuation-passing
 style value, as it can dispatch dynamically between focused and unfocused
 behaviour.
 
+The same mechanism for explicit binding of variables as described in the
+previous section applies.
+
 Ltac2 from Ltac1
 ~~~~~~~~~~~~~~~~
 
-- 
cgit v1.2.3


From e5c788f9efce9a9dd11910cd53c4a99451c48d8a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 9 Jun 2019 12:19:28 +0200
Subject: Give a functional type to Ltac1 quotations with a context.

This looks more principled, and doesn't require as much tinkering with
the typing implementation.
---
 doc/sphinx/proof-engine/ltac2.rst |  8 ++--
 test-suite/ltac2/compat.v         | 11 ++---
 user-contrib/Ltac2/tac2core.ml    | 88 +++++++++++++++++++++------------------
 user-contrib/Ltac2/tac2intern.ml  | 17 --------
 user-contrib/Ltac2/tac2intern.mli |  1 -
 5 files changed, 56 insertions(+), 69 deletions(-)

diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index 3812fd7631..3036648b08 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -856,9 +856,11 @@ be done via an explicit annotation to the :n:`ltac1` quotation.
 .. productionlist:: coq
   ltac2_term : ltac1 : ( `ident` ... `ident` |- `ltac_expr` )
 
-The identifiers must be bound in the surrounding Ltac2 environment to values of
-type `Ltac2.Ltac1.t` (see below). This syntax will make them available to the
-quoted Ltac1 code as if they had been bound from Ltac1 itself.
+The return type of this expression is a function of the same arity as the number
+of identifiers, with arguments of type `Ltac2.Ltac1.t` (see below). This syntax
+will bind the variables in the quoted Ltac1 code as if they had been bound from
+Ltac1 itself. Similarly, the arguments applied to the quotation will be passed
+at runtime to the Ltac1 code.
 
 Low-level API
 +++++++++++++
diff --git a/test-suite/ltac2/compat.v b/test-suite/ltac2/compat.v
index a24c9af10d..9c11d19c27 100644
--- a/test-suite/ltac2/compat.v
+++ b/test-suite/ltac2/compat.v
@@ -30,17 +30,14 @@ Fail Ltac2 pose1 (v : constr) :=
 (** Variables explicitly crossing the boundary must satisfy typing properties *)
 Goal True.
 Proof.
-(* Missing variable *)
-Fail ltac1:(x |- idtac).
 (* Wrong type *)
-Fail let x := 0 in ltac1:(x |- idtac).
+Fail ltac1:(x |- idtac) 0.
 (* OK, and runtime has access to variable *)
-let x := Ltac1.of_constr constr:(Type) in ltac1:(x |- idtac x).
+ltac1:(x |- idtac x) (Ltac1.of_constr constr:(Type)).
 
 (* Same for ltac1val *)
-Fail Ltac1.run ltac1val:(x |- idtac).
-Fail let x := 0 in Ltac1.run ltac1val:(x |- idtac).
-let x := Ltac1.of_constr constr:(Type) in Ltac1.run ltac1val:(x |- idtac x).
+Fail Ltac1.run (ltac1val:(x |- idtac) 0).
+Ltac1.run (ltac1val:(x |- idtac x) (Ltac1.of_constr constr:(Type))).
 Abort.
 
 (** Test calls to Ltac2 from Ltac1 *)
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index 781f8cd25c..a05612c1b1 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -1119,35 +1119,38 @@ let () =
 
 let () =
   let intern self ist (ids, tac) =
-    (* Check that variables have the Ltac1 type *)
-    let t_ltac1 = gtypref t_ltac1 in
-    let check { CAst.loc; v = id } =
-      let () = Tac2intern.check_ltac2_var ist.Genintern.extra ?loc id t_ltac1 in
-      id
-    in
-    let ids = List.map check ids in
+    let map { CAst.v = id } = id in
+    let ids = List.map map ids in
     (* Prevent inner calls to Ltac2 values *)
     let extra = Tac2intern.drop_ltac2_env ist.Genintern.extra in
     let ltacvars = List.fold_right Id.Set.add ids ist.Genintern.ltacvars in
     let ist = { ist with Genintern.extra; ltacvars } in
     let _, tac = Genintern.intern Ltac_plugin.Tacarg.wit_tactic ist tac in
-    GlbVal (ids, tac), gtypref t_unit
+    let fold ty _ = GTypArrow (gtypref t_ltac1, ty) in
+    let ty = List.fold_left fold (gtypref t_unit) ids in
+    GlbVal (ids, tac), ty
   in
-  let interp ist (ids, tac) =
-    let add lfun id =
-      let v = Id.Map.find id ist.env_ist in
-      let v = Tac2ffi.to_ext val_ltac1 v in
-      Id.Map.add id v lfun
+  let interp _ (ids, tac) =
+    let clos args =
+      let add lfun id v =
+        let v = Tac2ffi.to_ext val_ltac1 v in
+        Id.Map.add id v lfun
+      in
+      let lfun = List.fold_left2 add Id.Map.empty ids args in
+      let ist = { env_ist = Id.Map.empty } in
+      let lfun = Tac2interp.set_env ist lfun in
+      let ist = Ltac_plugin.Tacinterp.default_ist () in
+      let ist = { ist with Geninterp.lfun = lfun } in
+      let tac = (Ltac_plugin.Tacinterp.eval_tactic_ist ist tac : unit Proofview.tactic) in
+      let wrap (e, info) = set_bt info >>= fun info -> Proofview.tclZERO ~info e in
+      Proofview.tclOR tac wrap >>= fun () ->
+      return v_unit
     in
-    let lfun = List.fold_left add Id.Map.empty ids in
-    let ist = { env_ist = Id.Map.empty } in
-    let lfun = Tac2interp.set_env ist lfun in
-    let ist = Ltac_plugin.Tacinterp.default_ist () in
-    let ist = { ist with Geninterp.lfun = lfun } in
-    let tac = (Ltac_plugin.Tacinterp.eval_tactic_ist ist tac : unit Proofview.tactic) in
-    let wrap (e, info) = set_bt info >>= fun info -> Proofview.tclZERO ~info e in
-    Proofview.tclOR tac wrap >>= fun () ->
-    return v_unit
+    let len = List.length ids in
+    if Int.equal len 0 then
+      clos []
+    else
+      return (Tac2ffi.of_closure (Tac2ffi.abstract len clos))
   in
   let subst s (ids, tac) = (ids, Genintern.substitute Ltac_plugin.Tacarg.wit_tactic s tac) in
   let print env (ids, tac) =
@@ -1168,32 +1171,35 @@ let () =
 let () =
   let open Ltac_plugin in
   let intern self ist (ids, tac) =
-    (* Check that variables have the Ltac1 type *)
-    let t_ltac1 = gtypref t_ltac1 in
-    let check { CAst.loc; v = id } =
-      let () = Tac2intern.check_ltac2_var ist.Genintern.extra ?loc id t_ltac1 in
-      id
-    in
-    let ids = List.map check ids in
+    let map { CAst.v = id } = id in
+    let ids = List.map map ids in
     (* Prevent inner calls to Ltac2 values *)
     let extra = Tac2intern.drop_ltac2_env ist.Genintern.extra in
     let ltacvars = List.fold_right Id.Set.add ids ist.Genintern.ltacvars in
     let ist = { ist with Genintern.extra; ltacvars } in
     let _, tac = Genintern.intern Ltac_plugin.Tacarg.wit_tactic ist tac in
-    GlbVal (ids, tac), t_ltac1
+    let fold ty _ = GTypArrow (gtypref t_ltac1, ty) in
+    let ty = List.fold_left fold (gtypref t_ltac1) ids in
+    GlbVal (ids, tac), ty
   in
-  let interp ist (ids, tac) =
-    let add lfun id =
-      let v = Id.Map.find id ist.env_ist in
-      let v = Tac2ffi.to_ext val_ltac1 v in
-      Id.Map.add id v lfun
+  let interp _ (ids, tac) =
+    let clos args =
+      let add lfun id v =
+        let v = Tac2ffi.to_ext val_ltac1 v in
+        Id.Map.add id v lfun
+      in
+      let lfun = List.fold_left2 add Id.Map.empty ids args in
+      let ist = { env_ist = Id.Map.empty } in
+      let lfun = Tac2interp.set_env ist lfun in
+      let ist = Ltac_plugin.Tacinterp.default_ist () in
+      let ist = { ist with Geninterp.lfun = lfun } in
+      return (Value.of_ext val_ltac1 (Tacinterp.Value.of_closure ist tac))
     in
-    let lfun = List.fold_left add Id.Map.empty ids in
-    let ist = { env_ist = Id.Map.empty } in
-    let lfun = Tac2interp.set_env ist lfun in
-    let ist = Ltac_plugin.Tacinterp.default_ist () in
-    let ist = { ist with Geninterp.lfun = lfun } in
-    return (Value.of_ext val_ltac1 (Tacinterp.Value.of_closure ist tac))
+    let len = List.length ids in
+    if Int.equal len 0 then
+      clos []
+    else
+      return (Tac2ffi.of_closure (Tac2ffi.abstract len clos))
   in
   let subst s (ids, tac) = (ids, Genintern.substitute Tacarg.wit_tactic s tac) in
   let print env (ids, tac) =
diff --git a/user-contrib/Ltac2/tac2intern.ml b/user-contrib/Ltac2/tac2intern.ml
index 9538943635..0961e9c9c9 100644
--- a/user-contrib/Ltac2/tac2intern.ml
+++ b/user-contrib/Ltac2/tac2intern.ml
@@ -1191,23 +1191,6 @@ let intern_open_type t =
   let t = normalize env (count, vars) t in
   (!count, t)
 
-let rec get_closed = function
-| GTypVar _ -> assert false
-| GTypArrow (t, u) -> GTypArrow (get_closed t, get_closed u)
-| GTypRef (t, args) -> GTypRef (t, List.map get_closed args)
-
-let check_ltac2_var ?loc store id t =
-  let env = match Genintern.Store.get store ltac2_env with
-  | None -> empty_env ()
-  | Some env -> env
-  in
-  match Id.Map.find id env.env_var with
-  | sch ->
-    let t' = fresh_mix_type_scheme env sch in
-    unify ?loc env t' (get_closed t)
-  | exception Not_found ->
-    CErrors.user_err ?loc (Id.print id ++ str " is not a bound variable")
-
 (** Subtyping *)
 
 let check_subtype t1 t2 =
diff --git a/user-contrib/Ltac2/tac2intern.mli b/user-contrib/Ltac2/tac2intern.mli
index 1caca3a411..5e282a386a 100644
--- a/user-contrib/Ltac2/tac2intern.mli
+++ b/user-contrib/Ltac2/tac2intern.mli
@@ -46,4 +46,3 @@ val error_nparams_mismatch : ?loc:Loc.t -> int -> int -> 'a
 (** Misc *)
 
 val drop_ltac2_env : Genintern.Store.t -> Genintern.Store.t
-val check_ltac2_var : ?loc:Loc.t -> Genintern.Store.t -> Id.t -> 'a glb_typexpr -> unit
-- 
cgit v1.2.3