1 files changed, 29 insertions, 14 deletions

diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index d9ac96d894..a0446bd6a0 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -141,16 +141,6 @@ let extract_trace ist = match TacStore.get ist.extra f_trace with
 | None -> []
 | Some l -> l
 
-module Value = struct
-
-  include Taccoerce.Value
-
-  let of_closure ist tac =
-    let closure = VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], tac) in
-    of_tacvalue closure
-
-end
-
 let print_top_val env v = Pptactic.pr_value Pptactic.ltop v
 
 let catching_error call_trace fail (e, info) =
@@ -1125,17 +1115,17 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
   | TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac)
   (* For extensions *)
   | TacAlias (loc,(s,l)) ->
-      let (ids, body) = Tacenv.interp_alias s in
+      let alias = Tacenv.interp_alias s in
       let (>>=) = Ftactic.bind in
       let interp_vars = Ftactic.List.map (fun v -> interp_tacarg ist v) l in
       let tac l =
         let addvar x v accu = Id.Map.add x v accu in
-        let lfun = List.fold_right2 addvar ids l ist.lfun in
+        let lfun = List.fold_right2 addvar alias.Tacenv.alias_args l ist.lfun in
         Ftactic.lift (push_trace (loc,LtacNotationCall s) ist) >>= fun trace ->
         let ist = {
           lfun = lfun;
           extra = TacStore.set ist.extra f_trace trace; } in
-        val_interp ist body >>= fun v ->
+        val_interp ist alias.Tacenv.alias_body >>= fun v ->
         Ftactic.lift (tactic_of_value ist v)
       in
       let tac =
@@ -1147,7 +1137,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
          some more elaborate solution will have to be used. *)
       in
       let tac =
-        let len1 = List.length ids in
+        let len1 = List.length alias.Tacenv.alias_args in
         let len2 = List.length l in
         if len1 = len2 then tac
         else Tacticals.New.tclZEROMSG (str "Arguments length mismatch: \
@@ -1860,6 +1850,31 @@ let eval_tactic_ist ist t =
   Proofview.tclLIFT db_initialize <*>
   interp_tactic ist t
 
+(** FFI *)
+
+module Value = struct
+
+  include Taccoerce.Value
+
+  let of_closure ist tac =
+    let closure = VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], tac) in
+    of_tacvalue closure
+
+  (** Apply toplevel tactic values *)
+  let apply (f : value) (args: value list) =
+    let fold arg (i, vars, lfun) =
+      let id = Id.of_string ("x" ^ string_of_int i) in
+      let x = Reference (ArgVar CAst.(make id)) in
+      (succ i, x :: vars, Id.Map.add id arg lfun)
+    in
+    let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in
+    let lfun = Id.Map.add (Id.of_string "F") f lfun in
+    let ist = { (default_ist ()) with lfun = lfun; } in
+    let tac = TacArg(Loc.tag @@ TacCall (Loc.tag (ArgVar CAst.(make @@ Id.of_string "F"),args))) in
+    eval_tactic_ist ist tac
+
+end
+
 (* globalization + interpretation *)