1 files changed, 21 insertions, 46 deletions
diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index e253cc382b..6512510f0a 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -18,7 +18,7 @@ module Value = Tac2ffi
 
 let return x = Proofview.tclUNIT x
 let v_unit = Value.of_unit ()
-let thaw f = Value.to_closure f [v_unit]
+let thaw f = Tac2ffi.apply (Value.to_closure f) [v_unit]
 
 let to_pair f g = function
 | ValBlk (0, [| x; y |]) -> (f x, g y)
@@ -189,46 +189,28 @@ let pname s = { mltac_plugin = "ltac2"; mltac_tactic = s }
 let lift tac = tac <*> return v_unit
 
 let define_prim0 name tac =
-  let tac arg = match arg with
-  | [_] -> lift tac
-  | _ -> assert false
-  in
-  Tac2env.define_primitive (pname name) tac
+  let tac _ = lift tac in
+  Tac2env.define_primitive (pname name) (MLTactic (OneAty, tac))
 
 let define_prim1 name tac =
-  let tac arg = match arg with
-  | [x] -> lift (tac x)
-  | _ -> assert false
-  in
-  Tac2env.define_primitive (pname name) tac
+  let tac x = lift (tac x) in
+  Tac2env.define_primitive (pname name) (MLTactic (OneAty, tac))
 
 let define_prim2 name tac =
-  let tac arg = match arg with
-  | [x; y] -> lift (tac x y)
-  | _ -> assert false
-  in
-  Tac2env.define_primitive (pname name) tac
+  let tac x y = lift (tac x y) in
+  Tac2env.define_primitive (pname name) (MLTactic (AddAty OneAty, tac))
 
 let define_prim3 name tac =
-  let tac arg = match arg with
-  | [x; y; z] -> lift (tac x y z)
-  | _ -> assert false
-  in
-  Tac2env.define_primitive (pname name) tac
+  let tac x y z = lift (tac x y z) in
+  Tac2env.define_primitive (pname name) (MLTactic (AddAty (AddAty OneAty), tac))
 
 let define_prim4 name tac =
-  let tac arg = match arg with
-  | [x; y; z; u] -> lift (tac x y z u)
-  | _ -> assert false
-  in
-  Tac2env.define_primitive (pname name) tac
+  let tac x y z u = lift (tac x y z u) in
+  Tac2env.define_primitive (pname name) (MLTactic (AddAty (AddAty (AddAty OneAty)), tac))
 
 let define_prim5 name tac =
-  let tac arg = match arg with
-  | [x; y; z; u; v] -> lift (tac x y z u v)
-  | _ -> assert false
-  in
-  Tac2env.define_primitive (pname name) tac
+  let tac x y z u v = lift (tac x y z u v) in
+  Tac2env.define_primitive (pname name) (MLTactic (AddAty (AddAty (AddAty (AddAty OneAty))), tac))
 
 (** Tactics from Tacexpr *)
 
@@ -401,26 +383,19 @@ end
 
 (** Reduction functions *)
 
+let lift tac = tac >>= fun c -> Proofview.tclUNIT (Value.of_constr c)
+
 let define_red1 name tac =
-  let tac arg = match arg with
-  | [x] -> tac x >>= fun c -> Proofview.tclUNIT (Value.of_constr c)
-  | _ -> assert false
-  in
-  Tac2env.define_primitive (pname name) tac
+  let tac x = lift (tac x) in
+  Tac2env.define_primitive (pname name) (MLTactic (OneAty, tac))
 
 let define_red2 name tac =
-  let tac arg = match arg with
-  | [x; y] -> tac x y >>= fun c -> Proofview.tclUNIT (Value.of_constr c)
-  | _ -> assert false
-  in
-  Tac2env.define_primitive (pname name) tac
+  let tac x y = lift (tac x y) in
+  Tac2env.define_primitive (pname name) (MLTactic (AddAty OneAty, tac))
 
 let define_red3 name tac =
-  let tac arg = match arg with
-  | [x; y; z] -> tac x y z >>= fun c -> Proofview.tclUNIT (Value.of_constr c)
-  | _ -> assert false
-  in
-  Tac2env.define_primitive (pname name) tac
+  let tac x y z = lift (tac x y z) in
+  Tac2env.define_primitive (pname name) (MLTactic (AddAty (AddAty OneAty), tac))
 
 let () = define_red1 "eval_red" begin fun c ->
   let c = Value.to_constr c in