Turning the ltac2 subfolder into a standalone plugin.

15 files changed, 4259 insertions, 0 deletions

diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
new file mode 100644
index 0000000000..36057b3a67
--- /dev/null
+++ b/src/g_ltac2.ml4
@@ -0,0 +1,278 @@
+(************************************************************************)
+(*  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 Names
+open Pcoq
+open Constrexpr
+open Misctypes
+open Tac2expr
+open Ltac_plugin
+
+let tac2expr = Tac2entries.Pltac.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 tac2def_syn = Gram.entry_create "tactic:tac2def_syn"
+let tac2mode = Gram.entry_create "vernac:ltac2_command"
+
+let inj_wit wit loc x = CTacExt (loc, Genarg.in_gen (Genarg.rawwit wit) x)
+let inj_constr loc c = inj_wit Stdarg.wit_constr loc c
+let inj_open_constr loc c = inj_wit Stdarg.wit_open_constr loc c
+let inj_ident loc c = inj_wit Stdarg.wit_ident loc c
+
+GEXTEND Gram
+  GLOBAL: tac2expr tac2type tac2def_val tac2def_typ tac2def_ext tac2def_syn;
+  tac2pat:
+    [ "1" LEFTA
+      [ id = Prim.qualid; pl = LIST1 tac2pat LEVEL "0" -> CPatRef (!@loc, RelId id, pl)
+      | id = Prim.qualid -> CPatRef (!@loc, RelId id, []) ]
+    | "0"
+      [ "_" -> CPatAny (!@loc)
+      | "()" -> CPatTup (Loc.tag ~loc:!@loc [])
+      | id = Prim.qualid -> CPatRef (!@loc, RelId id, [])
+      | "("; pl = LIST0 tac2pat LEVEL "1" SEP ","; ")" -> CPatTup (Loc.tag ~loc:!@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)
+      | e = SELF; ".("; qid = Prim.qualid; ")" -> CTacPrj (!@loc, e, RelId qid)
+      | e = SELF; ".("; qid = Prim.qualid; ")"; ":="; r = tac2expr LEVEL "1" -> CTacSet (!@loc, e, RelId qid, r)
+      | e0 = tac2expr; ","; el = LIST1 tac2expr LEVEL "1" SEP "," -> CTacTup (Loc.tag ~loc:!@loc (e0 :: el)) ]
+    | "0"
+      [ "("; a = tac2expr LEVEL "5"; ")" -> a
+      | "("; a = tac2expr; ":"; t = tac2type; ")" -> CTacCnv (!@loc, a, t)
+      | "()" -> CTacTup (Loc.tag ~loc:!@loc [])
+      | "("; ")" -> CTacTup (Loc.tag ~loc:!@loc [])
+      | "["; a = LIST0 tac2expr LEVEL "1" SEP ";"; "]" -> CTacLst (Loc.tag ~loc:!@loc a)
+      | "{"; a = tac2rec_fieldexprs; "}" -> CTacRec (!@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.tag ~loc:!@loc (AtmInt n))
+      | s = Prim.string -> CTacAtm (Loc.tag ~loc:!@loc (AtmStr s))
+      | id = Prim.qualid -> CTacRef (RelId id)
+      | IDENT "constr"; ":"; "("; c = Constr.lconstr; ")" -> inj_constr !@loc c
+      | IDENT "open_constr"; ":"; "("; c = Constr.lconstr; ")" -> inj_open_constr !@loc c
+      | IDENT "ident"; ":"; "("; c = Prim.ident; ")" -> inj_ident !@loc c
+    ] ]
+  ;
+  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" LEFTA
+      [ t = SELF; qid = Prim.qualid -> CTypRef (!@loc, RelId qid, [t]) ]
+    | "0"
+      [ "("; t = tac2type LEVEL "5"; ")"  -> t
+      | id = typ_param -> CTypVar (Loc.tag ~loc:!@loc (Name id))
+      | "_" -> CTypVar (Loc.tag ~loc:!@loc Anonymous)
+      | qid = Prim.qualid -> CTypRef (!@loc, RelId qid, [])
+      | "("; p = LIST1 tac2type LEVEL "5" SEP ","; ")"; qid = Prim.qualid ->
+        CTypRef (!@loc, RelId qid, p) ]
+    ];
+  locident:
+    [ [ id = Prim.ident -> Loc.tag ~loc:!@loc id ] ]
+  ;
+  binder:
+    [ [ "_" -> Loc.tag ~loc:!@loc Anonymous
+      | l = Prim.ident -> Loc.tag ~loc:!@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)
+      | "["; ".."; "]" -> CTydOpn
+      | "["; t = tac2alg_constructors; "]" -> CTydAlg t
+      | "{"; t = tac2rec_fields; "}"-> CTydRec t ] ]
+  ;
+  tac2alg_constructors:
+    [ [ "|"; cs = LIST1 tac2alg_constructor SEP "|" -> cs
+      | cs = LIST0 tac2alg_constructor SEP "|" -> cs ] ]
+  ;
+  tac2alg_constructor:
+    [ [ c = Prim.ident -> (c, [])
+      | c = Prim.ident; "("; args = LIST0 tac2type SEP ","; ")"-> (c, args) ] ]
+  ;
+  tac2rec_fields:
+    [ [ f = tac2rec_field; ";"; l = tac2rec_fields -> f :: l
+      | f = tac2rec_field; ";" -> [f]
+      | f = tac2rec_field -> [f]
+      | -> [] ] ]
+  ;
+  tac2rec_field:
+    [ [ mut = [ -> false | IDENT "mutable" -> true]; id = Prim.ident; ":"; t = tac2type -> (id, mut, t) ] ]
+  ;
+  tac2rec_fieldexprs:
+    [ [ f = tac2rec_fieldexpr; ";"; l = tac2rec_fieldexprs -> f :: l
+      | f = tac2rec_fieldexpr; ";" -> [f]
+      | f = tac2rec_fieldexpr-> [f]
+      | -> [] ] ]
+  ;
+  tac2rec_fieldexpr:
+    [ [ qid = Prim.qualid; ":="; e = tac2expr LEVEL "1" -> RelId qid, e ] ]
+  ;
+  tac2typ_prm:
+    [ [ -> []
+      | id = typ_param -> [Loc.tag ~loc:!@loc id]
+      | "("; ids = LIST1 [ id = typ_param -> Loc.tag ~loc:!@loc id ] SEP "," ;")" -> ids
+    ] ]
+  ;
+  tac2typ_def:
+    [ [ prm = tac2typ_prm; id = Prim.qualid; (r, e) = tac2type_body -> (id, r, (prm, e)) ] ]
+  ;
+  tac2type_body:
+    [ [ -> false, CTydDef None
+      | ":="; e = tac2typ_knd -> false, e
+      | "::="; e = tac2typ_knd -> true, e
+    ] ]
+  ;
+  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)
+    ] ]
+  ;
+  syn_node:
+    [ [ "_" -> Loc.tag ~loc:!@loc None
+      | id = Prim.ident -> Loc.tag ~loc:!@loc (Some id)
+    ] ]
+  ;
+  sexpr:
+    [ [ s = Prim.string -> SexprStr (Loc.tag ~loc:!@loc s)
+      | n = Prim.integer -> SexprInt (Loc.tag ~loc:!@loc n)
+      | id = syn_node -> SexprRec (!@loc, id, [])
+      | id = syn_node; "("; tok = LIST1 sexpr SEP "," ; ")" ->
+        SexprRec (!@loc, id, tok)
+    ] ]
+  ;
+  syn_level:
+    [ [ -> None
+      | ":"; n = Prim.integer -> Some n
+    ] ]
+  ;
+  tac2def_syn:
+    [ [ "Notation"; toks = LIST1 sexpr; n = syn_level; ":=";
+        e = tac2expr ->
+        StrSyn (toks, n, e)
+    ] ]
+  ;
+END
+
+GEXTEND Gram
+  Pcoq.Constr.operconstr: LEVEL "0"
+    [ [ IDENT "ltac2"; ":"; "("; tac = tac2expr; ")" ->
+          let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2) tac in
+          CAst.make ~loc:!@loc (CHole (None, IntroAnonymous, Some arg)) ] ]
+  ;
+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 ]
+| [ tac2def_syn(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/src/ltac2_plugin.mlpack b/src/ltac2_plugin.mlpack
new file mode 100644
index 0000000000..3d87a8cddb
--- /dev/null
+++ b/src/ltac2_plugin.mlpack
@@ -0,0 +1,7 @@
+Tac2env
+Tac2print
+Tac2intern
+Tac2interp
+Tac2entries
+Tac2core
+G_ltac2
diff --git a/src/tac2core.ml b/src/tac2core.ml
new file mode 100644
index 0000000000..91a3bfa168
--- /dev/null
+++ b/src/tac2core.ml
@@ -0,0 +1,648 @@
+(************************************************************************)
+(*  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 Genarg
+open Geninterp
+open Tac2env
+open Tac2expr
+open Tac2interp
+open Proofview.Notations
+
+(** Standard values *)
+
+let coq_core n = KerName.make2 Tac2env.coq_prefix (Label.of_id (Id.of_string_soft n))
+
+let val_tag t = match val_tag t with
+| Val.Base t -> t
+| _ -> assert false
+
+let val_constr = val_tag (topwit Stdarg.wit_constr)
+let val_ident = val_tag (topwit Stdarg.wit_ident)
+let val_pp = Val.create "ltac2:pp"
+
+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
+
+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 t_constr = coq_core "constr"
+let t_ident = coq_core "ident"
+let t_option = coq_core "option"
+
+let c_nil = coq_core "[]"
+let c_cons = coq_core "::"
+
+let c_none = coq_core "None"
+let c_some = coq_core "Some"
+
+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 of_int n = ValInt n
+let to_int = function
+| ValInt n -> n
+| _ -> assert false
+
+let of_bool b = if b then ValInt 0 else ValInt 1
+
+let to_bool = function
+| ValInt 0 -> true
+| ValInt 1 -> false
+| _ -> assert false
+
+let of_char n = ValInt (Char.code n)
+let to_char = function
+| ValInt n -> Char.chr n
+| _ -> assert false
+
+let of_string s = ValStr s
+let to_string = function
+| ValStr s -> s
+| _ -> 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
+
+let of_ext tag c =
+  ValExt (Val.Dyn (tag, c))
+
+let to_ext tag = function
+| ValExt e -> extract_val tag e
+| _ -> assert false
+
+let of_constr c = of_ext val_constr c
+let to_constr c = to_ext val_constr c
+
+let of_ident c = of_ext val_ident c
+let to_ident c = to_ext val_ident c
+
+(** FIXME: handle backtrace in Ltac2 exceptions *)
+let of_exn c = match fst c with
+| LtacError (kn, c) -> ValOpn (kn, c)
+| _ -> of_ext val_exn c
+
+let to_exn c = match c with
+| ValOpn (kn, c) -> (LtacError (kn, c), Exninfo.null)
+| _ -> to_ext val_exn c
+
+let of_pp c = of_ext val_pp c
+let to_pp c = to_ext val_pp c
+
+end
+
+let val_valexpr = Val.create "ltac2:valexpr"
+
+(** Stdlib exceptions *)
+
+let err_notfocussed =
+  LtacError (coq_core "Not_focussed", [||])
+
+let err_outofbounds =
+  LtacError (coq_core "Out_of_bounds", [||])
+
+let err_notfound =
+  LtacError (coq_core "Not_found", [||])
+
+(** Helper functions *)
+
+let thaw f = interp_app f [v_unit]
+let throw e = Proofview.tclLIFT (Proofview.NonLogical.raise e)
+
+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
+
+let pf_apply f =
+  Proofview.Goal.goals >>= function
+  | [] ->
+    Proofview.tclENV >>= fun env ->
+    Proofview.tclEVARMAP >>= fun sigma ->
+    f env sigma
+  | [gl] ->
+    gl >>= fun gl ->
+    f (Proofview.Goal.env gl) (Tacmach.New.project gl)
+  | _ :: _ :: _ ->
+    throw err_notfocussed
+
+(** Primitives *)
+
+(** Printing *)
+
+let prm_print : ml_tactic = function
+| [pp] -> wrap_unit (fun () -> Feedback.msg_notice (Value.to_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 (Bytes.to_string s))))
+| _ -> assert false
+
+let prm_message_of_constr : ml_tactic = function
+| [c] ->
+  pf_apply begin fun env sigma ->
+    let c = Value.to_constr c in
+    let pp = Printer.pr_econstr_env env sigma c in
+    return (ValExt (Val.Dyn (val_pp, pp)))
+  end
+| _ -> assert false
+
+let prm_message_concat : ml_tactic = function
+| [m1; m2] ->
+  let m1 = Value.to_pp m1 in
+  let m2 = Value.to_pp m2 in
+  return (Value.of_pp (Pp.app m1 m2))
+| _ -> assert false
+
+(** Array *)
+
+let prm_array_make : ml_tactic = function
+| [ValInt n; x] ->
+  if n < 0 || n > Sys.max_array_length then throw err_outofbounds
+  else 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] ->
+  if n < 0 || n >= Array.length v then throw err_outofbounds
+  else wrap_unit (fun () -> v.(n) <- x)
+| _ -> assert false
+
+let prm_array_get : ml_tactic = function
+| [ValBlk (_, v); ValInt n] ->
+  if n < 0 || n >= Array.length v then throw err_outofbounds
+  else wrap (fun () -> v.(n))
+| _ -> assert false
+
+(** Int *)
+
+let prm_int_equal : ml_tactic = function
+| [m; n] ->
+  return (Value.of_bool (Value.to_int m == Value.to_int n))
+| _ -> assert false
+
+let binop f : ml_tactic = function
+| [m; n] -> return (Value.of_int (f (Value.to_int m) (Value.to_int n)))
+| _ -> assert false
+
+let prm_int_compare args = binop Int.compare args
+let prm_int_add args = binop (+) args
+let prm_int_sub args = binop (-) args
+let prm_int_mul args = binop ( * ) args
+
+let prm_int_neg : ml_tactic = function
+| [m] -> return (Value.of_int (~- (Value.to_int m)))
+| _ -> assert false
+
+(** String *)
+
+let prm_string_make : ml_tactic = function
+| [n; c] ->
+  let n = Value.to_int n in
+  let c = Value.to_char c in
+  if n < 0 || n > Sys.max_string_length then throw err_outofbounds
+  else wrap (fun () -> Value.of_string (Bytes.make n c))
+| _ -> assert false
+
+let prm_string_length : ml_tactic = function
+| [s] ->
+  return (Value.of_int (Bytes.length (Value.to_string s)))
+| _ -> assert false
+
+let prm_string_set : ml_tactic = function
+| [s; n; c] ->
+  let s = Value.to_string s in
+  let n = Value.to_int n in
+  let c = Value.to_char c in
+  if n < 0 || n >= Bytes.length s then throw err_outofbounds
+  else wrap_unit (fun () -> Bytes.set s n c)
+| _ -> assert false
+
+let prm_string_get : ml_tactic = function
+| [s; n] ->
+  let s = Value.to_string s in
+  let n = Value.to_int n in
+  if n < 0 || n >= Bytes.length s then throw err_outofbounds
+  else wrap (fun () -> Value.of_char (Bytes.get s n))
+| _ -> assert false
+
+(** Terms *)
+
+(** constr -> constr *)
+let prm_constr_type : ml_tactic = function
+| [c] ->
+  let c = Value.to_constr c in
+  let get_type env sigma =
+  Proofview.V82.wrap_exceptions begin fun () ->
+    let (sigma, t) = Typing.type_of env sigma c in
+    let t = Value.of_constr t in
+    Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT t
+  end in
+  pf_apply get_type
+| _ -> assert false
+
+(** constr -> constr *)
+let prm_constr_equal : ml_tactic = function
+| [c1; c2] ->
+  let c1 = Value.to_constr c1 in
+  let c2 = Value.to_constr c2 in
+  Proofview.tclEVARMAP >>= fun sigma ->
+  let b = EConstr.eq_constr sigma c1 c2 in
+  Proofview.tclUNIT (Value.of_bool b)
+| _ -> assert false
+
+(** Error *)
+
+let prm_throw : ml_tactic = function
+| [e] ->
+  let (e, info) = Value.to_exn e in
+  Proofview.tclLIFT (Proofview.NonLogical.raise ~info e)
+| _ -> assert false
+
+(** Control *)
+
+(** exn -> 'a *)
+let prm_zero : ml_tactic = function
+| [e] ->
+  let (e, info) = Value.to_exn e in
+  Proofview.tclZERO ~info e
+| _ -> assert false
+
+(** exn -> 'a *)
+let prm_plus : ml_tactic = function
+| [x; k] ->
+  Proofview.tclOR (thaw x) (fun e -> interp_app k [Value.of_exn e])
+| _ -> assert false
+
+(** (unit -> 'a) -> 'a *)
+let prm_once : ml_tactic = function
+| [f] -> Proofview.tclONCE (thaw f)
+| _ -> assert false
+
+(** (unit -> unit) list -> unit *)
+let prm_dispatch : ml_tactic = function
+| [l] ->
+  let l = Value.to_list l in
+  let l = List.map (fun f -> Proofview.tclIGNORE (thaw f)) l in
+  Proofview.tclDISPATCH l >>= fun () -> return v_unit
+| _ -> assert false
+
+(** (unit -> unit) list -> (unit -> unit) -> (unit -> unit) list -> unit *)
+let prm_extend : ml_tactic = function
+| [lft; tac; rgt] ->
+  let lft = Value.to_list lft in
+  let lft = List.map (fun f -> Proofview.tclIGNORE (thaw f)) lft in
+  let tac = Proofview.tclIGNORE (thaw tac) in
+  let rgt = Value.to_list rgt in
+  let rgt = List.map (fun f -> Proofview.tclIGNORE (thaw f)) rgt in
+  Proofview.tclEXTEND lft tac rgt >>= fun () -> return v_unit
+| _ -> assert false
+
+(** (unit -> unit) -> unit *)
+let prm_enter : ml_tactic = function
+| [f] ->
+  let f = Proofview.tclIGNORE (thaw f) in
+  Proofview.tclINDEPENDENT f >>= fun () -> return v_unit
+| _ -> assert false
+
+(** int -> int -> (unit -> 'a) -> 'a *)
+let prm_focus : ml_tactic = function
+| [i; j; tac] ->
+  let i = Value.to_int i in
+  let j = Value.to_int j in
+  Proofview.tclFOCUS i j (thaw tac)
+| _ -> assert false
+
+(** unit -> unit *)
+let prm_shelve : ml_tactic = function
+| [_] -> Proofview.shelve >>= fun () -> return v_unit
+| _ -> assert false
+
+(** unit -> unit *)
+let prm_shelve_unifiable : ml_tactic = function
+| [_] -> Proofview.shelve_unifiable >>= fun () -> return v_unit
+| _ -> assert false
+
+let prm_new_goal : ml_tactic = function
+| [ev] ->
+  let ev = Evar.unsafe_of_int (Value.to_int ev) in
+  Proofview.tclEVARMAP >>= fun sigma ->
+  if Evd.mem sigma ev then
+    Proofview.Unsafe.tclNEWGOALS [ev] <*> Proofview.tclUNIT v_unit
+  else throw err_notfound
+| _ -> assert false
+
+(** unit -> constr *)
+let prm_goal : ml_tactic = function
+| [_] ->
+  Proofview.Goal.enter_one begin fun gl ->
+    let concl = Tacmach.New.pf_nf_concl gl in
+    return (Value.of_constr concl)
+  end
+| _ -> assert false
+
+(** ident -> constr *)
+let prm_hyp : ml_tactic = function
+| [id] ->
+  let id = Value.to_ident id in
+  pf_apply begin fun env _ ->
+    let mem = try ignore (Environ.lookup_named id env); true with Not_found -> false in
+    if mem then return (Value.of_constr (EConstr.mkVar id))
+    else Tacticals.New.tclZEROMSG
+      (str "Hypothesis " ++ quote (Id.print id) ++ str " not found") (** FIXME: Do something more sensible *)
+  end
+| _ -> assert false
+
+(** (unit -> constr) -> unit *)
+let prm_refine : ml_tactic = function
+| [c] ->
+  let c = thaw c >>= fun c -> Proofview.tclUNIT ((), Value.to_constr c) in
+  Proofview.Goal.nf_enter begin fun gl ->
+    Refine.generic_refine ~typecheck:true c gl
+  end >>= fun () -> return v_unit
+| _ -> 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 "message_of_constr") prm_message_of_constr
+let () = Tac2env.define_primitive (pname "message_concat") prm_message_concat
+
+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
+
+let () = Tac2env.define_primitive (pname "string_make") prm_string_make
+let () = Tac2env.define_primitive (pname "string_length") prm_string_length
+let () = Tac2env.define_primitive (pname "string_get") prm_string_get
+let () = Tac2env.define_primitive (pname "string_set") prm_string_set
+
+let () = Tac2env.define_primitive (pname "constr_type") prm_constr_type
+let () = Tac2env.define_primitive (pname "constr_equal") prm_constr_equal
+
+let () = Tac2env.define_primitive (pname "int_equal") prm_int_equal
+let () = Tac2env.define_primitive (pname "int_compare") prm_int_compare
+let () = Tac2env.define_primitive (pname "int_neg") prm_int_neg
+let () = Tac2env.define_primitive (pname "int_add") prm_int_add
+let () = Tac2env.define_primitive (pname "int_sub") prm_int_sub
+let () = Tac2env.define_primitive (pname "int_mul") prm_int_mul
+
+let () = Tac2env.define_primitive (pname "throw") prm_throw
+
+let () = Tac2env.define_primitive (pname "zero") prm_zero
+let () = Tac2env.define_primitive (pname "plus") prm_plus
+let () = Tac2env.define_primitive (pname "once") prm_once
+let () = Tac2env.define_primitive (pname "dispatch") prm_dispatch
+let () = Tac2env.define_primitive (pname "extend") prm_extend
+let () = Tac2env.define_primitive (pname "enter") prm_enter
+
+let () = Tac2env.define_primitive (pname "focus") prm_focus
+let () = Tac2env.define_primitive (pname "shelve") prm_shelve
+let () = Tac2env.define_primitive (pname "shelve_unifiable") prm_shelve_unifiable
+let () = Tac2env.define_primitive (pname "new_goal") prm_new_goal
+let () = Tac2env.define_primitive (pname "goal") prm_goal
+let () = Tac2env.define_primitive (pname "hyp") prm_hyp
+let () = Tac2env.define_primitive (pname "refine") prm_refine
+
+(** ML types *)
+
+let constr_flags () =
+  let open Pretyping in
+  {
+    use_typeclasses = true;
+    solve_unification_constraints = true;
+    use_hook = Pfedit.solve_by_implicit_tactic ();
+    fail_evar = true;
+    expand_evars = true
+  }
+
+let open_constr_no_classes_flags () =
+  let open Pretyping in
+  {
+  use_typeclasses = false;
+  solve_unification_constraints = true;
+  use_hook = Pfedit.solve_by_implicit_tactic ();
+  fail_evar = false;
+  expand_evars = true
+  }
+
+(** Embed all Ltac2 data into Values *)
+let to_lvar ist =
+  let open Glob_ops in
+  let map e = Val.Dyn (val_valexpr, e) in
+  let lfun = Id.Map.map map ist in
+  { empty_lvar with Glob_term.ltac_genargs = lfun }
+
+let interp_constr flags ist (c, _) =
+  let open Pretyping in
+  pf_apply begin fun env sigma ->
+  Proofview.V82.wrap_exceptions begin fun () ->
+    let ist = to_lvar ist in
+    let (sigma, c) = understand_ltac flags env sigma ist WithoutTypeConstraint c in
+    let c = Val.Dyn (val_constr, c) in
+    Proofview.Unsafe.tclEVARS sigma >>= fun () ->
+    Proofview.tclUNIT c
+  end
+  end
+
+let () =
+  let interp ist c = interp_constr (constr_flags ()) ist c in
+  let obj = {
+    ml_type = t_constr;
+    ml_interp = interp;
+  } in
+  define_ml_object Stdarg.wit_constr obj
+
+let () =
+  let interp ist c = interp_constr (open_constr_no_classes_flags ()) ist c in
+  let obj = {
+    ml_type = t_constr;
+    ml_interp = interp;
+  } in
+  define_ml_object Stdarg.wit_open_constr obj
+
+let () =
+  let interp _ id = return (Val.Dyn (val_ident, id)) in
+  let obj = {
+    ml_type = t_ident;
+    ml_interp = interp;
+  } in
+  define_ml_object Stdarg.wit_ident obj
+
+let () =
+  let interp ist env sigma concl tac =
+    let fold id (Val.Dyn (tag, v)) (accu : environment) : environment =
+      match Val.eq tag val_valexpr with
+      | None -> accu
+      | Some Refl -> Id.Map.add id v accu
+    in
+    let ist = Id.Map.fold fold ist Id.Map.empty in
+    let tac = Proofview.tclIGNORE (interp ist tac) in
+    let c, sigma = Pfedit.refine_by_tactic env sigma concl tac in
+    (EConstr.of_constr c, sigma)
+  in
+  Pretyping.register_constr_interp0 wit_ltac2 interp
+
+(** Built-in notation scopes *)
+
+let add_scope s f =
+  Tac2entries.register_scope (Id.of_string s) f
+
+let scope_fail () = CErrors.user_err (str "Invalid parsing token")
+
+let dummy_loc = Loc.make_loc (-1, -1)
+
+let rthunk e =
+  let loc = Tac2intern.loc_of_tacexpr e in
+  let var = [Loc.tag ~loc Anonymous, Some (CTypRef (loc, AbsKn Core.t_unit, []))] in
+  CTacFun (loc, var, e)
+
+let add_generic_scope s entry arg =
+  let parse = function
+  | [] ->
+    let scope = Extend.Aentry entry in
+    let act x = rthunk (CTacExt (dummy_loc, in_gen (rawwit arg) x)) in
+    Tac2entries.ScopeRule (scope, act)
+  | _ -> scope_fail ()
+  in
+  add_scope s parse
+
+let () = add_scope "list0" begin function
+| [tok] ->
+  let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in
+  let scope = Extend.Alist0 scope in
+  let act l =
+    let l = List.map act l in
+    CTacLst (None, l)
+  in
+  Tac2entries.ScopeRule (scope, act)
+| [tok; SexprStr (_, str)] ->
+  let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in
+  let sep = Extend.Atoken (CLexer.terminal str) in
+  let scope = Extend.Alist0sep (scope, sep) in
+  let act l =
+    let l = List.map act l in
+    CTacLst (None, l)
+  in
+  Tac2entries.ScopeRule (scope, act)
+| _ -> scope_fail ()
+end
+
+let () = add_scope "list1" begin function
+| [tok] ->
+  let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in
+  let scope = Extend.Alist1 scope in
+  let act l =
+    let l = List.map act l in
+    CTacLst (None, l)
+  in
+  Tac2entries.ScopeRule (scope, act)
+| [tok; SexprStr (_, str)] ->
+  let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in
+  let sep = Extend.Atoken (CLexer.terminal str) in
+  let scope = Extend.Alist1sep (scope, sep) in
+  let act l =
+    let l = List.map act l in
+    CTacLst (None, l)
+  in
+  Tac2entries.ScopeRule (scope, act)
+| _ -> scope_fail ()
+end
+
+let () = add_scope "opt" begin function
+| [tok] ->
+  let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in
+  let scope = Extend.Aopt scope in
+  let act opt = match opt with
+  | None ->
+    CTacRef (AbsKn (TacConstructor Core.c_none))
+  | Some x ->
+    CTacApp (dummy_loc, CTacRef (AbsKn (TacConstructor Core.c_some)), [act x])
+  in
+  Tac2entries.ScopeRule (scope, act)
+| _ -> scope_fail ()
+end
+
+let () = add_scope "self" begin function
+| [] ->
+  let scope = Extend.Aself in
+  let act tac = rthunk tac in
+  Tac2entries.ScopeRule (scope, act)
+| _ -> scope_fail ()
+end
+
+let () = add_scope "next" begin function
+| [] ->
+  let scope = Extend.Anext in
+  let act tac = rthunk tac in
+  Tac2entries.ScopeRule (scope, act)
+| _ -> scope_fail ()
+end
+
+let () = add_scope "tactic" begin function
+| [] ->
+  (** Default to level 5 parsing *)
+  let scope = Extend.Aentryl (Tac2entries.Pltac.tac2expr, 5) in
+  let act tac = rthunk tac in
+  Tac2entries.ScopeRule (scope, act)
+| [SexprInt (loc, n)] ->
+  let () = if n < 0 || n > 5 then scope_fail () in
+  let scope = Extend.Aentryl (Tac2entries.Pltac.tac2expr, n) in
+  let act tac = rthunk tac in
+  Tac2entries.ScopeRule (scope, act)
+| _ -> scope_fail ()
+end
+
+let () = add_generic_scope "ident" Pcoq.Prim.ident Stdarg.wit_ident
+let () = add_generic_scope "constr" Pcoq.Constr.constr Stdarg.wit_constr
diff --git a/src/tac2core.mli b/src/tac2core.mli
new file mode 100644
index 0000000000..fc90499ac6
--- /dev/null
+++ b/src/tac2core.mli
@@ -0,0 +1,62 @@
+(************************************************************************)
+(*  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 Names
+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
+
+val t_int : type_constant
+val t_option : type_constant
+val t_string : type_constant
+val t_array : type_constant
+
+end
+
+(** {5 Ltac2 FFI} *)
+
+(** These functions allow to convert back and forth between OCaml and Ltac2
+    data representation. The [to_*] functions raise an anomaly whenever the data
+    has not expected shape. *)
+
+module Value :
+sig
+
+val of_unit : unit -> valexpr
+val to_unit : valexpr -> unit
+
+val of_int : int -> valexpr
+val to_int : valexpr -> int
+
+val of_bool : bool -> valexpr
+val to_bool : valexpr -> bool
+
+val of_char : char -> valexpr
+val to_char : valexpr -> char
+
+val of_list : valexpr list -> valexpr
+val to_list : valexpr -> valexpr list
+
+val of_constr : EConstr.t -> valexpr
+val to_constr : valexpr -> EConstr.t
+
+val of_exn : Exninfo.iexn -> valexpr
+val to_exn : valexpr -> Exninfo.iexn
+
+val of_ident : Id.t -> valexpr
+val to_ident : valexpr -> Id.t
+
+end
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
new file mode 100644
index 0000000000..46f390a6d4
--- /dev/null
+++ b/src/tac2entries.ml
@@ -0,0 +1,648 @@
+(************************************************************************)
+(*  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 Tac2print
+open Tac2intern
+open Vernacexpr
+
+(** Grammar entries *)
+
+module Pltac =
+struct
+let tac2expr = Pcoq.Gram.entry_create "tactic:tac2expr"
+end
+
+(** Tactic definition *)
+
+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 (TacConstant 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 (TacConstant 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 definition *)
+
+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 (TacConstructor knc)
+  in
+  Tac2env.push_type visibility sp kn;
+  List.iter iter cstrs
+| GTydRec fields ->
+  (** Register fields *)
+  let iter (c, _, _) =
+    let spc = change_sp_label sp c in
+    let knc = change_kn_label kn c in
+    Tac2env.push_projection visibility spc knc
+  in
+  Tac2env.push_type visibility sp kn;
+  List.iter iter fields
+| GTydOpn ->
+  Tac2env.push_type visibility sp kn
+
+let next i =
+  let ans = !i in
+  let () = incr i in
+  ans
+
+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 data = {
+      Tac2env.cdata_prms = params;
+      cdata_type = kn;
+      cdata_args = args;
+      cdata_indx = Some tag;
+    } in
+    Tac2env.define_constructor knc data
+  in
+  Tac2env.define_type kn qdef;
+  List.iter iter cstrs
+| GTydRec fs ->
+  (** Define projections *)
+  let iter i (id, mut, t) =
+    let knp = change_kn_label kn id in
+    let proj = {
+      Tac2env.pdata_prms = params;
+      pdata_type = kn;
+      pdata_ptyp = t;
+      pdata_mutb = mut;
+      pdata_indx = i;
+    } in
+    Tac2env.define_projection knp proj
+  in
+  Tac2env.define_type kn qdef;
+  List.iteri iter fs
+| GTydOpn ->
+  Tac2env.define_type kn qdef
+
+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}
+
+(** Type extension *)
+
+type extension_data = {
+  edata_name : Id.t;
+  edata_args : int glb_typexpr list;
+}
+
+type typext = {
+  typext_local : bool;
+  typext_prms : int;
+  typext_type : type_constant;
+  typext_expr : extension_data list;
+}
+
+let push_typext vis sp kn def =
+  let iter data =
+    let spc = change_sp_label sp data.edata_name in
+    let knc = change_kn_label kn data.edata_name in
+    Tac2env.push_ltac vis spc (TacConstructor knc)
+  in
+  List.iter iter def.typext_expr
+
+let define_typext kn def =
+  let iter data =
+    let knc = change_kn_label kn data.edata_name in
+    let cdata = {
+      Tac2env.cdata_prms = def.typext_prms;
+      cdata_type = def.typext_type;
+      cdata_args = data.edata_args;
+      cdata_indx = None;
+    } in
+    Tac2env.define_constructor knc cdata
+  in
+  List.iter iter def.typext_expr
+
+let cache_typext ((sp, kn), def) =
+  let () = define_typext kn def in
+  push_typext (Until 1) sp kn def
+
+let perform_typext vs ((sp, kn), def) =
+  let () = if not def.typext_local then push_typext vs sp kn def in
+  define_typext kn def
+
+let load_typext i obj = perform_typext (Until i) obj
+let open_typext i obj = perform_typext (Exactly i) obj
+
+let subst_typext (subst, e) =
+  let open Mod_subst in
+  let subst_data data =
+    let edata_args = List.smartmap (fun e -> subst_type subst e) data.edata_args in
+    if edata_args == data.edata_args then data
+    else { data with edata_args }
+  in
+  let typext_type = subst_kn subst e.typext_type in
+  let typext_expr = List.smartmap subst_data e.typext_expr in
+  if typext_type == e.typext_type && typext_expr == e.typext_expr then
+    e
+  else
+    { e with typext_type; typext_expr }
+
+let classify_typext o = Substitute o
+
+let inTypExt : typext -> obj =
+  declare_object {(default_object "TAC2-TYPE-EXTENSION") with
+     cache_function  = cache_typext;
+     load_function   = load_typext;
+     open_function   = open_typext;
+     subst_function = subst_typext;
+     classify_function = classify_typext}
+
+(** Toplevel entries *)
+
+let dummy_loc = Loc.make_loc (-1, -1)
+
+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 (dummy_loc, true, bindings, CTacRef (RelId (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 qualid_to_ident (loc, qid) =
+  let (dp, id) = Libnames.repr_qualid qid in
+  if DirPath.is_empty dp then (loc, id)
+  else user_err ?loc (str "Identifier expected")
+
+let register_typedef ?(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 cs ->
+      let same_name (id1, _) (id2, _) = Id.equal id1 id2 in
+      let () = match List.duplicates same_name cs with
+      | [] -> ()
+      | (id, _) :: _ ->
+        user_err (str "Multiple definitions of the constructor " ++ Id.print id)
+      in
+      ()
+    | CTydRec ps ->
+      let same_name (id1, _, _) (id2, _, _) = Id.equal id1 id2 in
+      let () = match List.duplicates same_name ps with
+      | [] -> ()
+      | (id, _, _) :: _ ->
+        user_err (str "Multiple definitions of the projection " ++ Id.print id)
+      in
+      ()
+    | CTydOpn ->
+      if isrec then
+        user_err ?loc (str "The open type declaration " ++ Id.print id ++
+          str " cannot be recursive")
+  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_open ?(local = false) (loc, qid) (params, def) =
+  let kn =
+    try Tac2env.locate_type qid
+    with Not_found ->
+      user_err ?loc (str "Unbound type " ++ pr_qualid qid)
+  in
+  let (tparams, t) = Tac2env.interp_type kn in
+  let () = match t with
+  | GTydOpn -> ()
+  | GTydAlg _ | GTydRec _ | GTydDef _ ->
+    user_err ?loc (str "Type " ++ pr_qualid qid ++ str " is not an open type")
+  in
+  let () =
+    let loc = Option.default dummy_loc loc in
+    if not (Int.equal (List.length params) tparams) then
+      Tac2intern.error_nparams_mismatch loc (List.length params) tparams
+  in
+  match def with
+  | CTydOpn -> ()
+  | CTydAlg def ->
+    let intern_type t =
+      let tpe = CTydDef (Some t) in
+      let (_, ans) = intern_typedef Id.Map.empty (params, tpe) in
+      match ans with
+      | GTydDef (Some t) -> t
+      | _ -> assert false
+    in
+    let map (id, tpe) =
+      let tpe = List.map intern_type tpe in
+      { edata_name = id; edata_args = tpe }
+    in
+    let def = List.map map def in
+    let def = {
+      typext_local = local;
+      typext_type = kn;
+      typext_prms = tparams;
+      typext_expr = def;
+    } in
+    Lib.add_anonymous_leaf (inTypExt def)
+  | CTydRec _ | CTydDef _ ->
+    user_err ?loc (str "Extensions only accept inductive constructors")
+
+let register_type ?local isrec types = match types with
+| [qid, true, def] ->
+  let (loc, _) = qid in
+  let () = if isrec then user_err ?loc (str "Extensions cannot be recursive") in
+  register_open ?local qid def
+| _ ->
+  let map (qid, redef, def) =
+    let (loc, _) = qid in
+    let () = if redef then
+      user_err ?loc (str "Types can only be extended one by one")
+    in
+    (qualid_to_ident qid, def)
+  in
+  let types = List.map map types in
+  register_typedef ?local isrec types
+
+(** Parsing *)
+
+type 'a token =
+| TacTerm of string
+| TacNonTerm of Name.t * 'a
+
+type scope_rule =
+| ScopeRule : (raw_tacexpr, 'a) Extend.symbol * ('a -> raw_tacexpr) -> scope_rule
+
+type scope_interpretation = sexpr list -> scope_rule
+
+let scope_table : scope_interpretation Id.Map.t ref = ref Id.Map.empty
+
+let register_scope id s =
+  scope_table := Id.Map.add id s !scope_table
+
+module ParseToken =
+struct
+
+let loc_of_token = function
+| SexprStr (loc, _) -> Option.default dummy_loc loc
+| SexprInt (loc, _) -> Option.default dummy_loc loc
+| SexprRec (loc, _, _) -> loc
+
+let parse_scope = function
+| SexprRec (_, (loc, Some id), toks) ->
+  if Id.Map.mem id !scope_table then
+    Id.Map.find id !scope_table toks
+  else
+    CErrors.user_err ?loc (str "Unknown scope" ++ spc () ++ Nameops.pr_id id)
+| tok ->
+  let loc = loc_of_token tok in
+  CErrors.user_err ~loc (str "Invalid parsing token")
+
+let parse_token = function
+| SexprStr (_, s) -> TacTerm s
+| SexprRec (_, (_, na), [tok]) ->
+  let na = match na with None -> Anonymous | Some id -> Name id in
+  let scope = parse_scope tok in
+  TacNonTerm (na, scope)
+| tok ->
+  let loc = loc_of_token tok in
+  CErrors.user_err ~loc (str "Invalid parsing token")
+
+end
+
+let parse_scope = ParseToken.parse_scope
+
+type synext = {
+  synext_tok : sexpr list;
+  synext_exp : raw_tacexpr;
+  synext_lev : int option;
+  synext_loc : bool;
+}
+
+type krule =
+| KRule :
+  (raw_tacexpr, 'act, Loc.t -> raw_tacexpr) Extend.rule *
+  ((Loc.t -> (Name.t * raw_tacexpr) list -> raw_tacexpr) -> 'act) -> krule
+
+let rec get_rule (tok : scope_rule token list) : krule = match tok with
+| [] -> KRule (Extend.Stop, fun k loc -> k loc [])
+| TacNonTerm (na, ScopeRule (scope, inj)) :: tok ->
+  let KRule (rule, act) = get_rule tok in
+  let rule = Extend.Next (rule, scope) in
+  let act k e = act (fun loc acc -> k loc ((na, inj e) :: acc)) in
+  KRule (rule, act)
+| TacTerm t :: tok ->
+  let KRule (rule, act) = get_rule tok in
+  let rule = Extend.Next (rule, Extend.Atoken (CLexer.terminal t)) in
+  let act k _ = act k in
+  KRule (rule, act)
+
+let perform_notation syn st =
+  let tok = List.rev_map ParseToken.parse_token syn.synext_tok in
+  let KRule (rule, act) = get_rule tok in
+  let mk loc args =
+    let map (na, e) =
+      let loc = loc_of_tacexpr e in
+      (Loc.tag ~loc na, None, e)
+    in
+    let bnd = List.map map args in
+    CTacLet (loc, false, bnd, syn.synext_exp)
+  in
+  let rule = Extend.Rule (rule, act mk) in
+  let lev = match syn.synext_lev with
+  | None -> None
+  | Some lev -> Some (string_of_int lev)
+  in
+  let rule = (lev, None, [rule]) in
+  ([Pcoq.ExtendRule (Pltac.tac2expr, None, (None, [rule]))], st)
+
+let ltac2_notation =
+  Pcoq.create_grammar_command "ltac2-notation" perform_notation
+
+let cache_synext (_, syn) =
+  Pcoq.extend_grammar_command ltac2_notation syn
+
+let open_synext i (_, syn) =
+  if Int.equal i 1 then Pcoq.extend_grammar_command ltac2_notation syn
+
+let subst_synext (subst, syn) =
+  let e = Tac2intern.subst_rawexpr subst syn.synext_exp in
+  if e == syn.synext_exp then syn else { syn with synext_exp = e }
+
+let classify_synext o =
+  if o.synext_loc then Dispose else Substitute o
+
+let inTac2Notation : synext -> obj =
+  declare_object {(default_object "TAC2-NOTATION") with
+     cache_function  = cache_synext;
+     open_function   = open_synext;
+     subst_function = subst_synext;
+     classify_function = classify_synext}
+
+let register_notation ?(local = false) tkn lev body =
+  (** Check that the tokens make sense *)
+  let entries = List.map ParseToken.parse_token tkn in
+  let fold accu tok = match tok with
+  | TacTerm _ -> accu
+  | TacNonTerm (Name id, _) -> Id.Set.add id accu
+  | TacNonTerm (Anonymous, _) -> accu
+  in
+  let ids = List.fold_left fold Id.Set.empty entries in
+  (** Globalize so that names are absolute *)
+  let body = Tac2intern.globalize ids body in
+  let ext = {
+    synext_tok = tkn;
+    synext_exp = body;
+    synext_lev = lev;
+    synext_loc = local;
+  } in
+  Lib.add_anonymous_leaf (inTac2Notation ext)
+
+(** Toplevel entries *)
+
+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
+| StrSyn (tok, lev, e) -> register_notation ?local tok lev e
+
+(** 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
+  match kn with
+  | TacConstant kn ->
+    let (e, _, (_, t)) = Tac2env.interp_global kn in
+    let name = int_name () in
+    Feedback.msg_notice (
+      hov 0 (
+        hov 2 (pr_qualid qid ++ spc () ++ str ":" ++ spc () ++ pr_glbtype name t) ++ fnl () ++
+        hov 2 (pr_qualid qid ++ spc () ++ str ":=" ++ spc () ++ pr_glbexpr e)
+      )
+    )
+  | TacConstructor kn ->
+    let _ = Tac2env.interp_constructor kn in
+    Feedback.msg_notice (hov 2 (str "Constructor" ++ spc () ++ str ":" ++ spc () ++ pr_qualid qid))
+
+(** 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_def n = KerName.make2 Tac2env.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/src/tac2entries.mli b/src/tac2entries.mli
new file mode 100644
index 0000000000..71e8150057
--- /dev/null
+++ b/src/tac2entries.mli
@@ -0,0 +1,57 @@
+(************************************************************************)
+(*  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 Libnames
+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 ->
+  (qualid located * redef_flag * 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
+
+val register_notation : ?local:bool -> sexpr list -> int option ->
+  raw_tacexpr -> unit
+
+(** {5 Notations} *)
+
+type scope_rule =
+| ScopeRule : (raw_tacexpr, 'a) Extend.symbol * ('a -> raw_tacexpr) -> scope_rule
+
+type scope_interpretation = sexpr list -> scope_rule
+
+val register_scope : Id.t -> scope_interpretation -> unit
+(** Create a new scope with the provided name *)
+
+val parse_scope : sexpr -> scope_rule
+(** Use this to interpret the subscopes for interpretation functions *)
+
+(** {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
+
+(** {5 Parsing entries} *)
+
+module Pltac :
+sig
+val tac2expr : raw_tacexpr Pcoq.Gram.entry
+end
diff --git a/src/tac2env.ml b/src/tac2env.ml
new file mode 100644
index 0000000000..5ccdd018ee
--- /dev/null
+++ b/src/tac2env.ml
@@ -0,0 +1,242 @@
+(************************************************************************)
+(*  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 Names
+open Libnames
+open Tac2expr
+
+type constructor_data = {
+  cdata_prms : int;
+  cdata_type : type_constant;
+  cdata_args : int glb_typexpr list;
+  cdata_indx : int option;
+}
+
+type projection_data = {
+  pdata_prms : int;
+  pdata_type : type_constant;
+  pdata_ptyp : int glb_typexpr;
+  pdata_mutb : bool;
+  pdata_indx : int;
+}
+
+type ltac_state = {
+  ltac_tactics : (glb_tacexpr * type_scheme) KNmap.t;
+  ltac_constructors : constructor_data KNmap.t;
+  ltac_projections : projection_data KNmap.t;
+  ltac_types : glb_quant_typedef KNmap.t;
+}
+
+let empty_state = {
+  ltac_tactics = KNmap.empty;
+  ltac_constructors = KNmap.empty;
+  ltac_projections = 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 }
+| GTacCst (_, n, []) -> ValInt n
+| GTacCst (_, n, el) -> ValBlk (n, Array.map_of_list eval_pure el)
+| GTacOpn (kn, el) -> ValOpn (kn, Array.map_of_list eval_pure el)
+| GTacAtm (AtmStr _) | GTacArr _ | GTacLet _ | GTacVar _ | GTacSet _
+| GTacApp _ | GTacCse _ | GTacPrj _ | GTacPrm _ | GTacExt _ | GTacWth _ ->
+  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
+  (e, 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_projection kn t =
+  let state = !ltac_state in
+  ltac_state := { state with ltac_projections = KNmap.add kn t state.ltac_projections }
+
+let interp_projection kn = KNmap.find kn ltac_state.contents.ltac_projections
+
+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
+
+type tacref = Tac2expr.tacref =
+| TacConstant of ltac_constant
+| TacConstructor of ltac_constructor
+
+module TacRef =
+struct
+type t = tacref
+let equal r1 r2 = match r1, r2 with
+| TacConstant c1, TacConstant c2 -> KerName.equal c1 c2
+| TacConstructor c1, TacConstructor c2 -> KerName.equal c1 c2
+| _ -> false
+end
+
+module KnTab = Nametab.Make(FullPath)(KerName)
+module RfTab = Nametab.Make(FullPath)(TacRef)
+
+type nametab = {
+  tab_ltac : RfTab.t;
+  tab_ltac_rev : full_path KNmap.t * full_path KNmap.t;
+  tab_type : KnTab.t;
+  tab_type_rev : full_path KNmap.t;
+  tab_proj : KnTab.t;
+  tab_proj_rev : full_path KNmap.t;
+}
+
+let empty_nametab = {
+  tab_ltac = RfTab.empty;
+  tab_ltac_rev = (KNmap.empty, KNmap.empty);
+  tab_type = KnTab.empty;
+  tab_type_rev = KNmap.empty;
+  tab_proj = KnTab.empty;
+  tab_proj_rev = KNmap.empty;
+}
+
+let nametab = Summary.ref empty_nametab ~name:"ltac2-nametab"
+
+let push_ltac vis sp kn =
+  let tab = !nametab in
+  let tab_ltac = RfTab.push vis sp kn tab.tab_ltac in
+  let (constant_map, constructor_map) = tab.tab_ltac_rev in
+  let tab_ltac_rev = match kn with
+  | TacConstant c -> (KNmap.add c sp constant_map, constructor_map)
+  | TacConstructor c -> (constant_map, KNmap.add c sp constructor_map)
+  in
+  nametab := { tab with tab_ltac; tab_ltac_rev }
+
+let locate_ltac qid =
+  let tab = !nametab in
+  RfTab.locate qid tab.tab_ltac
+
+let locate_extended_all_ltac qid =
+  let tab = !nametab in
+  RfTab.find_prefixes qid tab.tab_ltac
+
+let shortest_qualid_of_ltac kn =
+  let tab = !nametab in
+  let sp = match kn with
+  | TacConstant c -> KNmap.find c (fst tab.tab_ltac_rev)
+  | TacConstructor c -> KNmap.find c (snd tab.tab_ltac_rev)
+  in
+  RfTab.shortest_qualid Id.Set.empty sp tab.tab_ltac
+
+let push_type vis sp kn =
+  let tab = !nametab in
+  let tab_type = KnTab.push vis sp kn tab.tab_type in
+  let tab_type_rev = KNmap.add kn sp tab.tab_type_rev in
+  nametab := { tab with tab_type; tab_type_rev }
+
+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
+
+let shortest_qualid_of_type kn =
+  let tab = !nametab in
+  let sp = KNmap.find kn tab.tab_type_rev in
+  KnTab.shortest_qualid Id.Set.empty sp tab.tab_type
+
+let push_projection vis sp kn =
+  let tab = !nametab in
+  let tab_proj = KnTab.push vis sp kn tab.tab_proj in
+  let tab_proj_rev = KNmap.add kn sp tab.tab_proj_rev in
+  nametab := { tab with tab_proj; tab_proj_rev }
+
+let locate_projection qid =
+  let tab = !nametab in
+  KnTab.locate qid tab.tab_proj
+
+let locate_extended_all_projection qid =
+  let tab = !nametab in
+  KnTab.find_prefixes qid tab.tab_proj
+
+let shortest_qualid_of_projection kn =
+  let tab = !nametab in
+  let sp = KNmap.find kn tab.tab_proj_rev in
+  KnTab.shortest_qualid Id.Set.empty sp tab.tab_proj
+
+type 'a ml_object = {
+  ml_type : type_constant;
+  ml_interp : environment -> 'a -> Geninterp.Val.t Proofview.tactic;
+}
+
+module MLTypeObj =
+struct
+  type ('a, 'b, 'c) obj = 'b ml_object
+  let name = "ltac2_ml_type"
+  let default _ = None
+end
+
+module MLType = Genarg.Register(MLTypeObj)
+
+let define_ml_object t tpe = MLType.register0 t tpe
+let interp_ml_object t = MLType.obj t
+
+(** Absolute paths *)
+
+let coq_prefix =
+  MPfile (DirPath.make (List.map Id.of_string ["Init"; "ltac2"; "Coq"]))
+
+(** Generic arguments *)
+
+let wit_ltac2 = Genarg.make0 "ltac2"
diff --git a/src/tac2env.mli b/src/tac2env.mli
new file mode 100644
index 0000000000..c4b8c1e0ca
--- /dev/null
+++ b/src/tac2env.mli
@@ -0,0 +1,106 @@
+(************************************************************************)
+(*  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 *)
+
+(** {5 Toplevel definition of values} *)
+
+val define_global : ltac_constant -> (glb_tacexpr * type_scheme) -> unit
+val interp_global : ltac_constant -> (glb_tacexpr * 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_prms : int;
+  (** Type parameters *)
+  cdata_type : type_constant;
+  (** Inductive definition to which the constructor pertains *)
+  cdata_args : int glb_typexpr list;
+  (** Types of the constructor arguments *)
+  cdata_indx : int option;
+  (** Index of the constructor in the ADT. Numbering is duplicated between
+      argumentless and argument-using constructors, e.g. in type ['a option]
+      [None] and [Some] have both index 0. This field is empty whenever the
+      constructor is a member of an open type. *)
+}
+
+val define_constructor : ltac_constructor -> constructor_data -> unit
+val interp_constructor : ltac_constructor -> constructor_data
+
+(** {5 Toplevel definition of projections} *)
+
+type projection_data = {
+  pdata_prms : int;
+  (** Type parameters *)
+  pdata_type : type_constant;
+  (** Record definition to which the projection pertains *)
+  pdata_ptyp : int glb_typexpr;
+  (** Type of the projection *)
+  pdata_mutb : bool;
+  (** Whether the field is mutable *)
+  pdata_indx : int;
+  (** Index of the projection *)
+}
+
+val define_projection : ltac_projection -> projection_data -> unit
+val interp_projection : ltac_projection -> projection_data
+
+(** {5 Name management} *)
+
+val push_ltac : visibility -> full_path -> tacref -> unit
+val locate_ltac : qualid -> tacref
+val locate_extended_all_ltac : qualid -> tacref list
+val shortest_qualid_of_ltac : tacref -> qualid
+
+val push_type : visibility -> full_path -> type_constant -> unit
+val locate_type : qualid -> type_constant
+val locate_extended_all_type : qualid -> type_constant list
+val shortest_qualid_of_type : type_constant -> qualid
+
+val push_projection : visibility -> full_path -> ltac_projection -> unit
+val locate_projection : qualid -> ltac_projection
+val locate_extended_all_projection : qualid -> ltac_projection list
+val shortest_qualid_of_projection : ltac_projection -> qualid
+
+(** {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
+
+(** {5 ML primitive types} *)
+
+type 'a ml_object = {
+  ml_type : type_constant;
+  ml_interp : environment -> 'a -> Geninterp.Val.t Proofview.tactic;
+}
+
+val define_ml_object : ('a, 'b, 'c) genarg_type -> 'b ml_object -> unit
+val interp_ml_object : ('a, 'b, 'c) genarg_type -> 'b ml_object
+
+(** {5 Absolute paths} *)
+
+val coq_prefix : ModPath.t
+(** Path where primitive datatypes are defined in Ltac2 plugin. *)
+
+(** {5 Generic arguments} *)
+
+val wit_ltac2 : (raw_tacexpr, glb_tacexpr, Util.Empty.t) genarg_type
diff --git a/src/tac2expr.mli b/src/tac2expr.mli
new file mode 100644
index 0000000000..acdad9bab4
--- /dev/null
+++ b/src/tac2expr.mli
@@ -0,0 +1,195 @@
+(************************************************************************)
+(*  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 redef_flag = bool
+type lid = Id.t
+type uid = Id.t
+
+type ltac_constant = KerName.t
+type ltac_constructor = KerName.t
+type ltac_projection = KerName.t
+type type_constant = KerName.t
+
+type 'a or_relid =
+| RelId of qualid located
+| AbsKn of 'a
+
+(** {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 * type_constant or_relid * 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
+| CTydOpn
+
+type 'a glb_typexpr =
+| GTypVar of 'a
+| GTypArrow of 'a glb_typexpr * 'a glb_typexpr
+| GTypTuple of 'a glb_typexpr list
+| GTypRef of type_constant * '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
+| GTydOpn
+
+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
+
+type tacref =
+| TacConstant of ltac_constant
+| TacConstructor of ltac_constructor
+
+(** Tactic expressions *)
+type raw_patexpr =
+| CPatAny of Loc.t
+| CPatRef of Loc.t * ltac_constructor or_relid * raw_patexpr list
+| CPatTup of raw_patexpr list located
+
+type raw_tacexpr =
+| CTacAtm of atom located
+| CTacRef of tacref or_relid
+| 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
+| CTacRec of Loc.t * raw_recexpr
+| CTacPrj of Loc.t * raw_tacexpr * ltac_projection or_relid
+| CTacSet of Loc.t * raw_tacexpr * ltac_projection or_relid * raw_tacexpr
+| CTacExt of Loc.t * raw_generic_argument
+
+and raw_taccase = raw_patexpr * raw_tacexpr
+
+and raw_recexpr = (ltac_projection or_relid * raw_tacexpr) list
+
+type case_info =
+| GCaseTuple of int
+| GCaseAlg of type_constant
+
+type 'a open_match = {
+  opn_match : 'a;
+  opn_branch : (Name.t * Name.t array * 'a) KNmap.t;
+  (** Invariant: should not be empty *)
+  opn_default : Name.t * 'a;
+}
+
+type glb_tacexpr =
+| GTacAtm of atom
+| GTacVar of Id.t
+| GTacRef of ltac_constant
+| 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
+| GTacArr of glb_tacexpr list
+| GTacCst of case_info * int * glb_tacexpr list
+| GTacCse of glb_tacexpr * case_info * glb_tacexpr array * (Name.t array * glb_tacexpr) array
+| GTacPrj of type_constant * glb_tacexpr * int
+| GTacSet of type_constant * glb_tacexpr * int * glb_tacexpr
+| GTacOpn of ltac_constructor * glb_tacexpr list
+| GTacWth of glb_tacexpr open_match
+| GTacExt of glob_generic_argument
+| GTacPrm of ml_tactic_name * glb_tacexpr list
+
+(** {5 Parsing & Printing} *)
+
+type exp_level =
+| E5
+| E4
+| E3
+| E2
+| E1
+| E0
+
+type sexpr =
+| SexprStr of string located
+| SexprInt of int located
+| SexprRec of Loc.t * Id.t option located * sexpr list
+
+(** {5 Toplevel statements} *)
+
+type strexpr =
+| StrVal of rec_flag * (Name.t located * raw_tacexpr) list
+  (** Term definition *)
+| StrTyp of rec_flag * (qualid located * redef_flag * raw_quant_typedef) list
+  (** Type definition *)
+| StrPrm of Id.t located * raw_typexpr * ml_tactic_name
+  (** External definition *)
+| StrSyn of sexpr list * int option * raw_tacexpr
+  (** Syntactic extensions *)
+
+
+(** {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, named constructors, 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 Bytes.t
+  (** Strings *)
+| ValCls of closure
+  (** Closures *)
+| ValOpn of KerName.t * valexpr array
+  (** Open constructors *)
+| 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
+
+type environment = valexpr Id.Map.t
diff --git a/src/tac2intern.ml b/src/tac2intern.ml
new file mode 100644
index 0000000000..b63e6a0cd8
--- /dev/null
+++ b/src/tac2intern.ml
@@ -0,0 +1,1454 @@
+(************************************************************************)
+(*  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 Tac2print
+open Tac2expr
+
+(** Hardwired types and constants *)
+
+let coq_type n = KerName.make2 Tac2env.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 (GCaseAlg t_list, 0, [])
+let c_cons e el = GTacCst (GCaseAlg 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 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
+  val exists : (key -> 'a -> bool) -> 'a t -> bool
+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 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 env_name env =
+  (** Generate names according to a provided environment *)
+  let mk num =
+    let base = num mod 26 in
+    let rem = num / 26 in
+    let name = String.make 1 (Char.chr (97 + base)) in
+    let suff = if Int.equal rem 0 then "" else string_of_int rem in
+    let name = name ^ suff in
+    name
+  in
+  let fold id elt acc = UF.Map.add elt (Id.to_string id) acc in
+  let vars = Id.Map.fold fold env.env_als.contents UF.Map.empty in
+  let vars = ref vars in
+  let rec fresh n =
+    let name = mk n in
+    if UF.Map.exists (fun _ name' -> String.equal name name') !vars then fresh (succ n)
+    else name
+  in
+  fun n ->
+    if UF.Map.mem n !vars then UF.Map.find n !vars
+    else
+      let ans = fresh 0 in
+      let () = vars := UF.Map.add n ans !vars in
+      ans
+
+let ltac2_env : environment Genintern.Store.field =
+  Genintern.Store.field ()
+
+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 dummy_loc = Loc.make_loc (-1, -1)
+
+let loc_of_tacexpr = function
+| CTacAtm (loc, _) -> Option.default dummy_loc loc
+| CTacRef (RelId (loc, _)) -> Option.default dummy_loc loc
+| CTacRef (AbsKn _) -> dummy_loc
+| CTacFun (loc, _, _) -> loc
+| CTacApp (loc, _, _) -> loc
+| CTacLet (loc, _, _, _) -> loc
+| CTacTup (loc, _) -> Option.default dummy_loc loc
+| CTacArr (loc, _) -> Option.default dummy_loc loc
+| CTacLst (loc, _) -> Option.default dummy_loc loc
+| CTacCnv (loc, _, _) -> loc
+| CTacSeq (loc, _, _) -> loc
+| CTacCse (loc, _, _) -> loc
+| CTacRec (loc, _) -> loc
+| CTacPrj (loc, _, _) -> loc
+| CTacSet (loc, _, _, _) -> loc
+| CTacExt (loc, _) -> loc
+
+let loc_of_patexpr = function
+| CPatAny loc -> loc
+| CPatRef (loc, _, _) -> loc
+| CPatTup (loc, _) -> Option.default dummy_loc loc
+
+let error_nargs_mismatch loc nargs nfound =
+  user_err ~loc (str "Constructor expects " ++ int nargs ++
+    str " arguments, but is applied to " ++ int nfound ++
+    str " arguments")
+
+let error_nparams_mismatch loc nargs nfound =
+  user_err ~loc (str "Type expects " ++ int nargs ++
+    str " arguments, but is applied to " ++ int nfound ++
+    str " arguments")
+
+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.tag ?loc id) env)
+| CTypVar (_, Anonymous) -> GTypVar (fresh_id env)
+| CTypRef (loc, rel, args) ->
+  let (kn, nparams) = match rel with
+  | RelId (loc, qid) ->
+    let (dp, id) = repr_qualid qid in
+    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)
+  | AbsKn kn ->
+    let (nparams, _) = Tac2env.interp_type kn in
+    (kn, nparams)
+  in
+  let nargs = List.length args in
+  let () =
+    if not (Int.equal nparams nargs) then
+      let loc, qid = match rel with
+      | RelId lid -> lid
+      | AbsKn kn -> Some loc, shortest_qualid_of_type kn
+      in
+      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 _ | GTydOpn -> 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))
+
+let unify ?loc env t1 t2 =
+  try unify env t1 t2
+  with CannotUnify (u1, u2) ->
+    let name = env_name env in
+    user_err ?loc (str "This expression has type " ++ pr_glbtype name t1 ++
+      str " but an expression what expected of type " ++ pr_glbtype name t2)
+
+(** Term typing *)
+
+let is_pure_constructor kn =
+  match snd (Tac2env.interp_type kn) with
+  | GTydAlg _ | GTydOpn -> true
+  | GTydRec fields ->
+    let is_pure (_, mut, _) = not mut in
+    List.for_all is_pure fields
+  | GTydDef _ -> assert false (** Type definitions have no constructors *)
+
+let rec is_value = function
+| GTacAtm (AtmInt _) | GTacVar _ | GTacRef _ | GTacFun _ -> true
+| GTacAtm (AtmStr _) | GTacApp _ | GTacLet _ -> false
+| GTacCst (GCaseTuple _, _, el) -> List.for_all is_value el
+| GTacCst (_, _, []) -> true
+| GTacOpn (_, el) -> List.for_all is_value el
+| GTacCst (GCaseAlg kn, _, el) -> is_pure_constructor kn && List.for_all is_value el
+| GTacArr _ | GTacCse _ | GTacPrj _ | GTacSet _ | GTacExt _ | GTacPrm _
+| GTacWth _ -> false
+
+let is_rec_rhs = function
+| GTacFun _ -> true
+| GTacAtm _ | GTacVar _ | GTacRef _ | GTacApp _ | GTacLet _ | GTacPrj _
+| GTacSet _ | GTacArr _ | GTacExt _ | GTacPrm _ | GTacCst _
+| GTacCse _ | GTacOpn _ | GTacWth _ -> 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 _ ->
+  let name = env_name env in
+  user_err ~loc (str "Type " ++ pr_glbtype name t ++ str " is not an empty type")
+| GTypRef (kn, _) ->
+  let def = Tac2env.interp_type kn in
+  match def with
+  | _, GTydAlg [] -> kn
+  | _ ->
+    let name = env_name env in
+    user_err ~loc (str "Type " ++ pr_glbtype name 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_variable0 mem var = match var with
+| RelId (loc, qid) ->
+  let (dp, id) = repr_qualid qid in
+  if DirPath.is_empty dp && mem id 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
+| AbsKn kn -> ArgArg kn
+
+let get_variable env var =
+  let mem id = Id.Map.mem id env.env_var in
+  get_variable0 mem var
+
+let get_constructor env var = match var with
+| RelId (loc, qid) ->
+  let c = try Some (Tac2env.locate_ltac qid) with Not_found -> None in
+  begin match c with
+  | Some (TacConstructor knc) ->
+    let kn = Tac2env.interp_constructor knc in
+    ArgArg (kn, knc)
+  | Some (TacConstant _) ->
+    CErrors.user_err ?loc (str "The term " ++ pr_qualid qid ++
+      str " is not the constructor of an inductive type.")
+  | 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)
+  end
+| AbsKn knc ->
+  let kn = Tac2env.interp_constructor knc in
+  ArgArg (kn, knc)
+
+let get_projection var = match var with
+| RelId (loc, qid) ->
+  let kn = try Tac2env.locate_projection qid with Not_found ->
+    user_err ?loc (pr_qualid qid ++ str " is not a projection")
+  in
+  Tac2env.interp_projection kn
+| AbsKn kn ->
+  Tac2env.interp_projection kn
+
+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' -> pr_typref kn
+  | GCaseTuple n -> str "tuple"
+  in
+  user_err ?loc (str "Invalid pattern, expected a pattern for type " ++
+    pr_typref kn ++ str ", found a pattern of type " ++ pt) (** FIXME *)
+
+(** Pattern view *)
+
+type glb_patexpr =
+| GPatVar of Name.t
+| GPatRef of ltac_constructor * glb_patexpr list
+| GPatTup of glb_patexpr list
+
+let rec intern_patexpr env = function
+| CPatAny _ -> GPatVar Anonymous
+| CPatRef (_, qid, []) ->
+  begin match get_constructor env qid with
+  | ArgVar (_, id) -> GPatVar (Name id)
+  | ArgArg (_, kn) -> GPatRef (kn, [])
+  end
+| CPatRef (_, qid, pl) ->
+  begin match get_constructor env qid with
+  | ArgVar (loc, id) ->
+    user_err ?loc (str "Unbound constructor " ++ Nameops.pr_id id)
+  | ArgArg (_, kn) -> GPatRef (kn, List.map (fun p -> intern_patexpr env p) pl)
+  end
+| CPatTup (_, pl) ->
+  GPatTup (List.map (fun p -> intern_patexpr env p) pl)
+
+type pattern_kind =
+| PKind_empty
+| PKind_variant of type_constant
+| PKind_open of type_constant
+| 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 intern_patexpr env p with
+  | GPatVar _ ->
+    begin match pl with
+    | [] -> PKind_any
+    | p :: pl -> get_kind p pl
+    end
+  | GPatRef (kn, pl) ->
+    let data = Tac2env.interp_constructor kn in
+    if Option.is_empty data.cdata_indx then PKind_open data.cdata_type
+    else PKind_variant data.cdata_type
+  | GPatTup tp -> PKind_tuple (List.length tp)
+  in
+  get_kind p pl
+
+(** Internalization *)
+
+let is_constructor env qid = match get_variable env qid with
+| ArgArg (TacConstructor _) -> true
+| _ -> false
+
+let rec intern_rec env = function
+| CTacAtm (_, atm) -> intern_atm env atm
+| CTacRef qid as e ->
+  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 (TacConstant kn) ->
+    let (_, _, sch) = Tac2env.interp_global kn in
+    (GTacRef kn, fresh_type_scheme env sch)
+  | ArgArg (TacConstructor kn) ->
+    let loc = loc_of_tacexpr e in
+    intern_constructor env loc kn []
+  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 bnd = List.rev 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, CTacRef qid, args) as e when is_constructor env qid ->
+  let kn = match get_variable env qid with
+  | ArgArg (TacConstructor kn) -> kn
+  | _ -> assert false
+  in
+  let loc = loc_of_tacexpr e in
+  intern_constructor env loc kn args
+| 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, []) ->
+  (GTacCst (GCaseAlg t_unit, 0, []), 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
+  (GTacCst (GCaseTuple (List.length el), 0, 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 = intern_rec_with_constraint env e t0 :: 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 = c_cons (intern_rec_with_constraint env e t0) 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
+| CTacRec (loc, fs) ->
+  intern_record env loc fs
+| CTacPrj (loc, e, proj) ->
+  let pinfo = get_projection proj in
+  let loc = loc_of_tacexpr e in
+  let (e, t) = intern_rec env e in
+  let subst = Array.init pinfo.pdata_prms (fun _ -> fresh_id env) in
+  let params = Array.map_to_list (fun i -> GTypVar i) subst in
+  let exp = GTypRef (pinfo.pdata_type, params) in
+  let () = unify ~loc env t exp in
+  let substf i = GTypVar subst.(i) in
+  let ret = subst_type substf pinfo.pdata_ptyp in
+  (GTacPrj (pinfo.pdata_type, e, pinfo.pdata_indx), ret)
+| CTacSet (loc, e, proj, r) ->
+  let pinfo = get_projection proj in
+  let () =
+    if not pinfo.pdata_mutb then
+      let loc = match proj with
+      | RelId (loc, _) -> loc
+      | AbsKn _ -> None
+      in
+      user_err ?loc (str "Field is not mutable")
+  in
+  let subst = Array.init pinfo.pdata_prms (fun _ -> fresh_id env) in
+  let params = Array.map_to_list (fun i -> GTypVar i) subst in
+  let exp = GTypRef (pinfo.pdata_type, params) in
+  let e = intern_rec_with_constraint env e exp in
+  let substf i = GTypVar subst.(i) in
+  let ret = subst_type substf pinfo.pdata_ptyp in
+  let r = intern_rec_with_constraint env r ret in
+  (GTacSet (pinfo.pdata_type, e, pinfo.pdata_indx, r), GTypRef (t_unit, []))
+| CTacExt (loc, ext) ->
+  let open Genintern in
+  let GenArg (Rawwit tag, _) = ext in
+  let tpe = interp_ml_object tag in
+  (** External objects do not have access to the named context because this is
+      not stable by dynamic semantics. *)
+  let genv = Global.env_of_context Environ.empty_named_context_val in
+  let ist = empty_glob_sign genv in
+  let ist = { ist with extra = Store.set ist.extra ltac2_env env } in
+  let (_, ext) = Flags.with_option Ltac_plugin.Tacintern.strict_check (fun () -> generic_intern ist ext) () in
+  (GTacExt ext, GTypRef (tpe.ml_type, []))
+
+and intern_rec_with_constraint env e exp =
+  let loc = loc_of_tacexpr e in
+  let (e, t) = intern_rec env e in
+  let () = unify ~loc env t exp in
+  e
+
+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 intern_patexpr env pat with
+    | GPatVar na -> na
+    | _ -> 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:(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:(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:(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 data.cdata_args in
+        let () =
+          if not (Int.equal nids nargs) then error_nargs_mismatch loc nargs nids
+        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 data.cdata_args in
+        let (br', brT) = intern_rec nenv br in
+        let () =
+          let index = match data.cdata_indx with
+          | Some i -> i
+          | None -> assert false
+          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:(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 "TODO: 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)
+  | PKind_open kn ->
+    let subst, tc = fresh_reftype env kn in
+    let () = unify ~loc:(loc_of_tacexpr e) env t tc in
+    let ret = GTypVar (fresh_id env) in
+    let rec intern_branch map = function
+    | [] ->
+      user_err ~loc (str "Missing default case")
+    | (pat, br) :: rem ->
+      match intern_patexpr env pat with
+      | GPatVar na ->
+        let () = check_redundant_clause rem in
+        let nenv = push_name na (monomorphic tc) env in
+        let br' = intern_rec_with_constraint nenv br ret in
+        let def = (na, br') in
+        (map, def)
+      | GPatRef (knc, args) ->
+        let get = function
+        | GPatVar na -> na
+        | GPatRef _ | GPatTup _ ->
+          user_err ~loc (str "TODO: Unhandled match case") (** FIXME *)
+        in
+        let loc = loc_of_patexpr pat in
+        let ids = List.map get args in
+        let data = Tac2env.interp_constructor knc in
+        let () =
+          if not (KerName.equal kn data.cdata_type) then
+            invalid_pattern ~loc kn (GCaseAlg data.cdata_type)
+        in
+        let nids = List.length ids in
+        let nargs = List.length data.cdata_args in
+        let () =
+          if not (Int.equal nids nargs) then error_nargs_mismatch loc nargs nids
+        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 data.cdata_args in
+        let br' = intern_rec_with_constraint nenv br ret in
+        let map =
+          if KNmap.mem knc map then
+            let () = warn_redundant_clause ~loc () in
+            map
+          else
+            KNmap.add knc (Anonymous, Array.of_list ids, br') map
+        in
+        intern_branch map rem
+      | GPatTup tup ->
+        invalid_pattern ~loc kn (GCaseTuple (List.length tup))
+    in
+    let (map, def) = intern_branch KNmap.empty pl in
+    (GTacWth { opn_match = e'; opn_branch = map; opn_default = def }, ret)
+
+and intern_constructor env loc kn args =
+  let cstr = interp_constructor kn in
+  let nargs = List.length cstr.cdata_args in
+  if Int.equal nargs (List.length args) then
+    let subst = Array.init cstr.cdata_prms (fun _ -> fresh_id env) in
+    let substf i = GTypVar subst.(i) in
+    let types = List.map (fun t -> subst_type substf t) cstr.cdata_args in
+    let ans = GTypRef (cstr.cdata_type, List.init cstr.cdata_prms (fun i -> GTypVar subst.(i))) in
+    let map arg tpe = intern_rec_with_constraint env arg tpe in
+    let args = List.map2 map args types in
+    match cstr.cdata_indx with
+    | Some idx ->
+      (GTacCst (GCaseAlg cstr.cdata_type, idx, args), ans)
+    | None ->
+      (GTacOpn (kn, args), ans)
+  else
+    error_nargs_mismatch loc nargs (List.length args)
+
+and intern_record env loc fs =
+  let map (proj, e) =
+    let loc = match proj with
+    | RelId (loc, _) -> loc
+    | AbsKn _ -> None
+    in
+    let proj = get_projection proj in
+    (loc, proj, e)
+  in
+  let fs = List.map map fs in
+  let kn = match fs with
+  | [] -> user_err ~loc (str "Cannot infer the corresponding record type")
+  | (_, proj, _) :: _ -> proj.pdata_type
+  in
+  let params, typdef = match Tac2env.interp_type kn with
+  | n, GTydRec def -> n, def
+  | _ -> assert false
+  in
+  let subst = Array.init params (fun _ -> fresh_id env) in
+  (** Set the answer [args] imperatively *)
+  let args = Array.make (List.length typdef) None in
+  let iter (loc, pinfo, e) =
+    if KerName.equal kn pinfo.pdata_type then
+      let index = pinfo.pdata_indx in
+      match args.(index) with
+      | None ->
+        let exp = subst_type (fun i -> GTypVar subst.(i)) pinfo.pdata_ptyp in
+        let e = intern_rec_with_constraint env e exp in
+        args.(index) <- Some e
+      | Some _ ->
+        let (name, _, _) = List.nth typdef pinfo.pdata_indx in
+        user_err ?loc (str "Field " ++ Id.print name ++ str " is defined \
+          several times")
+    else
+      user_err ?loc (str "Field " ++ (*KerName.print knp ++*) str " does not \
+        pertain to record definition " ++ pr_typref pinfo.pdata_type)
+  in
+  let () = List.iter iter fs in
+  let () = match Array.findi (fun _ o -> Option.is_empty o) args with
+  | None -> ()
+  | Some i ->
+    let (field, _, _) = List.nth typdef i in
+    user_err ~loc (str "Field " ++ Id.print field ++ str " is undefined")
+  in
+  let args = Array.map_to_list Option.get args in
+  let tparam = List.init params (fun i -> GTypVar subst.(i)) in
+  (GTacCst (GCaseAlg kn, 0, args), GTypRef (kn, tparam))
+
+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)
+  | CTydOpn -> (count, GTydOpn)
+
+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)
+
+(** Globalization *)
+
+let add_name accu = function
+| Name id -> Id.Set.add id accu
+| Anonymous -> accu
+
+let get_projection0 var = match var with
+| RelId (loc, qid) ->
+  let kn = try Tac2env.locate_projection qid with Not_found ->
+    user_err ?loc (pr_qualid qid ++ str " is not a projection")
+  in
+  kn
+| AbsKn kn -> kn
+
+let rec globalize ids e = match e with
+| CTacAtm _ -> e
+| CTacRef ref ->
+  let mem id = Id.Set.mem id ids in
+  begin match get_variable0 mem ref with
+  | ArgVar _ -> e
+  | ArgArg kn -> CTacRef (AbsKn kn)
+  end
+| CTacFun (loc, bnd, e) ->
+  let fold accu ((_, na), _) = add_name accu na in
+  let ids = List.fold_left fold ids bnd in
+  let e = globalize ids e in
+  CTacFun (loc, bnd, e)
+| CTacApp (loc, e, el) ->
+  let e = globalize ids e in
+  let el = List.map (fun e -> globalize ids e) el in
+  CTacApp (loc, e, el)
+| CTacLet (loc, isrec, bnd, e) ->
+  let fold accu ((_, na), _, _) = add_name accu na in
+  let ext = List.fold_left fold Id.Set.empty bnd in
+  let eids = Id.Set.union ext ids in
+  let e = globalize eids e in
+  let map (qid, t, e) =
+    let ids = if isrec then eids else ids in
+    (qid, t, globalize ids e)
+  in
+  let bnd = List.map map bnd in
+  CTacLet (loc, isrec, bnd, e)
+| CTacTup (loc, el) ->
+  let el = List.map (fun e -> globalize ids e) el in
+  CTacTup (loc, el)
+| CTacArr (loc, el) ->
+  let el = List.map (fun e -> globalize ids e) el in
+  CTacArr (loc, el)
+| CTacLst (loc, el) ->
+  let el = List.map (fun e -> globalize ids e) el in
+  CTacLst (loc, el)
+| CTacCnv (loc, e, t) ->
+  let e = globalize ids e in
+  CTacCnv (loc, e, t)
+| CTacSeq (loc, e1, e2) ->
+  let e1 = globalize ids e1 in
+  let e2 = globalize ids e2 in
+  CTacSeq (loc, e1, e2)
+| CTacCse (loc, e, bl) ->
+  let e = globalize ids e in
+  let bl = List.map (fun b -> globalize_case ids b) bl in
+  CTacCse (loc, e, bl)
+| CTacRec (loc, r) ->
+  let map (p, e) =
+    let p = get_projection0 p in
+    let e = globalize ids e in
+    (AbsKn p, e)
+  in
+  CTacRec (loc, List.map map r)
+| CTacPrj (loc, e, p) ->
+  let e = globalize ids e in
+  let p = get_projection0 p in
+  CTacPrj (loc, e, AbsKn p)
+| CTacSet (loc, e, p, e') ->
+  let e = globalize ids e in
+  let p = get_projection0 p in
+  let e' = globalize ids e' in
+  CTacSet (loc, e, AbsKn p, e')
+| CTacExt (loc, arg) ->
+  let arg = pr_argument_type (genarg_tag arg) in
+  CErrors.user_err ~loc (str "Cannot globalize generic arguments of type" ++ spc () ++ arg)
+
+and globalize_case ids (p, e) =
+  (globalize_pattern ids p, globalize ids e)
+
+and globalize_pattern ids p = match p with
+| CPatAny _ -> p
+| CPatRef (loc, cst, pl) ->
+  let cst = match get_constructor () cst with
+  | ArgVar _ -> cst
+  | ArgArg (_, knc) -> AbsKn knc
+  in
+  let pl = List.map (fun p -> globalize_pattern ids p) pl in
+  CPatRef (loc, cst, pl)
+| CPatTup (loc, pl) ->
+  let pl = List.map (fun p -> globalize_pattern ids p) pl in
+  CPatTup (loc, pl)
+
+(** 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)
+| GTacArr el ->
+  GTacArr (List.map (fun e -> subst_expr subst e) el)
+| GTacCst (t, n, el) as e0 ->
+  let t' = match t with
+  | GCaseAlg kn ->
+    let kn' = subst_kn subst kn in
+    if kn' == kn then t else GCaseAlg kn'
+  | GCaseTuple _ -> t
+  in
+  let el' = List.smartmap (fun e -> subst_expr subst e) el in
+  if t' == t && el' == el then e0 else GTacCst (t', n, 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')
+| GTacWth { opn_match = e; opn_branch = br; opn_default = (na, def) } as e0 ->
+  let e' = subst_expr subst e in
+  let def' = subst_expr subst def in
+  let fold kn (self, vars, p) accu =
+    let kn' = subst_kn subst kn in
+    let p' = subst_expr subst p in
+    if kn' == kn && p' == p then accu
+    else KNmap.add kn' (self, vars, p') (KNmap.remove kn accu)
+  in
+  let br' = KNmap.fold fold br br in
+  if e' == e && br' == br && def' == def then e0
+  else GTacWth { opn_match = e'; opn_default = (na, def'); opn_branch = br' }
+| GTacPrj (kn, e, p) as e0 ->
+  let kn' = subst_kn subst kn in
+  let e' = subst_expr subst e in
+  if kn' == kn && e' == e then e0 else GTacPrj (kn', e', p)
+| GTacSet (kn, e, p, r) as e0 ->
+  let kn' = subst_kn subst kn in
+  let e' = subst_expr subst e in
+  let r' = subst_expr subst r in
+  if kn' == kn && e' == e && r' == r then e0 else GTacSet (kn', e', p, r')
+| GTacExt ext ->
+  let ext' = Genintern.generic_substitute subst ext in
+  if ext' == ext then e else GTacExt ext'
+| GTacOpn (kn, el) as e0 ->
+  let kn' = subst_kn subst kn in
+  let el' = List.smartmap (fun e -> subst_expr subst e) el in
+  if kn' == kn && el' == el then e0 else GTacOpn (kn', el')
+
+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'
+| GTydOpn -> GTydOpn
+
+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')
+
+let subst_or_relid subst ref = match ref with
+| RelId _ -> ref
+| AbsKn kn ->
+  let kn' = subst_kn subst kn in
+  if kn' == kn then ref else AbsKn kn'
+
+let rec subst_rawtype subst t = match t with
+| CTypVar _ -> t
+| CTypArrow (loc, t1, t2) ->
+  let t1' = subst_rawtype subst t1 in
+  let t2' = subst_rawtype subst t2 in
+  if t1' == t1 && t2' == t2 then t else CTypArrow (loc, t1', t2')
+| CTypTuple (loc, tl) ->
+  let tl' = List.smartmap (fun t -> subst_rawtype subst t) tl in
+  if tl' == tl then t else CTypTuple (loc, tl')
+| CTypRef (loc, ref, tl) ->
+  let ref' = subst_or_relid subst ref in
+  let tl' = List.smartmap (fun t -> subst_rawtype subst t) tl in
+  if ref' == ref && tl' == tl then t else CTypRef (loc, ref', tl')
+
+let subst_tacref subst ref = match ref with
+| RelId _ -> ref
+| AbsKn (TacConstant kn) ->
+  let kn' = subst_kn subst kn in
+  if kn' == kn then ref else AbsKn (TacConstant kn')
+| AbsKn (TacConstructor kn) ->
+  let kn' = subst_kn subst kn in
+  if kn' == kn then ref else AbsKn (TacConstructor kn')
+
+let subst_projection subst prj = match prj with
+| RelId _ -> prj
+| AbsKn kn ->
+  let kn' = subst_kn subst kn in
+  if kn' == kn then prj else AbsKn kn'
+
+let rec subst_rawpattern subst p = match p with
+| CPatAny _ -> p
+| CPatRef (loc, c, pl) ->
+  let pl' = List.smartmap (fun p -> subst_rawpattern subst p) pl in
+  let c' = match c with
+  | RelId _ -> c
+  | AbsKn kn ->
+    let kn' = subst_kn subst kn in
+    if kn' == kn then c else AbsKn kn'
+  in
+  if pl' == pl && c' == c then p else CPatRef (loc, c', pl')
+| CPatTup (loc, pl) ->
+  let pl' = List.smartmap (fun p -> subst_rawpattern subst p) pl in
+  if pl' == pl then p else CPatTup (loc, pl')
+
+(** Used for notations *)
+let rec subst_rawexpr subst t = match t with
+| CTacAtm _ -> t
+| CTacRef ref ->
+  let ref' = subst_tacref subst ref in
+  if ref' == ref then t else CTacRef ref'
+| CTacFun (loc, bnd, e) ->
+  let map (na, t as p) =
+    let t' = Option.smartmap (fun t -> subst_rawtype subst t) t in
+    if t' == t then p else (na, t')
+  in
+  let bnd' = List.smartmap map bnd in
+  let e' = subst_rawexpr subst e in
+  if bnd' == bnd && e' == e then t else CTacFun (loc, bnd', e')
+| CTacApp (loc, e, el) ->
+  let e' = subst_rawexpr subst e in
+  let el' = List.smartmap (fun e -> subst_rawexpr subst e) el in
+  if e' == e && el' == el then t else CTacApp (loc, e', el')
+| CTacLet (loc, isrec, bnd, e) ->
+  let map (na, t, e as p) =
+    let t' = Option.smartmap (fun t -> subst_rawtype subst t) t in
+    let e' = subst_rawexpr subst e in
+    if t' == t && e' == e then p else (na, t', e')
+  in
+  let bnd' = List.smartmap map bnd in
+  let e' = subst_rawexpr subst e in
+  if bnd' == bnd && e' == e then t else CTacLet (loc, isrec, bnd', e')
+| CTacTup (loc, el) ->
+  let el' = List.smartmap (fun e -> subst_rawexpr subst e) el in
+  if el' == el then t else CTacTup (loc, el')
+| CTacArr (loc, el) ->
+  let el' = List.smartmap (fun e -> subst_rawexpr subst e) el in
+  if el' == el then t else CTacArr (loc, el')
+| CTacLst (loc, el) ->
+  let el' = List.smartmap (fun e -> subst_rawexpr subst e) el in
+  if el' == el then t else CTacLst (loc, el')
+| CTacCnv (loc, e, c) ->
+  let e' = subst_rawexpr subst e in
+  let c' = subst_rawtype subst c in
+  if c' == c && e' == e then t else CTacCnv (loc, e', c')
+| CTacSeq (loc, e1, e2) ->
+  let e1' = subst_rawexpr subst e1 in
+  let e2' = subst_rawexpr subst e2 in
+  if e1' == e1 && e2' == e2 then t else CTacSeq (loc, e1', e2')
+| CTacCse (loc, e, bl) ->
+  let map (p, e as x) =
+    let p' = subst_rawpattern subst p in
+    let e' = subst_rawexpr subst e in
+    if p' == p && e' == e then x else (p', e')
+  in
+  let e' = subst_rawexpr subst e in
+  let bl' = List.smartmap map bl in
+  if e' == e && bl' == bl then t else CTacCse (loc, e', bl')
+| CTacRec (loc, el) ->
+  let map (prj, e as p) =
+    let prj' = subst_projection subst prj in
+    let e' = subst_rawexpr subst e in
+    if prj' == prj && e' == e then p else (prj', e')
+  in
+  let el' = List.smartmap map el in
+  if el' == el then t else CTacRec (loc, el')
+| CTacPrj (loc, e, prj) ->
+    let prj' = subst_projection subst prj in
+    let e' = subst_rawexpr subst e in
+    if prj' == prj && e' == e then t else CTacPrj (loc, e', prj')
+| CTacSet (loc, e, prj, r) ->
+    let prj' = subst_projection subst prj in
+    let e' = subst_rawexpr subst e in
+    let r' = subst_rawexpr subst r in
+    if prj' == prj && e' == e && r' == r then t else CTacSet (loc, e', prj', r')
+| CTacExt _ -> assert false (** Should not be generated by gloabalization *)
+
+(** Registering *)
+
+let () =
+  let open Genintern in
+  let intern ist tac =
+    let env = match Genintern.Store.get ist.extra ltac2_env with
+    | None -> empty_env ()
+    | Some env -> env
+    in
+    let loc = loc_of_tacexpr tac in
+    let (tac, t) = intern_rec env tac in
+    let () = check_elt_unit loc env t in
+    (ist, tac)
+  in
+  Genintern.register_intern0 wit_ltac2 intern
+let () = Genintern.register_subst0 wit_ltac2 subst_expr
diff --git a/src/tac2intern.mli b/src/tac2intern.mli
new file mode 100644
index 0000000000..3d400a5cdd
--- /dev/null
+++ b/src/tac2intern.mli
@@ -0,0 +1,41 @@
+(************************************************************************)
+(*  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 subst_rawexpr : substitution -> raw_tacexpr -> raw_tacexpr
+
+(** {5 Notations} *)
+
+val globalize : Id.Set.t -> raw_tacexpr -> raw_tacexpr
+(** Replaces all qualified identifiers by their corresponding kernel name. The
+    set represents bound variables in the context. *)
+
+(** Errors *)
+
+val error_nargs_mismatch : Loc.t -> int -> int -> 'a
+val error_nparams_mismatch : Loc.t -> int -> int -> 'a
diff --git a/src/tac2interp.ml b/src/tac2interp.ml
new file mode 100644
index 0000000000..664b7de3d6
--- /dev/null
+++ b/src/tac2interp.ml
@@ -0,0 +1,160 @@
+(************************************************************************)
+(*  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 Util
+open Pp
+open CErrors
+open Genarg
+open Names
+open Proofview.Notations
+open Tac2expr
+
+exception LtacError of KerName.t * valexpr array
+
+let () = register_handler begin function
+| LtacError (kn, _) ->
+  let c = Tac2print.pr_constructor kn in
+  hov 0 (str "Uncaught Ltac2 exception:" ++ spc () ++ hov 0 c)
+| _ -> raise Unhandled
+end
+
+let val_exn = Geninterp.Val.create "ltac2:exn"
+
+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 pi2 (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 (Bytes.of_string 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 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
+| 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
+| GTacWth { opn_match = e; opn_branch = cse; opn_default = def } ->
+  interp ist e >>= fun e -> interp_with ist e cse def
+| GTacPrj (_, e, p) ->
+  interp ist e >>= fun e -> interp_proj ist e p
+| GTacSet (_, e, p, r) ->
+  interp ist e >>= fun e ->
+  interp ist r >>= fun r ->
+  interp_set ist e p r
+| GTacOpn (kn, el) ->
+  Proofview.Monad.List.map (fun e -> interp ist e) el >>= fun el ->
+  return (ValOpn (kn, Array.of_list el))
+| GTacPrm (ml, el) ->
+  Proofview.Monad.List.map (fun e -> interp ist e) el >>= fun el ->
+  Tac2env.interp_primitive ml el
+| GTacExt e ->
+  let GenArg (Glbwit tag, e) = e in
+  let tpe = Tac2env.interp_ml_object tag in
+  tpe.Tac2env.ml_interp ist e >>= fun e -> return (ValExt e)
+
+and interp_app 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 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 _ | ValOpn _ ->
+  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 _ | ValOpn _ ->
+  anomaly (str "Unexpected value shape")
+
+and interp_with ist e cse def = match e with
+| ValOpn (kn, args) ->
+  let br = try Some (KNmap.find kn cse) with Not_found -> None in
+  begin match br with
+  | None ->
+    let (self, def) = def in
+    let ist = push_name ist self e in
+    interp ist def
+  | Some (self, ids, p) ->
+    let ist = push_name ist self e in
+    let ist = CArray.fold_left2 push_name ist ids args in
+    interp ist p
+  end
+| ValInt _ | ValBlk _ | ValExt _ | ValStr _ | ValCls _ ->
+  anomaly (str "Unexpected value shape")
+
+and interp_proj ist e p = match e with
+| ValBlk (_, args) ->
+  return args.(p)
+| ValInt _ | ValExt _ | ValStr _ | ValCls _ | ValOpn _ ->
+  anomaly (str "Unexpected value shape")
+
+and interp_set ist e p r = match e with
+| ValBlk (_, args) ->
+  let () = args.(p) <- r in
+  return (ValInt 0)
+| ValInt _ | ValExt _ | ValStr _ | ValCls _ | ValOpn _ ->
+  anomaly (str "Unexpected value shape")
diff --git a/src/tac2interp.mli b/src/tac2interp.mli
new file mode 100644
index 0000000000..bf6b2d4dde
--- /dev/null
+++ b/src/tac2interp.mli
@@ -0,0 +1,28 @@
+(************************************************************************)
+(*  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
+
+type environment = valexpr Id.Map.t
+
+val empty_environment : environment
+
+val interp : environment -> glb_tacexpr -> valexpr Proofview.tactic
+
+val interp_app : valexpr -> valexpr list -> valexpr Proofview.tactic
+
+(** {5 Exceptions} *)
+
+exception LtacError of KerName.t * valexpr array
+(** Ltac2-defined exceptions seen from OCaml side *)
+
+val val_exn : Exninfo.iexn Geninterp.Val.typ
+(** Toplevel representation of OCaml exceptions. Invariant: no [LtacError]
+    should be put into a value with tag [val_exn]. *)
diff --git a/src/tac2print.ml b/src/tac2print.ml
new file mode 100644
index 0000000000..e6f0582e3d
--- /dev/null
+++ b/src/tac2print.ml
@@ -0,0 +1,296 @@
+(************************************************************************)
+(*  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 Util
+open Pp
+open Genarg
+open Names
+open Tac2expr
+open Tac2env
+
+(** Utils *)
+
+let change_kn_label kn id =
+  let (mp, dp, _) = KerName.repr kn in
+  KerName.make mp dp (Label.of_id id)
+
+let paren p = hov 2 (str "(" ++ p ++ str ")")
+
+(** Type printing *)
+
+type typ_level =
+| T5_l
+| T5_r
+| T2
+| T1
+| T0
+
+let pr_typref kn =
+  Libnames.pr_qualid (Tac2env.shortest_qualid_of_type kn)
+
+let pr_glbtype_gen pr lvl c =
+  let rec pr_glbtype lvl = function
+  | GTypVar n -> str "'" ++ str (pr n)
+  | GTypRef (kn, []) -> pr_typref kn
+  | GTypRef (kn, [t]) ->
+    let paren = match lvl with
+    | T5_r | T5_l | T2 | T1 -> fun x -> x
+    | T0 -> paren
+    in
+    paren (pr_glbtype lvl t ++ spc () ++ pr_typref kn)
+  | GTypRef (kn, tl) ->
+    let paren = match lvl with
+    | T5_r | T5_l | T2 | T1 -> fun x -> x
+    | T0 -> paren
+    in
+    paren (str "(" ++ prlist_with_sep (fun () -> str ", ") (pr_glbtype lvl) tl ++ str ")" ++ spc () ++ pr_typref kn)
+  | GTypArrow (t1, t2) ->
+    let paren = match lvl with
+    | T5_r -> fun x -> x
+    | T5_l | T2 | T1 | T0 -> paren
+    in
+    paren (pr_glbtype T5_l t1 ++ spc () ++ str "->" ++ spc () ++ pr_glbtype T5_r t2)
+  | GTypTuple tl ->
+    let paren = match lvl with
+    | T5_r | T5_l -> fun x -> x
+    | T2 | T1 | T0 -> paren
+    in
+    paren (prlist_with_sep (fun () -> str " * ") (pr_glbtype T2) tl)
+  in
+  hov 0 (pr_glbtype lvl c)
+
+let pr_glbtype pr c = pr_glbtype_gen pr T5_r c
+
+let int_name () =
+  let vars = ref Int.Map.empty in
+  fun n ->
+    if Int.Map.mem n !vars then Int.Map.find n !vars
+    else
+      let num = Int.Map.cardinal !vars in
+      let base = num mod 26 in
+      let rem = num / 26 in
+      let name = String.make 1 (Char.chr (97 + base)) in
+      let suff = if Int.equal rem 0 then "" else string_of_int rem in
+      let name = name ^ suff in
+      let () = vars := Int.Map.add n name !vars in
+      name
+
+(** Term printing *)
+
+let pr_constructor kn =
+  Libnames.pr_qualid (Tac2env.shortest_qualid_of_ltac (TacConstructor kn))
+
+let pr_projection kn =
+  Libnames.pr_qualid (Tac2env.shortest_qualid_of_projection kn)
+
+type exp_level = Tac2expr.exp_level =
+| E5
+| E4
+| E3
+| E2
+| E1
+| E0
+
+let pr_atom = function
+| AtmInt n -> int n
+| AtmStr s -> qstring s
+
+let pr_name = function
+| Name id -> Id.print id
+| Anonymous -> str "_"
+
+let find_constructor n empty def =
+  let rec find n = function
+  | [] -> assert false
+  | (id, []) :: rem ->
+    if empty then
+      if Int.equal n 0 then id
+      else find (pred n) rem
+    else find n rem
+  | (id, _ :: _) :: rem ->
+    if not empty then
+      if Int.equal n 0 then id
+      else find (pred n) rem
+    else find n rem
+  in
+  find n def
+
+let order_branches cbr nbr def =
+  let rec order cidx nidx def = match def with
+  | [] -> []
+  | (id, []) :: rem ->
+    let ans = order (succ cidx) nidx rem in
+    (id, [], cbr.(cidx)) :: ans
+  | (id, _ :: _) :: rem ->
+    let ans = order cidx (succ nidx) rem in
+    let (vars, e) = nbr.(nidx) in
+    (id, Array.to_list vars, e) :: ans
+  in
+  order 0 0 def
+
+let pr_glbexpr_gen lvl c =
+  let rec pr_glbexpr lvl = function
+  | GTacAtm atm -> pr_atom atm
+  | GTacVar id -> Id.print id
+  | GTacRef gr ->
+    let qid = shortest_qualid_of_ltac (TacConstant gr) in
+    Libnames.pr_qualid qid
+  | GTacFun (nas, c) ->
+    let nas = pr_sequence pr_name nas in
+    let paren = match lvl with
+    | E0 | E1 | E2 | E3 | E4 -> paren
+    | E5 -> fun x -> x
+    in
+    paren (str "fun" ++ spc () ++ nas ++ spc () ++ str "=>" ++ spc () ++
+      hov 0 (pr_glbexpr E5 c))
+  | GTacApp (c, cl) ->
+    let paren = match lvl with
+    | E0 -> paren
+    | E1 | E2 | E3 | E4 | E5 -> fun x -> x
+    in
+    paren (pr_glbexpr E1 c ++ spc () ++ (pr_sequence (pr_glbexpr E0) cl))
+  | GTacLet (mut, bnd, e) ->
+    let paren = match lvl with
+    | E0 | E1 | E2 | E3 | E4 -> paren
+    | E5 -> fun x -> x
+    in
+    let mut = if mut then str "rec" ++ spc () else mt () in
+    let pr_bnd (na, e) =
+      pr_name na ++ spc () ++ str ":=" ++ spc () ++ hov 2 (pr_glbexpr E5 e) ++ spc ()
+    in
+    let bnd = prlist_with_sep (fun () -> str "with" ++ spc ()) pr_bnd bnd in
+    paren (str "let" ++ spc () ++ mut ++ bnd ++ str "in" ++ spc () ++ pr_glbexpr E5 e)
+  | GTacCst (GCaseTuple _, _, cl) ->
+    let paren = match lvl with
+    | E0 | E1 -> paren
+    | E2 | E3 | E4 | E5 -> fun x -> x
+    in
+    paren (prlist_with_sep (fun () -> str "," ++ spc ()) (pr_glbexpr E1) cl)
+  | GTacArr cl ->
+    mt () (** FIXME when implemented *)
+  | GTacCst (GCaseAlg tpe, n, cl) ->
+    begin match Tac2env.interp_type tpe with
+    | _, GTydAlg def ->
+      let paren = match lvl with
+      | E0 -> paren
+      | E1 | E2 | E3 | E4 | E5 -> fun x -> x
+      in
+      let id = find_constructor n (List.is_empty cl) def in
+      let kn = change_kn_label tpe id in
+      let cl = match cl with
+      | [] -> mt ()
+      | _ -> spc () ++ pr_sequence (pr_glbexpr E0) cl
+      in
+      paren (pr_constructor kn ++ cl)
+    | _, GTydRec def ->
+      let args = List.combine def cl in
+      let pr_arg ((id, _, _), arg) =
+        let kn = change_kn_label tpe id in
+        pr_projection kn ++ spc () ++ str ":=" ++ spc () ++ pr_glbexpr E1 arg
+      in
+      let args = prlist_with_sep (fun () -> str ";" ++ spc ()) pr_arg args in
+      str "{" ++ spc () ++ args ++ spc () ++ str "}"
+    | _, (GTydDef _ | GTydOpn) -> assert false
+    end
+  | GTacCse (e, info, cst_br, ncst_br) ->
+    let e = pr_glbexpr E5 e in
+    let br = match info with
+    | GCaseAlg kn ->
+      let def = match Tac2env.interp_type kn with
+      | _, GTydAlg def -> def
+      | _, GTydDef _ | _, GTydRec _ | _, GTydOpn -> assert false
+      in
+      let br = order_branches cst_br ncst_br def in
+      let pr_branch (cstr, vars, p) =
+        let cstr = change_kn_label kn cstr in
+        let cstr = pr_constructor cstr in
+        let vars = match vars with
+        | [] -> mt ()
+        | _ -> spc () ++ pr_sequence pr_name vars
+        in
+        hov 0 (str "|" ++ spc () ++ cstr ++ vars ++ spc () ++ str "=>" ++ spc () ++
+          hov 2 (pr_glbexpr E5 p)) ++ spc ()
+      in
+      prlist pr_branch br
+    | GCaseTuple n ->
+      let (vars, p) = ncst_br.(0) in
+      let p = pr_glbexpr E5 p in
+      let vars = prvect_with_sep (fun () -> str "," ++ spc ()) pr_name vars in
+      str "|" ++ spc () ++ paren vars ++ spc () ++ str "=>" ++ spc () ++ p
+    in
+    hov 0 (hov 0 (str "match" ++ spc () ++ e ++ spc () ++ str "with") ++ spc () ++ Pp.v 0 br ++ str "end")
+  | GTacWth wth ->
+    let e = pr_glbexpr E5 wth.opn_match in
+    let pr_pattern c self vars p =
+      let self = match self with
+      | Anonymous -> mt ()
+      | Name id -> spc () ++ str "as" ++ spc () ++ Id.print id
+      in
+      hov 0 (str "|" ++ spc () ++ c ++ vars ++ self ++ spc () ++ str "=>" ++ spc () ++
+        hov 2 (pr_glbexpr E5 p)) ++ spc ()
+    in
+    let pr_branch (cstr, (self, vars, p)) =
+      let cstr = pr_constructor cstr in
+      let vars = match Array.to_list vars with
+      | [] -> mt ()
+      | vars -> spc () ++ pr_sequence pr_name vars
+      in
+      pr_pattern cstr self vars p
+    in
+    let br = prlist pr_branch (KNmap.bindings wth.opn_branch) in
+    let (def_as, def_p) = wth.opn_default in
+    let def = pr_pattern (str "_") def_as (mt ()) def_p in
+    let br = br ++ def in
+    hov 0 (hov 0 (str "match" ++ spc () ++ e ++ spc () ++ str "with") ++ spc () ++ Pp.v 0 br ++ str "end")
+  | GTacPrj (kn, e, n) ->
+    let def = match Tac2env.interp_type kn with
+    | _, GTydRec def -> def
+    | _, GTydDef _ | _, GTydAlg _ | _, GTydOpn -> assert false
+    in
+    let (proj, _, _) = List.nth def n in
+    let proj = change_kn_label kn proj in
+    let proj = pr_projection proj in
+    let e = pr_glbexpr E0 e in
+    e ++ str "." ++ paren proj
+  | GTacSet (kn, e, n, r) ->
+    let def = match Tac2env.interp_type kn with
+    | _, GTydRec def -> def
+    | _, GTydDef _ | _, GTydAlg _ | _, GTydOpn -> assert false
+    in
+    let (proj, _, _) = List.nth def n in
+    let proj = change_kn_label kn proj in
+    let proj = pr_projection proj in
+    let e = pr_glbexpr E0 e in
+    let r = pr_glbexpr E1 r in
+    e ++ str "." ++ paren proj ++ spc () ++ str ":=" ++ spc () ++ r
+  | GTacOpn (kn, cl) ->
+    let paren = match lvl with
+    | E0 -> paren
+    | E1 | E2 | E3 | E4 | E5 -> fun x -> x
+    in
+    let c = pr_constructor kn in
+    paren (c ++ spc () ++ (pr_sequence (pr_glbexpr E0) cl))
+  | GTacExt arg ->
+    let GenArg (Glbwit tag, arg) = arg in
+    let name = match tag with
+    | ExtraArg tag -> ArgT.repr tag
+    | _ -> assert false
+    in
+    str name ++ str ":" ++ paren (Genprint.glb_print tag arg)
+  | GTacPrm (prm, args) ->
+    let args = match args with
+    | [] -> mt ()
+    | _ -> spc () ++ pr_sequence (pr_glbexpr E0) args
+    in
+    str "@external" ++ spc () ++ qstring prm.mltac_plugin ++ spc () ++
+      qstring prm.mltac_tactic ++ args
+  in
+  hov 0 (pr_glbexpr lvl c)
+
+let pr_glbexpr c =
+  pr_glbexpr_gen E5 c
diff --git a/src/tac2print.mli b/src/tac2print.mli
new file mode 100644
index 0000000000..ddd599641d
--- /dev/null
+++ b/src/tac2print.mli
@@ -0,0 +1,37 @@
+(************************************************************************)
+(*  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 Names
+open Tac2expr
+
+(** {5 Printing types} *)
+
+type typ_level =
+| T5_l
+| T5_r
+| T2
+| T1
+| T0
+
+val pr_typref : type_constant -> std_ppcmds
+val pr_glbtype_gen : ('a -> string) -> typ_level -> 'a glb_typexpr -> std_ppcmds
+val pr_glbtype : ('a -> string) -> 'a glb_typexpr -> std_ppcmds
+
+(** {5 Printing expressions} *)
+
+val pr_constructor : ltac_constructor -> std_ppcmds
+val pr_projection : ltac_projection -> std_ppcmds
+val pr_glbexpr_gen : exp_level -> glb_tacexpr -> std_ppcmds
+val pr_glbexpr : glb_tacexpr -> std_ppcmds
+
+(** {5 Utilities} *)
+
+val int_name : unit -> (int -> string)
+(** Create a function that give names to integers. The names are generated on
+    the fly, in the order they are encountered. *)