Introduction of the Ltac2 plugin.

For now, it is only a simple mini-ML whose effects are the proofview monad.
There is no facility to manipulate terms nor any hardwired tactic.

Pattern-matching is restricted to superficial constructors, the language is
lacking a lot of user-friendly interfaces, the grammar is crappy, and much
more.

15 files changed, 2173 insertions, 0 deletions

diff --git a/Ltac2.v b/Ltac2.v
new file mode 100644
index 0000000000..a952524e71
--- /dev/null
+++ b/Ltac2.v
@@ -0,0 +1,42 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+Declare ML Module "ltac2_plugin".
+
+Global Set Default Proof Mode "Ltac2".
+
+(** Primitive types *)
+
+Ltac2 Type int.
+Ltac2 Type string.
+Ltac2 Type constr.
+Ltac2 Type message.
+Ltac2 Type 'a array.
+
+(** Pervasive types *)
+
+Ltac2 Type 'a option := | None | Some ('a).
+
+(** Primitive tactics *)
+
+Module Message.
+
+Ltac2 @ external print : message -> unit := "ltac2" "print".
+Ltac2 @ external of_string : string -> message := "ltac2" "message_of_string".
+Ltac2 @ external of_int : int -> message := "ltac2" "message_of_int".
+
+End Message.
+
+Module Array.
+
+Ltac2 @external make : int -> 'a -> ('a) array := "ltac2" "array_make".
+Ltac2 @external length : ('a) array -> int := "ltac2" "array_length".
+Ltac2 @external get : ('a) array -> int -> 'a := "ltac2" "array_get".
+Ltac2 @external set : ('a) array -> int -> 'a -> unit := "ltac2" "array_set".
+
+End Array.
diff --git a/g_ltac2.ml4 b/g_ltac2.ml4
new file mode 100644
index 0000000000..349220f9de
--- /dev/null
+++ b/g_ltac2.ml4
@@ -0,0 +1,206 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Util
+open Genarg
+open Names
+open Pcoq
+open Tac2expr
+open Ltac_plugin
+
+let tac2expr = Gram.entry_create "tactic:tac2expr"
+let tac2type = Gram.entry_create "tactic:tac2type"
+let tac2def_val = Gram.entry_create "tactic:tac2def_val"
+let tac2def_typ = Gram.entry_create "tactic:tac2def_typ"
+let tac2def_ext = Gram.entry_create "tactic:tac2def_ext"
+let tac2mode = Gram.entry_create "vernac:ltac2_command"
+
+GEXTEND Gram
+  GLOBAL: tac2expr tac2type tac2def_val tac2def_typ tac2def_ext;
+  tac2pat:
+    [ "1" LEFTA
+      [ id = Prim.qualid; pl = LIST1 tac2pat LEVEL "0" -> CPatRef (!@loc, id, pl)
+      | id = Prim.qualid -> CPatRef (!@loc, id, []) ]
+    | "0"
+      [ "_" -> CPatAny (!@loc)
+      | "()" -> CPatTup (!@loc, [])
+      | id = Prim.qualid -> CPatRef (!@loc, id, [])
+      | "("; pl = LIST0 tac2pat LEVEL "1" SEP ","; ")" -> CPatTup (!@loc, pl) ]
+    ]
+  ;
+  tac2expr:
+    [ "5"
+      [ "fun"; it = LIST1 input_fun ; "=>"; body = tac2expr LEVEL "5" -> CTacFun (!@loc, it, body)
+      | "let"; isrec = rec_flag;
+          lc = LIST1 let_clause SEP "with"; "in";
+          e = tac2expr LEVEL "5" -> CTacLet (!@loc, isrec, lc, e)
+      | "match"; e = tac2expr LEVEL "5"; "with"; bl = branches ;"end" ->
+         CTacCse (!@loc, e, bl)
+      ]
+    | "2" LEFTA
+      [ e1 = tac2expr; ";"; e2 = tac2expr -> CTacSeq (!@loc, e1, e2) ]
+    | "1" LEFTA
+      [ e = tac2expr; el = LIST1 tac2expr LEVEL "0" -> CTacApp (!@loc, e, el)
+      | e0 = tac2expr; ","; el = LIST1 tac2expr LEVEL "0" SEP "," -> CTacTup (!@loc, e0 :: el) ]
+    | "0"
+      [ "("; a = tac2expr LEVEL "5"; ")" -> a
+      | "("; a = tac2expr; ":"; t = tac2type; ")" -> CTacCnv (!@loc, a, t)
+      | "()" -> CTacTup (!@loc, [])
+      | "("; ")" -> CTacTup (!@loc, [])
+      | "["; a = LIST0 tac2expr LEVEL "1" SEP ";"; "]" -> CTacLst (!@loc, a)
+      | a = tactic_atom -> a ]
+    ]
+  ;
+  branches:
+  [ [ -> []
+    | "|"; bl = LIST1 branch SEP "|" -> bl
+    | bl = LIST1 branch SEP "|" -> bl ]
+  ]
+  ;
+  branch:
+  [ [ pat = tac2pat LEVEL "1"; "=>"; e = tac2expr LEVEL "5" -> (pat, e) ] ]
+  ;
+  rec_flag:
+    [ [ IDENT "rec" -> true
+      | -> false ] ]
+  ;
+  typ_param:
+    [ [ "'"; id = Prim.ident -> id ] ]
+  ;
+  tactic_atom:
+    [ [ n = Prim.integer -> CTacAtm (!@loc, AtmInt n)
+      | s = Prim.string -> CTacAtm (!@loc, AtmStr s)
+      | id = Prim.qualid -> CTacRef id
+    ] ]
+  ;
+  let_clause:
+    [ [ id = binder; ":="; te = tac2expr ->
+         (id, None, te)
+      | id = binder; args = LIST1 input_fun; ":="; te = tac2expr ->
+         (id, None, CTacFun (!@loc, args, te)) ] ]
+  ;
+  tac2type:
+    [ "5" RIGHTA
+      [ t1 = tac2type; "->"; t2 = tac2type -> CTypArrow (!@loc, t1, t2) ]
+    | "2"
+      [ t = tac2type; "*"; tl = LIST1 tac2type SEP "*" -> CTypTuple (!@loc, t :: tl) ]
+    | "1"
+      [ "("; p = LIST1 tac2type LEVEL "5" SEP ","; ")"; qid = Prim.qualid -> CTypRef (!@loc, qid, p) ]
+    | "0"
+      [ "("; t = tac2type; ")"  -> t
+      | id = typ_param -> CTypVar (!@loc, Name id)
+      | "_" -> CTypVar (!@loc, Anonymous)
+      | qid = Prim.qualid -> CTypRef (!@loc, qid, []) ]
+    ];
+  locident:
+    [ [ id = Prim.ident -> (!@loc, id) ] ]
+  ;
+  binder:
+    [ [ "_" -> (!@loc, Anonymous)
+      | l = Prim.ident -> (!@loc, Name l) ] ]
+  ;
+  input_fun:
+    [ [ b = binder -> (b, None)
+      | "("; b = binder; ":"; t = tac2type; ")" -> (b, Some t) ] ]
+  ;
+  tac2def_body:
+    [ [ name = binder; it = LIST0 input_fun; ":="; e = tac2expr ->
+        let e = if List.is_empty it then e else CTacFun (!@loc, it, e) in
+        (name, e)
+    ] ]
+  ;
+  tac2def_val:
+    [ [ isrec = rec_flag; l = LIST1 tac2def_body SEP "with" ->
+        StrVal (isrec, l)
+    ] ]
+  ;
+  tac2typ_knd:
+    [ [ t = tac2type -> CTydDef (Some t)
+      | t = tac2alg_type -> CTydAlg t ] ]
+  ;
+  tac2alg_type:
+    [ [ -> []
+      | "|"; bl = LIST1 tac2alg_constructor SEP "|" -> bl ] ]
+  ;
+  tac2alg_constructor:
+    [ [ c = Prim.ident -> (c, [])
+      | c = Prim.ident; "("; args = LIST0 tac2type SEP ","; ")"-> (c, args) ] ]
+  ;
+  tac2typ_prm:
+    [ [ -> []
+      | id = typ_param -> [!@loc, id]
+      | "("; ids = LIST1 [ id = typ_param -> (!@loc, id) ] SEP "," ;")" -> ids
+    ] ]
+  ;
+  tac2typ_def:
+    [ [ prm = tac2typ_prm; id = locident; ":="; e = tac2typ_knd ->
+        (id, (prm, e))
+      | prm = tac2typ_prm; id = locident -> (id, (prm, CTydDef None))
+    ] ]
+  ;
+  tac2def_typ:
+    [ [ "Type"; isrec = rec_flag; l = LIST1 tac2typ_def SEP "with" ->
+        StrTyp (isrec, l)
+    ] ]
+  ;
+  tac2def_ext:
+    [ [ "@"; IDENT "external"; id = locident; ":"; t = tac2type LEVEL "5"; ":=";
+        plugin = Prim.string; name = Prim.string ->
+        let ml = { mltac_plugin = plugin; mltac_tactic = name } in
+        StrPrm (id, t, ml)
+    ] ]
+  ;
+END
+
+let pr_ltac2entry _ = mt () (** FIXME *)
+let pr_ltac2expr _ = mt () (** FIXME *)
+
+VERNAC ARGUMENT EXTEND ltac2_entry
+PRINTED BY pr_ltac2entry
+| [ tac2def_val(v) ] -> [ v ]
+| [ tac2def_typ(t) ] -> [ t ]
+| [ tac2def_ext(e) ] -> [ e ]
+END
+
+VERNAC COMMAND EXTEND VernacDeclareTactic2Definition CLASSIFIED AS SIDEFF
+| [ "Ltac2" ltac2_entry(e) ] -> [
+    let local = Locality.LocalityFixme.consume () in
+    Tac2entries.register_struct ?local e
+  ]
+END
+
+let _ =
+  let mode = {
+    Proof_global.name = "Ltac2";
+    set = (fun () -> set_command_entry tac2mode);
+    reset = (fun () -> set_command_entry Pcoq.Vernac_.noedit_mode);
+  } in
+  Proof_global.register_proof_mode mode
+
+VERNAC ARGUMENT EXTEND ltac2_expr
+PRINTED BY pr_ltac2expr
+| [ tac2expr(e) ] -> [ e ]
+END
+
+open G_ltac
+open Vernac_classifier
+
+VERNAC tac2mode EXTEND VernacLtac2
+| [ - ltac2_expr(t) ltac_use_default(default) ] =>
+    [ classify_as_proofstep ] -> [
+(*     let g = Option.default (Proof_global.get_default_goal_selector ()) g in *)
+    Tac2entries.call ~default t
+  ]
+END
+
+open Stdarg
+
+VERNAC COMMAND EXTEND Ltac2Print CLASSIFIED AS SIDEFF
+| [ "Print" "Ltac2" reference(tac) ] -> [ Tac2entries.print_ltac tac ]
+END
diff --git a/ltac2_plugin.mlpack b/ltac2_plugin.mlpack
new file mode 100644
index 0000000000..561bd0eb0a
--- /dev/null
+++ b/ltac2_plugin.mlpack
@@ -0,0 +1,6 @@
+Tac2env
+Tac2intern
+Tac2interp
+Tac2entries
+Tac2core
+G_ltac2
diff --git a/tac2core.ml b/tac2core.ml
new file mode 100644
index 0000000000..af4124e647
--- /dev/null
+++ b/tac2core.ml
@@ -0,0 +1,119 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open CSig
+open Pp
+open Names
+open Geninterp
+open Tac2expr
+open Proofview.Notations
+
+(** Standard values *)
+
+let coq_prefix = DirPath.make (List.map Id.of_string ["Ltac2"; "ltac2"; "Coq"])
+let coq_core n = KerName.make2 (MPfile coq_prefix) (Label.of_id (Id.of_string_soft n))
+
+module Core =
+struct
+
+let t_int = coq_core "int"
+let t_string = coq_core "string"
+let t_array = coq_core "array"
+let t_unit = coq_core "unit"
+let t_list = coq_core "list"
+
+let c_nil = coq_core "[]"
+let c_cons = coq_core "::"
+
+end
+
+open Core
+
+let v_unit = ValInt 0
+let v_nil = ValInt 0
+let v_cons v vl = ValBlk (0, [|v; vl|])
+
+module Value =
+struct
+
+let of_unit () = v_unit
+
+let to_unit = function
+| ValInt 0 -> ()
+| _ -> assert false
+
+let rec of_list = function
+| [] -> v_nil
+| x :: l -> v_cons x (of_list l)
+
+let rec to_list = function
+| ValInt 0 -> []
+| ValBlk (0, [|v; vl|]) -> v :: to_list vl
+| _ -> assert false
+
+end
+
+let extract_val (type a) (tag : a Val.typ) (Val.Dyn (tag', v)) : a =
+match Val.eq tag tag' with
+| None -> assert false
+| Some Refl -> v
+
+let val_pp = Val.create "ltac2:pp"
+let get_pp v = extract_val val_pp v
+
+(** Helper functions *)
+
+let return x = Proofview.tclUNIT x
+let pname s = { mltac_plugin = "ltac2"; mltac_tactic = s }
+
+let wrap f =
+  return () >>= fun () -> return (f ())
+
+let wrap_unit f =
+  return () >>= fun () -> f (); return v_unit
+
+(** Primitives *)
+
+let prm_print : ml_tactic = function
+| [ValExt pp] -> wrap_unit (fun () -> Feedback.msg_notice (get_pp pp))
+| _ -> assert false
+
+let prm_message_of_int : ml_tactic = function
+| [ValInt s] -> return (ValExt (Val.Dyn (val_pp, int s)))
+| _ -> assert false
+
+let prm_message_of_string : ml_tactic = function
+| [ValStr s] -> return (ValExt (Val.Dyn (val_pp, str s)))
+| _ -> assert false
+
+let prm_array_make : ml_tactic = function
+| [ValInt n; x] -> wrap (fun () -> ValBlk (0, Array.make n x))
+| _ -> assert false
+
+let prm_array_length : ml_tactic = function
+| [ValBlk (_, v)] -> return (ValInt (Array.length v))
+| _ -> assert false
+
+let prm_array_set : ml_tactic = function
+| [ValBlk (_, v); ValInt n; x] -> wrap_unit (fun () -> v.(n) <- x)
+| _ -> assert false
+
+let prm_array_get : ml_tactic = function
+| [ValBlk (_, v); ValInt n] -> wrap (fun () -> v.(n))
+| _ -> assert false
+
+(** Registering *)
+
+let () = Tac2env.define_primitive (pname "print") prm_print
+let () = Tac2env.define_primitive (pname "message_of_string") prm_message_of_string
+let () = Tac2env.define_primitive (pname "message_of_int") prm_message_of_int
+
+let () = Tac2env.define_primitive (pname "array_make") prm_array_make
+let () = Tac2env.define_primitive (pname "array_length") prm_array_length
+let () = Tac2env.define_primitive (pname "array_get") prm_array_get
+let () = Tac2env.define_primitive (pname "array_set") prm_array_set
diff --git a/tac2core.mli b/tac2core.mli
new file mode 100644
index 0000000000..14bde483c1
--- /dev/null
+++ b/tac2core.mli
@@ -0,0 +1,34 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Tac2env
+open Tac2expr
+
+(** {5 Hardwired data} *)
+
+module Core :
+sig
+
+val t_list : type_constant
+val c_nil : ltac_constant
+val c_cons : ltac_constant
+
+end
+
+(** {5 Ltac2 FFI} *)
+
+module Value :
+sig
+
+val of_unit : unit -> valexpr
+val to_unit : valexpr -> unit
+
+val of_list : valexpr list -> valexpr
+val to_list : valexpr -> valexpr list
+
+end
diff --git a/tac2entries.ml b/tac2entries.ml
new file mode 100644
index 0000000000..7572270ab3
--- /dev/null
+++ b/tac2entries.ml
@@ -0,0 +1,321 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Util
+open CErrors
+open Names
+open Libnames
+open Libobject
+open Nametab
+open Tac2expr
+open Tac2intern
+open Vernacexpr
+
+type tacdef = {
+  tacdef_local : bool;
+  tacdef_expr : glb_tacexpr;
+  tacdef_type : type_scheme;
+}
+
+let perform_tacdef visibility ((sp, kn), def) =
+  let () = if not def.tacdef_local then Tac2env.push_ltac visibility sp kn in
+  Tac2env.define_global kn (def.tacdef_expr, def.tacdef_type)
+
+let load_tacdef i obj = perform_tacdef (Until i) obj
+let open_tacdef i obj = perform_tacdef (Exactly i) obj
+
+let cache_tacdef ((sp, kn), def) =
+  let () = Tac2env.push_ltac (Until 1) sp kn in
+  Tac2env.define_global kn (def.tacdef_expr, def.tacdef_type)
+
+let subst_tacdef (subst, def) =
+  let expr' = subst_expr subst def.tacdef_expr in
+  let type' = subst_type_scheme subst def.tacdef_type in
+  if expr' == def.tacdef_expr && type' == def.tacdef_type then def
+  else { def with tacdef_expr = expr'; tacdef_type = type' }
+
+let classify_tacdef o = Substitute o
+
+let inTacDef : tacdef -> obj =
+  declare_object {(default_object "TAC2-DEFINITION") with
+     cache_function  = cache_tacdef;
+     load_function   = load_tacdef;
+     open_function   = open_tacdef;
+     subst_function = subst_tacdef;
+     classify_function = classify_tacdef}
+
+type typdef = {
+  typdef_local : bool;
+  typdef_expr : glb_quant_typedef;
+}
+
+let change_kn_label kn id =
+  let (mp, dp, _) = KerName.repr kn in
+  KerName.make mp dp (Label.of_id id)
+
+let change_sp_label sp id =
+  let (dp, _) = Libnames.repr_path sp in
+  Libnames.make_path dp id
+
+let push_typedef visibility sp kn (_, def) = match def with
+| GTydDef _ ->
+  Tac2env.push_type visibility sp kn
+| GTydAlg cstrs ->
+  (** Register constructors *)
+  let iter (c, _) =
+    let spc = change_sp_label sp c in
+    let knc = change_kn_label kn c in
+    Tac2env.push_ltac visibility spc knc
+  in
+  Tac2env.push_type visibility sp kn;
+  List.iter iter cstrs
+| GTydRec _ ->
+  assert false (** FIXME *)
+
+let next i =
+  let ans = !i in
+  let () = incr i in
+  ans
+
+let dummy_var i = Id.of_string (Printf.sprintf "_%i" i)
+
+let define_typedef kn (params, def as qdef) = match def with
+| GTydDef _ ->
+  Tac2env.define_type kn qdef
+| GTydAlg cstrs ->
+  (** Define constructors *)
+  let constant = ref 0 in
+  let nonconstant = ref 0 in
+  let iter (c, args) =
+    let knc = change_kn_label kn c in
+    let tag = if List.is_empty args then next constant else next nonconstant in
+    let ids = List.mapi (fun i _ -> dummy_var i) args in
+    let c = GTacCst (kn, tag, List.map (fun id -> GTacVar id) ids) in
+    let c =
+      if List.is_empty args then c
+      else GTacFun (List.map (fun id -> Name id) ids, c)
+    in
+    let fold arg tpe = GTypArrow (arg, tpe) in
+    let cT = GTypRef (kn, List.init params (fun i -> GTypVar i)) in
+    let cT = List.fold_right fold args cT in
+    let data = {
+      Tac2env.cdata_type = kn;
+      cdata_args = params, args;
+      cdata_indx = tag;
+    } in
+    Tac2env.define_constructor knc data;
+    Tac2env.define_global knc (c, (params, cT))
+  in
+  Tac2env.define_type kn qdef;
+  List.iter iter cstrs
+| GTydRec _ ->
+  assert false (** FIXME *)
+
+let perform_typdef vs ((sp, kn), def) =
+  let () = if not def.typdef_local then push_typedef vs sp kn def.typdef_expr in
+  define_typedef kn def.typdef_expr
+
+let load_typdef i obj = perform_typdef (Until i) obj
+let open_typdef i obj = perform_typdef (Exactly i) obj
+
+let cache_typdef ((sp, kn), def) =
+  let () = push_typedef (Until 1) sp kn def.typdef_expr in
+  define_typedef kn def.typdef_expr
+
+let subst_typdef (subst, def) =
+  let expr' = subst_quant_typedef subst def.typdef_expr in
+  if expr' == def.typdef_expr then def else { def with typdef_expr = expr' }
+
+let classify_typdef o = Substitute o
+
+let inTypDef : typdef -> obj =
+  declare_object {(default_object "TAC2-TYPE-DEFINITION") with
+     cache_function  = cache_typdef;
+     load_function   = load_typdef;
+     open_function   = open_typdef;
+     subst_function = subst_typdef;
+     classify_function = classify_typdef}
+
+let register_ltac ?(local = false) isrec tactics =
+  if isrec then
+    let map (na, e) = (na, None, e) in
+    let bindings = List.map map tactics in
+    let map ((loc, na), e) = match na with
+    | Anonymous -> None
+    | Name id ->
+      let qid = Libnames.qualid_of_ident id in
+      let e = CTacLet (Loc.ghost, true, bindings, CTacRef (loc, qid)) in
+      let (e, t) = intern e in
+      let e = match e with
+      | GTacLet (true, _, e) -> assert false
+      | _ -> assert false
+      in
+      Some (e, t)
+    in
+    let tactics = List.map map tactics in
+    assert false (** FIXME *)
+  else
+    let map ((loc, na), e) =
+      let (e, t) = intern e in
+      let () =
+        if not (is_value e) then
+          user_err ~loc (str "Tactic definition must be a syntactical value")
+      in
+      let id = match na with
+      | Anonymous ->
+        user_err ~loc (str "Tactic definition must have a name")
+      | Name id -> id
+      in
+      let kn = Lib.make_kn id in
+      let exists =
+        try let _ = Tac2env.interp_global kn in true with Not_found -> false
+      in
+      let () =
+        if exists then
+          user_err ~loc (str "Tactic " ++ Nameops.pr_id id ++ str " already exists")
+      in
+      (id, e, t)
+    in
+    let defs = List.map map tactics in
+    let iter (id, e, t) =
+      let def = {
+        tacdef_local = local;
+        tacdef_expr = e;
+        tacdef_type = t;
+      } in
+      ignore (Lib.add_leaf id (inTacDef def))
+    in
+    List.iter iter defs
+
+let register_type ?(local = false) isrec types =
+  let same_name ((_, id1), _) ((_, id2), _) = Id.equal id1 id2 in
+  let () = match List.duplicates same_name types with
+  | [] -> ()
+  | ((loc, id), _) :: _ ->
+    user_err ~loc (str "Multiple definition of the type name " ++ Id.print id)
+  in
+  let check ((loc, id), (params, def)) =
+    let same_name (_, id1) (_, id2) = Id.equal id1 id2 in
+    let () = match List.duplicates same_name params with
+    | [] -> ()
+    | (loc, id) :: _ ->
+      user_err ~loc (str "The type parameter " ++ Id.print id ++
+        str " occurs several times")
+    in
+    match def with
+    | CTydDef _ ->
+      if isrec then
+        user_err ~loc (str "The type abbreviation " ++ Id.print id ++
+          str " cannot be recursive")
+    | CTydAlg _ -> () (** FIXME *)
+    | CTydRec _ -> assert false (** FIXME *)
+  in
+  let () = List.iter check types in
+  let self =
+    if isrec then
+      let fold accu ((_, id), (params, _)) =
+        Id.Map.add id (Lib.make_kn id, List.length params) accu
+      in
+      List.fold_left fold Id.Map.empty types
+    else Id.Map.empty
+  in
+  let map ((_, id), def) =
+    let typdef = {
+      typdef_local = local;
+      typdef_expr = intern_typedef self def;
+    } in
+    (id, typdef)
+  in
+  let types = List.map map types in
+  let iter (id, def) = ignore (Lib.add_leaf id (inTypDef def)) in
+  List.iter iter types
+
+let register_primitive ?(local = false) (loc, id) t ml =
+  let t = intern_open_type t in
+  let rec count_arrow = function
+  | GTypArrow (_, t) -> 1 + count_arrow t
+  | _ -> 0
+  in
+  let arrows = count_arrow (snd t) in
+  let () = if Int.equal arrows 0 then
+    user_err ~loc (str "External tactic must have at least one argument") in
+  let () =
+    try let _ = Tac2env.interp_primitive ml in () with Not_found ->
+      user_err ~loc (str "Unregistered primitive " ++
+        quote (str ml.mltac_plugin) ++ spc () ++ quote (str ml.mltac_tactic))
+  in
+  let init i = Id.of_string (Printf.sprintf "x%i" i) in
+  let names = List.init arrows init in
+  let bnd = List.map (fun id -> Name id) names in
+  let arg = List.map (fun id -> GTacVar id) names in
+  let e = GTacFun (bnd, GTacPrm (ml, arg)) in
+  let def = {
+    tacdef_local = local;
+    tacdef_expr = e;
+    tacdef_type = t;
+  } in
+  ignore (Lib.add_leaf id (inTacDef def))
+
+let register_struct ?local str = match str with
+| StrVal (isrec, e) -> register_ltac ?local isrec e
+| StrTyp (isrec, t) -> register_type ?local isrec t
+| StrPrm (id, t, ml) -> register_primitive ?local id t ml
+
+(** Printing *)
+
+let print_ltac ref =
+  let (loc, qid) = qualid_of_reference ref in
+  let kn =
+    try Tac2env.locate_ltac qid
+    with Not_found -> user_err ~loc (str "Unknown tactic " ++ pr_qualid qid)
+  in
+  let (_, (_, t)) = Tac2env.interp_global kn in
+  Feedback.msg_notice (pr_qualid qid ++ spc () ++ str ":" ++ spc () ++ pr_glbtype t)
+
+(** Calling tactics *)
+
+let solve default tac =
+  let status = Proof_global.with_current_proof begin fun etac p ->
+    let with_end_tac = if default then Some etac else None in
+    let (p, status) = Pfedit.solve SelectAll None tac ?with_end_tac p in
+    (* in case a strict subtree was completed,
+       go back to the top of the prooftree *)
+    let p = Proof.maximal_unfocus Vernacentries.command_focus p in
+    p, status
+  end in
+  if not status then Feedback.feedback Feedback.AddedAxiom
+
+let call ~default e =
+  let loc = loc_of_tacexpr e in
+  let (e, (_, t)) = intern e in
+  let () = check_unit ~loc t in
+  let tac = Tac2interp.interp Id.Map.empty e in
+  solve default (Proofview.tclIGNORE tac)
+
+(** Primitive algebraic types than can't be defined Coq-side *)
+
+let register_prim_alg name params def =
+  let id = Id.of_string name in
+  let def = List.map (fun (cstr, tpe) -> (Id.of_string_soft cstr, tpe)) def in
+  let def = (params, GTydAlg def) in
+  let def = { typdef_local = false; typdef_expr = def } in
+  ignore (Lib.add_leaf id (inTypDef def))
+
+let coq_prefix = DirPath.make (List.map Id.of_string ["Ltac2"; "ltac2"; "Coq"])
+let coq_def n = KerName.make2 (MPfile coq_prefix) (Label.make n)
+
+let t_list = coq_def "list"
+
+let _ = Mltop.declare_cache_obj begin fun () ->
+  register_prim_alg "unit" 0 ["()", []];
+  register_prim_alg "list" 1 [
+    ("[]", []);
+    ("::", [GTypVar 0; GTypRef (t_list, [GTypVar 0])]);
+  ];
+end "ltac2_plugin"
diff --git a/tac2entries.mli b/tac2entries.mli
new file mode 100644
index 0000000000..9c5d0a15fd
--- /dev/null
+++ b/tac2entries.mli
@@ -0,0 +1,33 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Loc
+open Names
+open Tac2expr
+
+(** {5 Toplevel definitions} *)
+
+val register_ltac : ?local:bool -> rec_flag ->
+  (Name.t located * raw_tacexpr) list -> unit
+
+val register_type : ?local:bool -> rec_flag ->
+  (Id.t located * raw_quant_typedef) list -> unit
+
+val register_primitive : ?local:bool ->
+  Id.t located -> raw_typexpr -> ml_tactic_name -> unit
+
+val register_struct : ?local:bool -> strexpr -> unit
+
+(** {5 Inspecting} *)
+
+val print_ltac : Libnames.reference -> unit
+
+(** {5 Eval loop} *)
+
+(** Evaluate a tactic expression in the current environment *)
+val call : default:bool -> raw_tacexpr -> unit
diff --git a/tac2env.ml b/tac2env.ml
new file mode 100644
index 0000000000..d17e657516
--- /dev/null
+++ b/tac2env.ml
@@ -0,0 +1,139 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open CErrors
+open Util
+open Genarg
+open Names
+open Libnames
+open Tac2expr
+
+type ltac_constant = KerName.t
+type ltac_constructor = KerName.t
+type type_constant = KerName.t
+
+type constructor_data = {
+  cdata_type : type_constant;
+  cdata_args : int * int glb_typexpr list;
+  cdata_indx : int;
+}
+
+type ltac_state = {
+  ltac_tactics : (glb_tacexpr * type_scheme) KNmap.t;
+  ltac_constructors : constructor_data KNmap.t;
+  ltac_types : glb_quant_typedef KNmap.t;
+}
+
+let empty_state = {
+  ltac_tactics = KNmap.empty;
+  ltac_constructors = KNmap.empty;
+  ltac_types = KNmap.empty;
+}
+
+let ltac_state = Summary.ref empty_state ~name:"ltac2-state"
+
+(** Get a dynamic value from syntactical value *)
+let rec eval_pure = function
+| GTacAtm (AtmInt n) -> ValInt n
+| GTacRef kn ->
+  let (e, _) =
+    try KNmap.find kn ltac_state.contents.ltac_tactics
+    with Not_found -> assert false
+  in
+  eval_pure e
+| GTacFun (na, e) ->
+  ValCls { clos_env = Id.Map.empty; clos_var = na; clos_exp = e }
+| GTacTup el -> ValBlk (0, Array.map_of_list eval_pure el)
+| GTacCst (_, n, []) -> ValInt n
+| GTacCst (_, n, el) -> ValBlk (n, Array.map_of_list eval_pure el)
+| GTacAtm (AtmStr _) | GTacArr _ | GTacLet _ | GTacVar _
+| GTacApp _ | GTacCse _ | GTacPrm _ ->
+  anomaly (Pp.str "Term is not a syntactical value")
+
+let define_global kn e =
+  let state = !ltac_state in
+  ltac_state := { state with ltac_tactics = KNmap.add kn e state.ltac_tactics }
+
+let interp_global kn =
+  let (e, t) = KNmap.find kn ltac_state.contents.ltac_tactics in
+  (eval_pure e, t)
+
+let define_constructor kn t =
+  let state = !ltac_state in
+  ltac_state := { state with ltac_constructors = KNmap.add kn t state.ltac_constructors }
+
+let interp_constructor kn = KNmap.find kn ltac_state.contents.ltac_constructors
+
+let define_type kn e =
+  let state = !ltac_state in
+  ltac_state := { state with ltac_types = KNmap.add kn e state.ltac_types }
+
+let interp_type kn = KNmap.find kn ltac_state.contents.ltac_types
+
+module ML =
+struct
+  type t = ml_tactic_name
+  let compare n1 n2 =
+    let c = String.compare n1.mltac_plugin n2.mltac_plugin in
+    if Int.equal c 0 then String.compare n1.mltac_tactic n2.mltac_tactic
+    else c
+end
+
+module MLMap = Map.Make(ML)
+
+let primitive_map = ref MLMap.empty
+
+let define_primitive name f = primitive_map := MLMap.add name f !primitive_map
+let interp_primitive name = MLMap.find name !primitive_map
+
+(** Name management *)
+
+module FullPath =
+struct
+  type t = full_path
+  let equal = eq_full_path
+  let to_string = string_of_path
+  let repr sp =
+    let dir,id = repr_path sp in
+    id, (DirPath.repr dir)
+end
+
+module KnTab = Nametab.Make(FullPath)(KerName)
+
+type nametab = {
+  tab_ltac : KnTab.t;
+  tab_type : KnTab.t;
+}
+
+let empty_nametab = { tab_ltac = KnTab.empty; tab_type = KnTab.empty }
+
+let nametab = Summary.ref empty_nametab ~name:"ltac2-nametab"
+
+let push_ltac vis sp kn =
+  let tab = !nametab in
+  nametab := { tab with tab_ltac = KnTab.push vis sp kn tab.tab_ltac }
+
+let locate_ltac qid =
+  let tab = !nametab in
+  KnTab.locate qid tab.tab_ltac
+
+let locate_extended_all_ltac qid =
+  let tab = !nametab in
+  KnTab.find_prefixes qid tab.tab_ltac
+
+let push_type vis sp kn =
+  let tab = !nametab in
+  nametab := { tab with tab_type = KnTab.push vis sp kn tab.tab_type }
+
+let locate_type qid =
+  let tab = !nametab in
+  KnTab.locate qid tab.tab_type
+
+let locate_extended_all_type qid =
+  let tab = !nametab in
+  KnTab.find_prefixes qid tab.tab_type
diff --git a/tac2env.mli b/tac2env.mli
new file mode 100644
index 0000000000..efabdb5466
--- /dev/null
+++ b/tac2env.mli
@@ -0,0 +1,58 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Genarg
+open Names
+open Libnames
+open Nametab
+open Tac2expr
+
+(** Ltac2 global environment *)
+
+type ltac_constant = KerName.t
+type ltac_constructor = KerName.t
+type type_constant = KerName.t
+
+(** {5 Toplevel definition of values} *)
+
+val define_global : ltac_constant -> (glb_tacexpr * type_scheme) -> unit
+val interp_global : ltac_constant -> (valexpr * type_scheme)
+
+(** {5 Toplevel definition of types} *)
+
+val define_type : type_constant -> glb_quant_typedef -> unit
+val interp_type : type_constant -> glb_quant_typedef
+
+(** {5 Toplevel definition of algebraic constructors} *)
+
+type constructor_data = {
+  cdata_type : type_constant;
+  cdata_args : int * int glb_typexpr list;
+  cdata_indx : int;
+}
+
+val define_constructor : ltac_constructor -> constructor_data -> unit
+val interp_constructor : ltac_constructor -> constructor_data
+
+(** {5 Name management} *)
+
+val push_ltac : visibility -> full_path -> ltac_constant -> unit
+val locate_ltac : qualid -> ltac_constant
+val locate_extended_all_ltac : qualid -> ltac_constant list
+
+val push_type : visibility -> full_path -> type_constant -> unit
+val locate_type : qualid -> type_constant
+val locate_extended_all_type : qualid -> type_constant list
+
+(** {5 Toplevel definitions of ML tactics} *)
+
+(** This state is not part of the summary, contrarily to the ones above. It is
+    intended to be used from ML plugins to register ML-side functions. *)
+
+val define_primitive : ml_tactic_name -> ml_tactic -> unit
+val interp_primitive : ml_tactic_name -> ml_tactic
diff --git a/tac2expr.mli b/tac2expr.mli
new file mode 100644
index 0000000000..445c69aa23
--- /dev/null
+++ b/tac2expr.mli
@@ -0,0 +1,136 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Loc
+open Genarg
+open Names
+open Libnames
+
+type mutable_flag = bool
+type rec_flag = bool
+type lid = Id.t
+type uid = Id.t
+
+(** {5 Misc} *)
+
+type ml_tactic_name = {
+  mltac_plugin : string;
+  mltac_tactic : string;
+}
+
+(** {5 Type syntax} *)
+
+type raw_typexpr =
+| CTypVar of Name.t located
+| CTypArrow of Loc.t * raw_typexpr * raw_typexpr
+| CTypTuple of Loc.t * raw_typexpr list
+| CTypRef of Loc.t * qualid located * raw_typexpr list
+
+type raw_typedef =
+| CTydDef of raw_typexpr option
+| CTydAlg of (uid * raw_typexpr list) list
+| CTydRec of (lid * mutable_flag * raw_typexpr) list
+
+type 'a glb_typexpr =
+| GTypVar of 'a
+| GTypArrow of 'a glb_typexpr * 'a glb_typexpr
+| GTypTuple of 'a glb_typexpr list
+| GTypRef of KerName.t * 'a glb_typexpr list
+
+type glb_typedef =
+| GTydDef of int glb_typexpr option
+| GTydAlg of (uid * int glb_typexpr list) list
+| GTydRec of (lid * mutable_flag * int glb_typexpr) list
+
+type type_scheme = int * int glb_typexpr
+
+type raw_quant_typedef = Id.t located list * raw_typedef
+type glb_quant_typedef = int * glb_typedef
+
+(** {5 Term syntax} *)
+
+type atom =
+| AtmInt of int
+| AtmStr of string
+
+(** Tactic expressions *)
+type raw_patexpr =
+| CPatAny of Loc.t
+| CPatRef of Loc.t * qualid located * raw_patexpr list
+| CPatTup of raw_patexpr list located
+
+type raw_tacexpr =
+| CTacAtm of atom located
+| CTacRef of qualid located
+| CTacFun of Loc.t * (Name.t located * raw_typexpr option) list * raw_tacexpr
+| CTacApp of Loc.t * raw_tacexpr * raw_tacexpr list
+| CTacLet of Loc.t * rec_flag * (Name.t located * raw_typexpr option * raw_tacexpr) list * raw_tacexpr
+| CTacTup of raw_tacexpr list located
+| CTacArr of raw_tacexpr list located
+| CTacLst of raw_tacexpr list located
+| CTacCnv of Loc.t * raw_tacexpr * raw_typexpr
+| CTacSeq of Loc.t * raw_tacexpr * raw_tacexpr
+| CTacCse of Loc.t * raw_tacexpr * raw_taccase list
+
+and raw_taccase = raw_patexpr * raw_tacexpr
+
+type case_info =
+| GCaseTuple of int
+| GCaseAlg of KerName.t
+
+type glb_tacexpr =
+| GTacAtm of atom
+| GTacVar of Id.t
+| GTacRef of KerName.t
+| GTacFun of Name.t list * glb_tacexpr
+| GTacApp of glb_tacexpr * glb_tacexpr list
+| GTacLet of rec_flag * (Name.t * glb_tacexpr) list * glb_tacexpr
+| GTacTup of glb_tacexpr list
+| GTacArr of glb_tacexpr list
+| GTacCst of KerName.t * int * glb_tacexpr list
+| GTacCse of glb_tacexpr * case_info * glb_tacexpr array * (Name.t array * glb_tacexpr) array
+| GTacPrm of ml_tactic_name * glb_tacexpr list
+
+(** Toplevel statements *)
+type strexpr =
+| StrVal of rec_flag * (Name.t located * raw_tacexpr) list
+| StrTyp of rec_flag * (Id.t located * raw_quant_typedef) list
+| StrPrm of Id.t located * raw_typexpr * ml_tactic_name
+
+(** {5 Dynamic semantics} *)
+
+(** Values are represented in a way similar to OCaml, i.e. they constrast
+    immediate integers (integers, constructors without arguments) and structured
+    blocks (tuples, arrays, constructors with arguments), as well as a few other
+    base cases, namely closures, strings and dynamic type coming from the Coq
+    implementation. *)
+
+type tag = int
+
+type valexpr =
+| ValInt of int
+  (** Immediate integers *)
+| ValBlk of tag * valexpr array
+  (** Structured blocks *)
+| ValStr of string
+  (** Strings *)
+| ValCls of closure
+  (** Closures *)
+| ValExt of Geninterp.Val.t
+  (** Arbitrary data *)
+
+and closure = {
+  mutable clos_env : valexpr Id.Map.t;
+  (** Mutable so that we can implement recursive functions imperatively *)
+  clos_var : Name.t list;
+  (** Bound variables *)
+  clos_exp : glb_tacexpr;
+  (** Body *)
+}
+
+type ml_tactic = valexpr list -> valexpr Proofview.tactic
diff --git a/tac2intern.ml b/tac2intern.ml
new file mode 100644
index 0000000000..b1b35b0787
--- /dev/null
+++ b/tac2intern.ml
@@ -0,0 +1,921 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Util
+open Genarg
+open CErrors
+open Names
+open Libnames
+open Misctypes
+open Tac2env
+open Tac2expr
+
+(** Hardwired types and constants *)
+
+let coq_prefix = DirPath.make (List.map Id.of_string ["Ltac2"; "ltac2"; "Coq"])
+let coq_type n = KerName.make2 (MPfile coq_prefix) (Label.make n)
+
+let t_int = coq_type "int"
+let t_string = coq_type "string"
+let t_array = coq_type "array"
+let t_unit = coq_type "unit"
+let t_list = coq_type "list"
+
+let c_nil = GTacCst (t_list, 0, [])
+let c_cons e el = GTacCst (t_list, 0, [e; el])
+
+(** Union find *)
+
+module UF :
+sig
+type elt
+type 'a t
+val equal : elt -> elt -> bool
+val create : unit -> 'a t
+val fresh : 'a t -> elt
+val size : 'a t -> int
+val find : elt -> 'a t -> (elt * 'a option)
+val union : elt -> elt -> 'a t -> unit
+val set : elt -> 'a -> 'a t -> unit
+module Map :
+sig
+  type key = elt
+  type +'a t
+  val empty : 'a t
+  val add : key -> 'a -> 'a t -> 'a t
+  val mem : key -> 'a t -> bool
+  val find : key -> 'a t -> 'a
+end
+end
+=
+struct
+type elt = int
+let equal = Int.equal
+module Map = Int.Map
+
+type 'a node =
+| Canon of int * 'a option
+| Equiv of elt
+
+type 'a t = {
+  mutable uf_data : 'a node array;
+  mutable uf_size : int;
+}
+
+let size p = p.uf_size
+
+let resize p =
+  if Int.equal (Array.length p.uf_data) p.uf_size then begin
+    let nsize = 2 * p.uf_size + 1 in
+    let v = Array.make nsize (Equiv 0) in
+    Array.blit p.uf_data 0 v 0 (Array.length p.uf_data);
+    p.uf_data <- v;
+  end
+
+let create () = { uf_data = [||]; uf_size = 0 }
+
+let fresh p =
+  resize p;
+  let n = p.uf_size in
+  p.uf_data.(n) <- (Canon (1, None));
+  p.uf_size <- n + 1;
+  n
+
+let rec lookup n p =
+  let node = Array.get p.uf_data n in
+  match node with
+  | Canon (size, v) -> n, size, v
+  | Equiv y ->
+    let ((z, _, _) as res) = lookup y p in
+    if not (Int.equal z y) then Array.set p.uf_data n (Equiv z);
+    res
+
+let find n p =
+  let (x, _, v) = lookup n p in (x, v)
+
+let union x y p =
+  let ((x, size1, _) as xcan) = lookup x p in
+  let ((y, size2, _) as ycan) = lookup y p in
+  let xcan, ycan = if size1 < size2 then xcan, ycan else ycan, xcan in
+  let x, _, xnode = xcan in
+  let y, _, ynode = ycan in
+  assert (Option.is_empty xnode);
+  assert (Option.is_empty ynode);
+  p.uf_data.(x) <- Equiv y;
+  p.uf_data.(y) <- Canon (size1 + size2, None)
+
+let set x v p =
+  let (x, s, v') = lookup x p in
+  assert (Option.is_empty v');
+  p.uf_data.(x) <- Canon (s, Some v)
+
+end
+
+type mix_var =
+| GVar of UF.elt
+| LVar of int
+
+type mix_type_scheme = int * mix_var glb_typexpr
+
+type environment = {
+  env_var : mix_type_scheme Id.Map.t;
+  (** Type schemes of bound variables *)
+  env_cst : UF.elt glb_typexpr UF.t;
+  (** Unification state *)
+  env_als : UF.elt Id.Map.t ref;
+  (** Map user-facing type variables to unification variables *)
+  env_opn : bool;
+  (** Accept unbound type variables *)
+  env_rec : (KerName.t * int) Id.Map.t;
+  (** Recursive type definitions *)
+}
+
+let empty_env () = {
+  env_var = Id.Map.empty;
+  env_cst = UF.create ();
+  env_als = ref Id.Map.empty;
+  env_opn = true;
+  env_rec = Id.Map.empty;
+}
+
+let fresh_id env = UF.fresh env.env_cst
+
+let get_alias (loc, id) env =
+  try Id.Map.find id env.env_als.contents
+  with Not_found ->
+    if env.env_opn then
+      let n = fresh_id env in
+      let () = env.env_als := Id.Map.add id n env.env_als.contents in
+      n
+    else user_err ~loc (str "Unbound type parameter " ++ Id.print id)
+
+let push_name id t env = match id with
+| Anonymous -> env
+| Name id -> { env with env_var = Id.Map.add id t env.env_var }
+
+let loc_of_tacexpr = function
+| CTacAtm (loc, _) -> loc
+| CTacRef (loc, _) -> loc
+| CTacFun (loc, _, _) -> loc
+| CTacApp (loc, _, _) -> loc
+| CTacLet (loc, _, _, _) -> loc
+| CTacTup (loc, _) -> loc
+| CTacArr (loc, _) -> loc
+| CTacLst (loc, _) -> loc
+| CTacCnv (loc, _, _) -> loc
+| CTacSeq (loc, _, _) -> loc
+| CTacCse (loc, _, _) -> loc
+
+let loc_of_patexpr = function
+| CPatAny loc -> loc
+| CPatRef (loc, _, _) -> loc
+| CPatTup (loc, _) -> loc
+
+let rec subst_type subst (t : 'a glb_typexpr) = match t with
+| GTypVar id -> subst id
+| GTypArrow (t1, t2) -> GTypArrow (subst_type subst t1, subst_type subst t2)
+| GTypTuple tl -> GTypTuple (List.map (fun t -> subst_type subst t) tl)
+| GTypRef (qid, args) ->
+  GTypRef (qid, List.map (fun t -> subst_type subst t) args)
+
+let rec intern_type env (t : raw_typexpr) : UF.elt glb_typexpr = match t with
+| CTypVar (loc, Name id) -> GTypVar (get_alias (loc, id) env)
+| CTypVar (_, Anonymous) -> GTypVar (fresh_id env)
+| CTypRef (_, (loc, qid), args) ->
+  let (dp, id) = repr_qualid qid in
+  let (kn, nparams) =
+    if DirPath.is_empty dp && Id.Map.mem id env.env_rec then
+      Id.Map.find id env.env_rec
+    else
+      let kn =
+        try Tac2env.locate_type qid
+        with Not_found ->
+          user_err ~loc (str "Unbound type constructor " ++ pr_qualid qid)
+      in
+      let (nparams, _) = Tac2env.interp_type kn in
+      (kn, nparams)
+  in
+  let nargs = List.length args in
+  let () =
+    if not (Int.equal nparams nargs) then
+      user_err ~loc (strbrk "The type constructor " ++ pr_qualid qid ++
+        strbrk " expects " ++ int nparams ++ strbrk " argument(s), but is here \
+        applied to " ++ int nargs ++ strbrk "argument(s)")
+  in
+  GTypRef (kn, List.map (fun t -> intern_type env t) args)
+| CTypArrow (loc, t1, t2) -> GTypArrow (intern_type env t1, intern_type env t2)
+| CTypTuple (loc, tl) -> GTypTuple (List.map (fun t -> intern_type env t) tl)
+
+let fresh_type_scheme env (t : type_scheme) : UF.elt glb_typexpr =
+  let (n, t) = t in
+  let subst = Array.init n (fun _ -> fresh_id env) in
+  let substf i = GTypVar subst.(i) in
+  subst_type substf t
+
+let fresh_mix_type_scheme env (t : mix_type_scheme) : UF.elt glb_typexpr =
+  let (n, t) = t in
+  let subst = Array.init n (fun _ -> fresh_id env) in
+  let substf = function
+  | LVar i -> GTypVar subst.(i)
+  | GVar n -> GTypVar n
+  in
+  subst_type substf t
+
+let fresh_reftype env (kn : KerName.t) =
+  let (n, _) = Tac2env.interp_type kn in
+  let subst = Array.init n (fun _ -> fresh_id env) in
+  let t = GTypRef (kn, Array.map_to_list (fun i -> GTypVar i) subst) in
+  (subst, t)
+
+(** First-order unification algorithm *)
+
+let is_unfoldable kn = match snd (Tac2env.interp_type kn) with
+| GTydDef (Some _) -> true
+| GTydDef None | GTydAlg _ | GTydRec _ -> false
+
+let unfold env kn args =
+  let (nparams, def) = Tac2env.interp_type kn in
+  let def = match def with
+  | GTydDef (Some t) -> t
+  | _ -> assert false
+  in
+  let args = Array.of_list args in
+  let subst n = args.(n) in
+  subst_type subst def
+
+(** View function, allows to ensure head normal forms *)
+let rec kind env t = match t with
+| GTypVar id ->
+  let (id, v) = UF.find id env.env_cst in
+  begin match v with
+  | None -> GTypVar id
+  | Some t -> kind env t
+  end
+| GTypRef (kn, tl) ->
+  if is_unfoldable kn then kind env (unfold env kn tl) else t
+| GTypArrow _ | GTypTuple _ -> t
+
+exception Occur
+
+let rec occur_check env id t = match kind env t with
+| GTypVar id' -> if UF.equal id id' then raise Occur
+| GTypArrow (t1, t2) ->
+  let () = occur_check env id t1 in
+  occur_check env id t2
+| GTypTuple tl ->
+  List.iter (fun t -> occur_check env id t) tl
+| GTypRef (kn, tl) ->
+  List.iter (fun t -> occur_check env id t) tl
+
+exception CannotUnify of UF.elt glb_typexpr * UF.elt glb_typexpr
+
+let unify_var env id t = match kind env t with
+| GTypVar id' ->
+  if not (UF.equal id id') then UF.union id id' env.env_cst
+| GTypArrow _ | GTypRef _ | GTypTuple _ ->
+  try
+    let () = occur_check env id t in
+    UF.set id t env.env_cst
+  with Occur -> raise (CannotUnify (GTypVar id, t))
+
+let rec unify env t1 t2 = match kind env t1, kind env t2 with
+| GTypVar id, t | t, GTypVar id ->
+  unify_var env id t
+| GTypArrow (t1, u1), GTypArrow (t2, u2) ->
+  let () = unify env t1 t2 in
+  unify env u1 u2
+| GTypTuple tl1, GTypTuple tl2 ->
+  if Int.equal (List.length tl1) (List.length tl2) then
+    List.iter2 (fun t1 t2 -> unify env t1 t2) tl1 tl2
+  else raise (CannotUnify (t1, t2))
+| GTypRef (kn1, tl1), GTypRef (kn2, tl2) ->
+  if KerName.equal kn1 kn2 then
+    List.iter2 (fun t1 t2 -> unify env t1 t2) tl1 tl2
+  else raise (CannotUnify (t1, t2))
+| _ -> raise (CannotUnify (t1, t2))
+
+(** FIXME *)
+let rec pr_glbtype = function
+| GTypVar n -> str "?"
+| GTypRef (kn, tl) ->
+  KerName.print kn ++ str "(" ++ prlist_with_sep (fun () -> str ", ") pr_glbtype tl ++ str ")"
+| GTypArrow (t1, t2) -> str "Arr(" ++ pr_glbtype t1 ++ str ", " ++ pr_glbtype t2 ++ str ")"
+| GTypTuple tl -> str "Tup(" ++ prlist_with_sep (fun () -> str ", ") pr_glbtype tl ++ str ")"
+
+let unify loc env t1 t2 =
+  try unify env t1 t2
+  with CannotUnify (u1, u2) ->
+    user_err ~loc (str "This expression has type " ++ pr_glbtype t1 ++
+      str " but an expression what expected of type " ++ pr_glbtype t2)
+
+(** Term typing *)
+
+let rec is_value = function
+| GTacAtm (AtmInt _) | GTacVar _ | GTacRef _ | GTacFun _ -> true
+| GTacAtm (AtmStr _) | GTacApp _ | GTacLet _ -> false
+| GTacTup el -> List.for_all is_value el
+| GTacCst (_, _, []) -> true
+| GTacCst (kn, n, el) ->
+  (** To be a value, a constructor must be immutable *)
+  assert false (** TODO *)
+| GTacArr _ | GTacCse _ | GTacPrm _ -> false
+
+let is_rec_rhs = function
+| GTacFun _ -> true
+| GTacAtm _ | GTacVar _ | GTacRef _ | GTacApp _ | GTacLet _ -> false
+| GTacTup _ | GTacArr _ | GTacPrm _ | GTacCst _ | GTacCse _ -> false
+
+let rec fv_type f t accu = match t with
+| GTypVar id -> f id accu
+| GTypArrow (t1, t2) -> fv_type f t1 (fv_type f t2 accu)
+| GTypTuple tl -> List.fold_left (fun accu t -> fv_type f t accu) accu tl
+| GTypRef (kn, tl) -> List.fold_left (fun accu t -> fv_type f t accu) accu tl
+
+let fv_env env =
+  let rec f id accu = match UF.find id env.env_cst with
+  | id, None -> UF.Map.add id () accu
+  | _, Some t -> fv_type f t accu
+  in
+  let fold_var id (_, t) accu =
+    let fmix id accu = match id with
+    | LVar _ -> accu
+    | GVar id -> f id accu
+    in
+    fv_type fmix t accu
+  in
+  let fv_var = Id.Map.fold fold_var env.env_var UF.Map.empty in
+  let fold_als _ id accu = f id accu in
+  Id.Map.fold fold_als !(env.env_als) fv_var
+
+let abstract_var env (t : UF.elt glb_typexpr) : mix_type_scheme =
+  let fv = fv_env env in
+  let count = ref 0 in
+  let vars = ref UF.Map.empty in
+  let rec subst id =
+    let (id, t) = UF.find id env.env_cst in
+    match t with
+    | None ->
+      if UF.Map.mem id fv then GTypVar (GVar id)
+      else
+        begin try UF.Map.find id !vars
+        with Not_found ->
+          let n = !count in
+          let var = GTypVar (LVar n) in
+          let () = incr count in
+          let () = vars := UF.Map.add id var !vars in
+          var
+        end
+    | Some t -> subst_type subst t
+  in
+  let t = subst_type subst t in
+  (!count, t)
+
+let monomorphic (t : UF.elt glb_typexpr) : mix_type_scheme =
+  let subst id = GTypVar (GVar id) in
+  (0, subst_type subst t)
+
+let warn_not_unit =
+  CWarnings.create ~name:"not-unit" ~category:"ltac"
+    (fun () -> strbrk "The following expression should have type unit.")
+
+let warn_redundant_clause =
+  CWarnings.create ~name:"redundant-clause" ~category:"ltac"
+    (fun () -> strbrk "The following clause is redundant.")
+
+let check_elt_unit loc env t =
+  let maybe_unit = match kind env t with
+  | GTypVar _ -> true
+  | GTypArrow _ | GTypTuple _ -> false
+  | GTypRef (kn, _) -> KerName.equal kn t_unit
+  in
+  if not maybe_unit then warn_not_unit ~loc ()
+
+let check_elt_empty loc env t = match kind env t with
+| GTypVar _ ->
+  user_err ~loc (str "Cannot infer an empty type for this expression")
+| GTypArrow _ | GTypTuple _ ->
+  user_err ~loc (str "Type " ++ pr_glbtype t ++ str " is not an empty type")
+| GTypRef (kn, _) ->
+  let def = Tac2env.interp_type kn in
+  match def with
+  | _, GTydAlg [] -> kn
+  | _ ->
+    user_err ~loc (str "Type " ++ pr_glbtype t ++ str " is not an empty type")
+
+let check_unit ?loc t =
+  let maybe_unit = match t with
+  | GTypVar _ -> true
+  | GTypArrow _ | GTypTuple _ -> false
+  | GTypRef (kn, _) -> KerName.equal kn t_unit
+  in
+  if not maybe_unit then warn_not_unit ?loc ()
+
+let check_redundant_clause = function
+| [] -> ()
+| (p, _) :: _ -> warn_redundant_clause ~loc:(loc_of_patexpr p) ()
+
+let get_variable env (loc, qid) =
+  let (dp, id) = repr_qualid qid in
+  if DirPath.is_empty dp && Id.Map.mem id env.env_var then ArgVar (loc, id)
+  else
+    let kn =
+      try Tac2env.locate_ltac qid
+      with Not_found ->
+        CErrors.user_err ~loc (str "Unbound value " ++ pr_qualid qid)
+    in
+    ArgArg kn
+
+let get_constructor env (loc, qid) =
+  let c = try Some (Tac2env.locate_ltac qid) with Not_found -> None in
+  match c with
+  | Some knc ->
+    let kn =
+      try Tac2env.interp_constructor knc
+      with Not_found ->
+        CErrors.user_err ~loc (str "The term " ++ pr_qualid qid ++
+          str " is not the constructor of an inductive type.")    in
+    ArgArg (kn, knc)
+  | None ->
+    let (dp, id) = repr_qualid qid in
+    if DirPath.is_empty dp then ArgVar (loc, id)
+    else CErrors.user_err ~loc (str "Unbound constructor " ++ pr_qualid qid)
+
+let intern_atm env = function
+| AtmInt n -> (GTacAtm (AtmInt n), GTypRef (t_int, []))
+| AtmStr s -> (GTacAtm (AtmStr s), GTypRef (t_string, []))
+
+let invalid_pattern ~loc kn t =
+  let pt = match t with
+  | GCaseAlg kn' -> KerName.print kn
+  | GCaseTuple n -> str "tuple"
+  in
+  user_err ~loc (str "Invalid pattern, expected a pattern for type " ++
+    KerName.print kn ++ str ", found a pattern of type " ++ pt) (** FIXME *)
+
+type pattern_kind =
+| PKind_empty
+| PKind_variant of KerName.t
+| PKind_tuple of int
+| PKind_any
+
+let get_pattern_kind env pl = match pl with
+| [] -> PKind_empty
+| p :: pl ->
+  let rec get_kind p pl = match fst p with
+  | CPatAny _ ->
+    begin match pl with
+    | [] -> PKind_any
+    | p :: pl -> get_kind p pl
+    end
+  | CPatRef (_, qid, []) ->
+    begin match get_constructor env qid with
+    | ArgVar _ ->
+      begin match pl with
+      | [] -> PKind_any
+      | p :: pl -> get_kind p pl
+      end
+    | ArgArg (data, _) -> PKind_variant data.cdata_type
+    end
+  | CPatRef (_, qid, _ :: _) ->
+    begin match get_constructor env qid with
+    | ArgVar (loc, _) ->
+      user_err ~loc (str "Unbound constructor " ++ pr_qualid (snd qid))
+    | ArgArg (data, _) -> PKind_variant data.cdata_type
+    end
+  | CPatTup (_, tp) -> PKind_tuple (List.length tp)
+  in
+  get_kind p pl
+
+let rec intern_rec env = function
+| CTacAtm (_, atm) -> intern_atm env atm
+| CTacRef qid ->
+  begin match get_variable env qid with
+  | ArgVar (_, id) ->
+    let sch = Id.Map.find id env.env_var in
+    (GTacVar id, fresh_mix_type_scheme env sch)
+  | ArgArg kn ->
+    let (_, sch) = Tac2env.interp_global kn in
+    (GTacRef kn, fresh_type_scheme env sch)
+  end
+| CTacFun (loc, bnd, e) ->
+  let fold (env, bnd, tl) ((_, na), t) =
+    let t = match t with
+    | None -> GTypVar (fresh_id env)
+    | Some t -> intern_type env t
+    in
+    let env = push_name na (monomorphic t) env in
+    (env, na :: bnd, t :: tl)
+  in
+  let (env, bnd, tl) = List.fold_left fold (env, [], []) bnd in
+  let (e, t) = intern_rec env e in
+  let t = List.fold_left (fun accu t -> GTypArrow (t, accu)) t tl in
+  (GTacFun (bnd, e), t)
+| CTacApp (loc, f, args) ->
+  let (f, ft) = intern_rec env f in
+  let fold arg (args, t) =
+    let (arg, argt) = intern_rec env arg in
+    (arg :: args, GTypArrow (argt, t))
+  in
+  let ret = GTypVar (fresh_id env) in
+  let (args, t) = List.fold_right fold args ([], ret) in
+  let () = unify loc env ft t in
+  (GTacApp (f, args), ret)
+| CTacLet (loc, false, el, e) ->
+  let fold accu ((loc, na), _, _) = match na with
+  | Anonymous -> accu
+  | Name id ->
+    if Id.Set.mem id accu then
+      user_err ~loc (str "Variable " ++ Id.print id ++ str " is bound several \
+        times in this matching")
+    else Id.Set.add id accu
+  in
+  let _ = List.fold_left fold Id.Set.empty el in
+  let fold ((loc, na), tc, e) (el, p) =
+    let (e, t) = intern_rec env e in
+    let () = match tc with
+    | None -> ()
+    | Some tc ->
+      let tc = intern_type env tc in
+      unify loc env t tc
+    in
+    let t = if is_value e then abstract_var env t else monomorphic t in
+    ((na, e) :: el), ((na, t) :: p)
+  in
+  let (el, p) = List.fold_right fold el ([], []) in
+  let nenv = List.fold_left (fun accu (na, t) -> push_name na t env) env p in
+  let (e, t) = intern_rec nenv e in
+  (GTacLet (false, el, e), t)
+| CTacLet (loc, true, el, e) ->
+  intern_let_rec env loc el e
+| CTacTup (loc, []) ->
+  (GTacTup [], GTypRef (t_unit, []))
+| CTacTup (loc, el) ->
+  let fold e (el, tl) =
+    let (e, t) = intern_rec env e in
+    (e :: el, t :: tl)
+  in
+  let (el, tl) = List.fold_right fold el ([], []) in
+  (GTacTup el, GTypTuple tl)
+| CTacArr (loc, []) ->
+  let id = fresh_id env in
+  (GTacArr [], GTypRef (t_int, [GTypVar id]))
+| CTacArr (loc, e0 :: el) ->
+  let (e0, t0) = intern_rec env e0 in
+  let fold e el =
+    let loc = loc_of_tacexpr e in
+    let (e, t) = intern_rec env e in
+    let () = unify loc env t t0 in
+    e :: el
+  in
+  let el = e0 :: List.fold_right fold el [] in
+  (GTacArr el, GTypRef (t_array, [t0]))
+| CTacLst (loc, []) ->
+  let id = fresh_id env in
+  (c_nil, GTypRef (t_list, [GTypVar id]))
+| CTacLst (loc, e0 :: el) ->
+  let (e0, t0) = intern_rec env e0 in
+  let fold e el =
+    let loc = loc_of_tacexpr e in
+    let (e, t) = intern_rec env e in
+    let () = unify loc env t t0 in
+    c_cons e el
+  in
+  let el = c_cons e0 (List.fold_right fold el c_nil) in
+  (el, GTypRef (t_list, [t0]))
+| CTacCnv (loc, e, tc) ->
+  let (e, t) = intern_rec env e in
+  let tc = intern_type env tc in
+  let () = unify loc env t tc in
+  (e, tc)
+| CTacSeq (loc, e1, e2) ->
+  let (e1, t1) = intern_rec env e1 in
+  let (e2, t2) = intern_rec env e2 in
+  let () = check_elt_unit loc env t1 in
+  (GTacLet (false, [Anonymous, e1], e2), t2)
+| CTacCse (loc, e, pl) ->
+  intern_case env loc e pl
+
+and intern_let_rec env loc el e =
+  let fold accu ((loc, na), _, _) = match na with
+  | Anonymous -> accu
+  | Name id ->
+    if Id.Set.mem id accu then
+      user_err ~loc (str "Variable " ++ Id.print id ++ str " is bound several \
+        times in this matching")
+    else Id.Set.add id accu
+  in
+  let _ = List.fold_left fold Id.Set.empty el in
+  let map env ((loc, na), t, e) =
+    let id = fresh_id env in
+    let env = push_name na (monomorphic (GTypVar id)) env in
+    (env, (loc, na, t, e, id))
+  in
+  let (env, el) = List.fold_map map env el in
+  let fold (loc, na, tc, e, id) (el, tl) =
+    let loc_e = loc_of_tacexpr e in
+    let (e, t) = intern_rec env e in
+    let () =
+      if not (is_rec_rhs e) then
+        user_err ~loc:loc_e (str "This kind of expression is not allowed as \
+          right-hand side of a recursive binding")
+    in
+    let () = unify loc env t (GTypVar id) in
+    let () = match tc with
+    | None -> ()
+    | Some tc ->
+      let tc = intern_type env tc in
+      unify loc env t tc
+    in
+    ((na, e) :: el, t :: tl)
+  in
+  let (el, tl) = List.fold_right fold el ([], []) in
+  let (e, t) = intern_rec env e in
+  (GTacLet (true, el, e), t)
+
+(** For now, patterns recognized by the pattern-matching compiling are limited
+    to depth-one where leaves are either variables or catch-all *)
+and intern_case env loc e pl =
+  let (e', t) = intern_rec env e in
+  let todo ~loc () = user_err ~loc (str "Pattern not handled yet") in
+  match get_pattern_kind env pl with
+  | PKind_any ->
+    let (pat, b) = List.hd pl in
+    let na = match pat with
+    | CPatAny _ -> Anonymous
+    | CPatRef (_, (_, qid), _) -> Name (snd (repr_qualid qid))
+    | _ -> assert false
+    in
+    let () = check_redundant_clause (List.tl pl) in
+    let env = push_name na (monomorphic t) env in
+    let (b, tb) = intern_rec env b in
+    (GTacLet (false, [na, e'], b), tb)
+  | PKind_empty ->
+    let kn = check_elt_empty loc env t in
+    let r = fresh_id env in
+    (GTacCse (e', GCaseAlg kn, [||], [||]), GTypVar r)
+  | PKind_tuple len ->
+    begin match pl with
+    | [] -> assert false
+    | [CPatTup (_, []), b] ->
+      let () = unify (loc_of_tacexpr e) env t (GTypRef (t_unit, [])) in
+      let (b, tb) = intern_rec env b in
+      (GTacCse (e', GCaseAlg t_unit, [|b|], [||]), tb)
+    | [CPatTup (_, pl), b] ->
+      let map = function
+      | CPatAny _ -> Anonymous
+      | CPatRef (loc, qid, []) ->
+        begin match get_constructor env qid with
+        | ArgVar (_, id) -> Name id
+        | ArgArg _ -> todo ~loc ()
+        end
+      | p -> todo ~loc:(loc_of_patexpr p) ()
+      in
+      let ids = Array.map_of_list map pl in
+      let tc = GTypTuple (List.map (fun _ -> GTypVar (fresh_id env)) pl) in
+      let () = unify (loc_of_tacexpr e) env t tc in
+      let (b, tb) = intern_rec env b in
+      (GTacCse (e', GCaseTuple len, [||], [|ids, b|]), tb)
+    | (p, _) :: _ -> todo ~loc:(loc_of_patexpr p) ()
+    end
+  | PKind_variant kn ->
+    let subst, tc = fresh_reftype env kn in
+    let () = unify (loc_of_tacexpr e) env t tc in
+    let (params, def) = Tac2env.interp_type kn in
+    let cstrs = match def with
+    | GTydAlg c -> c
+    | _ -> assert false
+    in
+    let count (const, nonconst) (c, args) = match args with
+    | [] -> (succ const, nonconst)
+    | _ :: _ -> (const, succ nonconst)
+    in
+    let nconst, nnonconst = List.fold_left count (0, 0) cstrs in
+    let const = Array.make nconst None in
+    let nonconst = Array.make nnonconst None in
+    let ret = GTypVar (fresh_id env) in
+    let rec intern_branch = function
+    | [] -> ()
+    | (pat, br) :: rem ->
+      let tbr = match pat with
+      | CPatAny _ ->
+        let () = check_redundant_clause rem in
+        let (br', brT) = intern_rec env br in
+        (** Fill all remaining branches *)
+        let fill (ncst, narg) (_, args) =
+          if List.is_empty args then
+            let () =
+              if Option.is_empty const.(ncst) then const.(ncst) <- Some br'
+            in
+            (succ ncst, narg)
+          else
+            let () =
+              if Option.is_empty const.(narg) then
+                let ids = Array.map_of_list (fun _ -> Anonymous) args in
+                nonconst.(narg) <- Some (ids, br')
+            in
+            (ncst, succ narg)
+        in
+        let _ = List.fold_left fill (0, 0) cstrs in
+        brT
+      | CPatRef (loc, qid, args) ->
+        let data = match get_constructor env qid with
+        | ArgVar _ -> todo ~loc ()
+        | ArgArg (data, _) ->
+          let () =
+            let kn' = data.cdata_type in
+            if not (KerName.equal kn kn') then
+              invalid_pattern ~loc kn (GCaseAlg kn')
+          in
+          data
+        in
+        let get_id = function
+        | CPatAny _ -> Anonymous
+        | CPatRef (loc, qid, []) ->
+          begin match get_constructor env qid with
+          | ArgVar (_, id) -> Name id
+          | ArgArg _ -> todo ~loc ()
+          end
+        | p -> todo ~loc:(loc_of_patexpr p) ()
+        in
+        let ids = List.map get_id args in
+        let nids = List.length ids in
+        let nargs = List.length (snd data.cdata_args) in
+        let () =
+          if not (Int.equal nids nargs) then
+            user_err ~loc (str "Constructor expects " ++ int nargs ++
+              str " arguments, but is applied to " ++ int nids ++
+              str " arguments")
+        in
+        let fold env id tpe =
+          (** Instantiate all arguments *)
+          let subst n = GTypVar subst.(n) in
+          let tpe = subst_type subst tpe in
+          push_name id (monomorphic tpe) env
+        in
+        let nenv = List.fold_left2 fold env ids (snd data.cdata_args) in
+        let (br', brT) = intern_rec nenv br in
+        let () =
+          let index = data.cdata_indx in
+          if List.is_empty args then
+            if Option.is_empty const.(index) then const.(index) <- Some br'
+            else warn_redundant_clause ~loc ()
+          else
+            let ids = Array.of_list ids in
+            if Option.is_empty nonconst.(index) then nonconst.(index) <- Some (ids, br')
+            else warn_redundant_clause ~loc ()
+        in
+        brT
+      | CPatTup (loc, tup) ->
+        invalid_pattern ~loc kn (GCaseTuple (List.length tup))
+      in
+      let () = unify (loc_of_tacexpr br) env ret tbr in
+      intern_branch rem
+    in
+    let () = intern_branch pl in
+    let map = function
+    | None -> user_err ~loc (str "Unhandled match case") (** FIXME *)
+    | Some x -> x
+    in
+    let const = Array.map map const in
+    let nonconst = Array.map map nonconst in
+    let ce = GTacCse (e', GCaseAlg kn, const, nonconst) in
+    (ce, ret)
+
+let normalize env (count, vars) (t : UF.elt glb_typexpr) =
+  let get_var id =
+    try UF.Map.find id !vars
+    with Not_found ->
+      let () = assert env.env_opn in
+      let n = GTypVar !count in
+      let () = incr count in
+      let () = vars := UF.Map.add id n !vars in
+      n
+  in
+  let rec subst id = match UF.find id env.env_cst with
+  | id, None -> get_var id
+  | _, Some t -> subst_type subst t
+  in
+  subst_type subst t
+
+let intern e =
+  let env = empty_env () in
+  let (e, t) = intern_rec env e in
+  let count = ref 0 in
+  let vars = ref UF.Map.empty in
+  let t = normalize env (count, vars) t in
+  (e, (!count, t))
+
+let intern_typedef self (ids, t) : glb_quant_typedef =
+  let env = { (empty_env ()) with env_rec = self } in
+  (** Initialize type parameters *)
+  let map id = get_alias id env in
+  let ids = List.map map ids in
+  let count = ref (List.length ids) in
+  let vars = ref UF.Map.empty in
+  let iter n id = vars := UF.Map.add id (GTypVar n) !vars in
+  let () = List.iteri iter ids in
+  (** Do not accept unbound type variables *)
+  let env = { env with env_opn = false } in
+  let intern t =
+    let t = intern_type env t in
+    normalize env (count, vars) t
+  in
+  let count = !count in
+  match t with
+  | CTydDef None -> (count, GTydDef None)
+  | CTydDef (Some t) -> (count, GTydDef (Some (intern t)))
+  | CTydAlg constrs ->
+    let map (c, t) = (c, List.map intern t) in
+    let constrs = List.map map constrs in
+    (count, GTydAlg constrs)
+  | CTydRec fields ->
+    let map (c, mut, t) = (c, mut, intern t) in
+    let fields = List.map map fields in
+    (count, GTydRec fields)
+
+let intern_open_type t =
+  let env = empty_env () in
+  let t = intern_type env t in
+  let count = ref 0 in
+  let vars = ref UF.Map.empty in
+  let t = normalize env (count, vars) t in
+  (!count, t)
+
+(** Kernel substitution *)
+
+open Mod_subst
+
+let rec subst_type subst t = match t with
+| GTypVar _ -> t
+| GTypArrow (t1, t2) ->
+  let t1' = subst_type subst t1 in
+  let t2' = subst_type subst t2 in
+  if t1' == t1 && t2' == t2 then t
+  else GTypArrow (t1', t2')
+| GTypTuple tl ->
+  let tl'= List.smartmap (fun t -> subst_type subst t) tl in
+  if tl' == tl then t else GTypTuple tl'
+| GTypRef (kn, tl) ->
+  let kn' = subst_kn subst kn in
+  let tl' = List.smartmap (fun t -> subst_type subst t) tl in
+  if kn' == kn && tl' == tl then t else GTypRef (kn', tl')
+
+let subst_case_info subst ci = match ci with
+| GCaseAlg kn ->
+  let kn' = subst_kn subst kn in
+  if kn' == kn then ci else GCaseAlg kn'
+| GCaseTuple _ -> ci
+
+let rec subst_expr subst e = match e with
+| GTacAtm _ | GTacVar _ | GTacPrm _ -> e
+| GTacRef kn -> GTacRef (subst_kn subst kn)
+| GTacFun (ids, e) -> GTacFun (ids, subst_expr subst e)
+| GTacApp (f, args) ->
+  GTacApp (subst_expr subst f, List.map (fun e -> subst_expr subst e) args)
+| GTacLet (r, bs, e) ->
+  let bs = List.map (fun (na, e) -> (na, subst_expr subst e)) bs in
+  GTacLet (r, bs, subst_expr subst e)
+| GTacTup el ->
+  GTacTup (List.map (fun e -> subst_expr subst e) el)
+| GTacArr el ->
+  GTacArr (List.map (fun e -> subst_expr subst e) el)
+| GTacCst (kn, n, el) -> 
+  GTacCst (subst_kn subst kn, n, List.map (fun e -> subst_expr subst e) el)
+| GTacCse (e, ci, cse0, cse1) ->
+  let cse0' = Array.map (fun e -> subst_expr subst e) cse0 in
+  let cse1' = Array.map (fun (ids, e) -> (ids, subst_expr subst e)) cse1 in
+  let ci' = subst_case_info subst ci in
+  GTacCse (subst_expr subst e, ci', cse0', cse1')
+
+let subst_typedef subst e = match e with
+| GTydDef t ->
+  let t' = Option.smartmap (fun t -> subst_type subst t) t in
+  if t' == t then e else GTydDef t'
+| GTydAlg constrs ->
+  let map (c, tl as p) =
+    let tl' = List.smartmap (fun t -> subst_type subst t) tl in
+    if tl' == tl then p else (c, tl')
+  in
+  let constrs' = List.smartmap map constrs in
+  if constrs' == constrs then e else GTydAlg constrs'
+| GTydRec fields ->
+  let map (c, mut, t as p) =
+    let t' = subst_type subst t in
+    if t' == t then p else (c, mut, t')
+  in
+  let fields' = List.smartmap map fields in
+  if fields' == fields then e else GTydRec fields'
+
+let subst_quant_typedef subst (prm, def as qdef) =
+  let def' = subst_typedef subst def in
+  if def' == def then qdef else (prm, def')
+
+let subst_type_scheme subst (prm, t as sch) =
+  let t' = subst_type subst t in
+  if t' == t then sch else (prm, t')
diff --git a/tac2intern.mli b/tac2intern.mli
new file mode 100644
index 0000000000..a6be01d647
--- /dev/null
+++ b/tac2intern.mli
@@ -0,0 +1,30 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Genarg
+open Names
+open Mod_subst
+open Tac2expr
+
+val loc_of_tacexpr : raw_tacexpr -> Loc.t
+
+val intern : raw_tacexpr -> glb_tacexpr * type_scheme
+val intern_typedef : (KerName.t * int) Id.Map.t -> raw_quant_typedef -> glb_quant_typedef
+val intern_open_type : raw_typexpr -> type_scheme
+
+(** Check that a term is a value. Only values are safe to marshall between
+    processes. *)
+val is_value : glb_tacexpr -> bool
+val check_unit : ?loc:Loc.t -> int glb_typexpr -> unit
+
+val subst_type : substitution -> 'a glb_typexpr -> 'a glb_typexpr
+val subst_expr : substitution -> glb_tacexpr -> glb_tacexpr
+val subst_quant_typedef : substitution -> glb_quant_typedef -> glb_quant_typedef
+val subst_type_scheme : substitution -> type_scheme -> type_scheme
+
+val pr_glbtype : 'a glb_typexpr -> Pp.std_ppcmds
diff --git a/tac2interp.ml b/tac2interp.ml
new file mode 100644
index 0000000000..221f107dc8
--- /dev/null
+++ b/tac2interp.ml
@@ -0,0 +1,108 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open CErrors
+open Genarg
+open Names
+open Proofview.Notations
+open Tac2expr
+
+exception LtacError of KerName.t * valexpr
+
+type environment = valexpr Id.Map.t
+
+let empty_environment = Id.Map.empty
+
+let push_name ist id v = match id with
+| Anonymous -> ist
+| Name id -> Id.Map.add id v ist
+
+let get_var ist id =
+  try Id.Map.find id ist with Not_found ->
+    anomaly (str "Unbound variable " ++ Id.print id)
+
+let get_ref ist kn =
+  try fst (Tac2env.interp_global kn) with Not_found ->
+    anomaly (str "Unbound reference" ++ KerName.print kn)
+
+let return = Proofview.tclUNIT
+
+let rec interp ist = function
+| GTacAtm (AtmInt n) -> return (ValInt n)
+| GTacAtm (AtmStr s) -> return (ValStr s)
+| GTacVar id -> return (get_var ist id)
+| GTacRef qid -> return (get_ref ist qid)
+| GTacFun (ids, e) ->
+  let cls = { clos_env = ist; clos_var = ids; clos_exp = e } in
+  return (ValCls cls)
+| GTacApp (f, args) ->
+  interp ist f >>= fun f ->
+  Proofview.Monad.List.map (fun e -> interp ist e) args >>= fun args ->
+  interp_app ist f args
+| GTacLet (false, el, e) ->
+  let fold accu (na, e) =
+    interp ist e >>= fun e ->
+    return (push_name accu na e)
+  in
+  Proofview.Monad.List.fold_left fold ist el >>= fun ist ->
+  interp ist e
+| GTacLet (true, el, e) ->
+  let map (na, e) = match e with
+  | GTacFun (ids, e) ->
+    let cls = { clos_env = ist; clos_var = ids; clos_exp = e } in
+    na, cls
+  | _ -> anomaly (str "Ill-formed recursive function")
+  in
+  let fixs = List.map map el in
+  let fold accu (na, cls) = match na with
+  | Anonymous -> accu
+  | Name id -> Id.Map.add id (ValCls cls) accu
+  in
+  let ist = List.fold_left fold ist fixs in
+  (** Hack to make a cycle imperatively in the environment *)
+  let iter (_, e) = e.clos_env <- ist in
+  let () = List.iter iter fixs in
+  interp ist e
+| GTacTup [] ->
+  return (ValInt 0)
+| GTacTup el | GTacArr el ->
+  Proofview.Monad.List.map (fun e -> interp ist e) el >>= fun el ->
+  return (ValBlk (0, Array.of_list el))
+| GTacCst (_, n, []) -> return (ValInt n)
+| GTacCst (_, n, el) ->
+  Proofview.Monad.List.map (fun e -> interp ist e) el >>= fun el ->
+  return (ValBlk (n, Array.of_list el))
+| GTacCse (e, _, cse0, cse1) ->
+  interp ist e >>= fun e -> interp_case ist e cse0 cse1
+| GTacPrm (ml, el) ->
+  Proofview.Monad.List.map (fun e -> interp ist e) el >>= fun el ->
+  Tac2env.interp_primitive ml el
+
+and interp_app ist f args = match f with
+| ValCls { clos_env = ist; clos_var = ids; clos_exp = e } ->
+  let rec push ist ids args = match ids, args with
+  | [], [] -> interp ist e
+  | [], _ :: _ -> interp ist e >>= fun f -> interp_app ist f args
+  | _ :: _, [] ->
+    let cls = { clos_env = ist; clos_var = ids; clos_exp = e } in
+    return (ValCls cls)
+  | id :: ids, arg :: args -> push (push_name ist id arg) ids args
+  in
+  push ist ids args
+| ValExt _ | ValInt _ | ValBlk _ | ValStr _ ->
+  anomaly (str "Unexpected value shape")
+
+and interp_case ist e cse0 cse1 = match e with
+| ValInt n -> interp ist cse0.(n)
+| ValBlk (n, args) ->
+  let (ids, e) = cse1.(n) in
+  let ist = CArray.fold_left2 push_name ist ids args in
+  interp ist e
+| ValExt _ | ValStr _ | ValCls _ ->
+  anomaly (str "Unexpected value shape")
diff --git a/tac2interp.mli b/tac2interp.mli
new file mode 100644
index 0000000000..b11ee36012
--- /dev/null
+++ b/tac2interp.mli
@@ -0,0 +1,19 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Genarg
+open Names
+open Tac2expr
+
+exception LtacError of KerName.t * valexpr
+
+type environment = valexpr Id.Map.t
+
+val empty_environment : environment
+
+val interp : environment -> glb_tacexpr -> valexpr Proofview.tactic
diff --git a/vo.itarget b/vo.itarget
new file mode 100644
index 0000000000..776404ad79
--- /dev/null
+++ b/vo.itarget
@@ -0,0 +1 @@
+Ltac2.vo