Fixing a precedence issue in type parameters.

19 files changed, 556 insertions, 96 deletions

diff --git a/Array.v b/Array.v
new file mode 100644
index 0000000000..be4ab025ae
--- /dev/null
+++ b/Array.v
@@ -0,0 +1,14 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+Require Import Coq.ltac2.Init.
+
+Ltac2 @external make : int -> 'a -> 'a array := "ltac2" "array_make".
+Ltac2 @external length : 'a array -> int := "ltac2" "array_length".
+Ltac2 @external get : 'a array -> int -> 'a := "ltac2" "array_get".
+Ltac2 @external set : 'a array -> int -> 'a -> unit := "ltac2" "array_set".
diff --git a/Constr.v b/Constr.v
new file mode 100644
index 0000000000..994f9bf3ac
--- /dev/null
+++ b/Constr.v
@@ -0,0 +1,9 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+Require Import Coq.ltac2.Init.
diff --git a/Control.v b/Control.v
new file mode 100644
index 0000000000..a476513ede
--- /dev/null
+++ b/Control.v
@@ -0,0 +1,44 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+Require Import Coq.ltac2.Init.
+
+(** Panic *)
+
+Ltac2 @ external throw : exn -> 'a := "ltac2" "throw".
+(** Fatal exception throwing. This does not induce backtracking. *)
+
+(** Generic backtracking control *)
+
+Ltac2 @ external zero : exn -> 'a := "ltac2" "zero".
+Ltac2 @ external plus : (unit -> 'a) -> (exn -> 'a) -> 'a := "ltac2" "plus".
+Ltac2 @ external once : (unit -> 'a) -> 'a := "ltac2" "once".
+Ltac2 @ external dispatch : (unit -> unit) list -> unit := "ltac2" "dispatch".
+Ltac2 @ external extend : (unit -> unit) list -> (unit -> unit) -> (unit -> unit) list -> unit := "ltac2" "extend".
+Ltac2 @ external enter : (unit -> unit) -> unit := "ltac2" "enter".
+
+(** Proof state manipulation *)
+
+Ltac2 @ external focus : int -> int -> (unit -> 'a) -> 'a := "ltac2" "focus".
+Ltac2 @ external shelve : unit -> unit := "ltac2" "shelve".
+Ltac2 @ external shelve_unifiable : unit -> unit := "ltac2" "shelve_unifiable".
+
+(** Goal inspection *)
+
+Ltac2 @ external goal : unit -> constr := "ltac2" "goal".
+(** Panics if there is not exactly one goal under focus. Otherwise returns
+    the conclusion of this goal. *)
+
+Ltac2 @ external hyp : ident -> constr := "ltac2" "hyp".
+(** Panics if there is more than one goal under focus. If there is no
+    goal under focus, looks for the section variable with the given name.
+    If there is one, looks for the hypothesis with the given name. *)
+
+(** Refinement *)
+
+Ltac2 @ external refine : (unit -> constr) -> unit := "ltac2" "refine".
diff --git a/Init.v b/Init.v
new file mode 100644
index 0000000000..0f0b4636d8
--- /dev/null
+++ b/Init.v
@@ -0,0 +1,32 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+Declare ML Module "ltac2_plugin".
+
+Global Set Default Proof Mode "Ltac2".
+
+(** Primitive types *)
+
+Ltac2 Type int.
+Ltac2 Type string.
+Ltac2 Type char.
+
+Ltac2 Type evar.
+Ltac2 Type constr.
+Ltac2 Type ident.
+Ltac2 Type message.
+Ltac2 Type exn.
+Ltac2 Type 'a array.
+
+(** Pervasive types *)
+
+Ltac2 Type 'a option := [ None | Some ('a) ].
+
+Ltac2 Type 'a ref := { mutable contents : 'a }.
+
+Ltac2 Type bool := [ true | false ].
diff --git a/Int.v b/Int.v
new file mode 100644
index 0000000000..bb0287efc8
--- /dev/null
+++ b/Int.v
@@ -0,0 +1,16 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+Require Import Coq.ltac2.Init.
+
+Ltac2 @ external equal : int -> int -> bool := "ltac2" "int_equal".
+Ltac2 @ external compare : int -> int -> int := "ltac2" "int_compare".
+Ltac2 @ external add : int -> int -> int := "ltac2" "int_add".
+Ltac2 @ external sub : int -> int -> int := "ltac2" "int_sub".
+Ltac2 @ external mul : int -> int -> int := "ltac2" "int_mul".
+Ltac2 @ external neg : int -> int := "ltac2" "int_neg".
diff --git a/Ltac2.v b/Ltac2.v
index 0933c1e0b4..625d4ac513 100644
--- a/Ltac2.v
+++ b/Ltac2.v
@@ -6,37 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Declare ML Module "ltac2_plugin".
-
-Global Set Default Proof Mode "Ltac2".
-
-(** Primitive types *)
-
-Ltac2 Type int.
-Ltac2 Type string.
-Ltac2 Type constr.
-Ltac2 Type message.
-Ltac2 Type 'a array.
-
-(** Pervasive types *)
-
-Ltac2 Type 'a option := [ None | Some ('a) ].
-
-(** Primitive tactics *)
-
-Module Message.
-
-Ltac2 @ external print : message -> unit := "ltac2" "print".
-Ltac2 @ external of_string : string -> message := "ltac2" "message_of_string".
-Ltac2 @ external of_int : int -> message := "ltac2" "message_of_int".
-
-End Message.
-
-Module Array.
-
-Ltac2 @external make : int -> 'a -> ('a) array := "ltac2" "array_make".
-Ltac2 @external length : ('a) array -> int := "ltac2" "array_length".
-Ltac2 @external get : ('a) array -> int -> 'a := "ltac2" "array_get".
-Ltac2 @external set : ('a) array -> int -> 'a -> unit := "ltac2" "array_set".
-
-End Array.
+Require Export Coq.ltac2.Init.
+
+Require Coq.ltac2.Int.
+Require Coq.ltac2.String.
+Require Coq.ltac2.Array.
+Require Coq.ltac2.Message.
+Require Coq.ltac2.Constr.
+Require Coq.ltac2.Control.
diff --git a/Message.v b/Message.v
new file mode 100644
index 0000000000..36233f4544
--- /dev/null
+++ b/Message.v
@@ -0,0 +1,20 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+Require Import Coq.ltac2.Init.
+
+Ltac2 @ external print : message -> unit := "ltac2" "print".
+
+Ltac2 @ external of_string : string -> message := "ltac2" "message_of_string".
+
+Ltac2 @ external of_int : int -> message := "ltac2" "message_of_int".
+
+Ltac2 @ external of_constr : constr -> message := "ltac2" "message_of_constr".
+(** Panics if there is more than one goal under focus. *)
+
+Ltac2 @ external concat : message -> message -> message := "ltac2" "message_concat".
diff --git a/String.v b/String.v
new file mode 100644
index 0000000000..3a4a178878
--- /dev/null
+++ b/String.v
@@ -0,0 +1,14 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+Require Import Coq.ltac2.Init.
+
+Ltac2 @external make : int -> char -> string := "ltac2" "string_make".
+Ltac2 @external length : string -> int := "ltac2" "string_length".
+Ltac2 @external get : string -> int -> char := "ltac2" "string_get".
+Ltac2 @external set : string -> int -> char -> unit := "ltac2" "string_set".
diff --git a/g_ltac2.ml4 b/g_ltac2.ml4
index ce2becd9f9..ff3d79bbae 100644
--- a/g_ltac2.ml4
+++ b/g_ltac2.ml4
@@ -23,6 +23,8 @@ 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;
@@ -84,6 +86,8 @@ GEXTEND Gram
       | s = Prim.string -> CTacAtm (!@loc, AtmStr s)
       | id = Prim.qualid -> CTacRef 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:
@@ -97,13 +101,15 @@ GEXTEND Gram
       [ t1 = tac2type; "->"; t2 = tac2type -> CTypArrow (!@loc, t1, t2) ]
     | "2"
       [ t = tac2type; "*"; tl = LIST1 tac2type SEP "*" -> CTypTuple (!@loc, t :: tl) ]
-    | "1"
-      [ "("; p = LIST1 tac2type LEVEL "5" SEP ","; ")"; qid = Prim.qualid -> CTypRef (!@loc, qid, p) ]
+    | "1" LEFTA
+      [ t = SELF; qid = Prim.qualid -> CTypRef (!@loc, qid, [t]) ]
     | "0"
-      [ "("; t = tac2type; ")"  -> t
+      [ "("; t = tac2type LEVEL "5"; ")"  -> t
       | id = typ_param -> CTypVar (!@loc, Name id)
       | "_" -> CTypVar (!@loc, Anonymous)
-      | qid = Prim.qualid -> CTypRef (!@loc, qid, []) ]
+      | qid = Prim.qualid -> CTypRef (!@loc, qid, [])
+      | "("; p = LIST1 tac2type LEVEL "5" SEP ","; ")"; qid = Prim.qualid ->
+        CTypRef (!@loc, qid, p) ]
     ];
   locident:
     [ [ id = Prim.ident -> (!@loc, id) ] ]
diff --git a/tac2core.ml b/tac2core.ml
index 95632bf7b1..fd998151fd 100644
--- a/tac2core.ml
+++ b/tac2core.ml
@@ -14,12 +14,25 @@ open Genarg
 open Geninterp
 open Tac2env
 open Tac2expr
+open Tac2interp
 open Proofview.Notations
 
 (** Standard values *)
 
-let coq_prefix = DirPath.make (List.map Id.of_string ["Ltac2"; "ltac2"; "Coq"])
-let coq_core n = KerName.make2 (MPfile coq_prefix) (Label.of_id (Id.of_string_soft n))
+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
@@ -30,6 +43,7 @@ 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 c_nil = coq_core "[]"
 let c_cons = coq_core "::"
@@ -51,6 +65,28 @@ 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)
@@ -60,20 +96,33 @@ let rec to_list = function
 | ValBlk (0, [|v; vl|]) -> v :: to_list vl
 | _ -> assert false
 
-end
+let of_ext tag c =
+  ValExt (Val.Dyn (tag, c))
 
-let extract_val (type a) (tag : a Val.typ) (Val.Dyn (tag', v)) : a =
-match Val.eq tag tag' with
-| None -> assert false
-| Some Refl -> v
+let to_ext tag = function
+| ValExt e -> extract_val tag e
+| _ -> assert false
 
-let val_pp = Val.create "ltac2:pp"
-let get_pp v = extract_val val_pp v
+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
+
+let of_exn c = of_ext val_exn c
+let to_exn c = 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"
 
 (** Helper functions *)
 
+let thaw f = interp_app f [v_unit]
+
 let return x = Proofview.tclUNIT x
 let pname s = { mltac_plugin = "ltac2"; mltac_tactic = s }
 
@@ -83,10 +132,35 @@ let wrap f =
 let wrap_unit f =
   return () >>= fun () -> f (); return v_unit
 
+(** In Ltac2, the notion of "current environment" only makes sense when there is
+    at most one goal under focus. Contrarily to Ltac1, instead of dynamically
+    focussing when we need it, we raise a non-backtracking error when it does
+    not make sense. *)
+exception NonFocussedGoal
+
+let () = register_handler begin function
+| NonFocussedGoal -> str "Several goals under focus"
+| _ -> raise Unhandled
+end
+
+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)
+  | _ :: _ :: _ ->
+    Proofview.tclLIFT (Proofview.NonLogical.raise NonFocussedGoal)
+
 (** Primitives *)
 
+(** Printing *)
+
 let prm_print : ml_tactic = function
-| [ValExt pp] -> wrap_unit (fun () -> Feedback.msg_notice (get_pp pp))
+| [pp] -> wrap_unit (fun () -> Feedback.msg_notice (Value.to_pp pp))
 | _ -> assert false
 
 let prm_message_of_int : ml_tactic = function
@@ -94,11 +168,31 @@ let prm_message_of_int : ml_tactic = function
 | _ -> assert false
 
 let prm_message_of_string : ml_tactic = function
-| [ValStr s] -> return (ValExt (Val.Dyn (val_pp, str s)))
+| [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] -> wrap (fun () -> ValBlk (0, Array.make n x))
+| [ValInt n; x] ->
+  (** FIXME: wrap exception *)
+  wrap (fun () -> ValBlk (0, Array.make n x))
 | _ -> assert false
 
 let prm_array_length : ml_tactic = function
@@ -106,31 +200,214 @@ let prm_array_length : ml_tactic = function
 | _ -> assert false
 
 let prm_array_set : ml_tactic = function
-| [ValBlk (_, v); ValInt n; x] -> wrap_unit (fun () -> v.(n) <- x)
+| [ValBlk (_, v); ValInt n; x] ->
+  (** FIXME: wrap exception *)
+  wrap_unit (fun () -> v.(n) <- x)
 | _ -> assert false
 
 let prm_array_get : ml_tactic = function
-| [ValBlk (_, v); ValInt n] -> wrap (fun () -> v.(n))
+| [ValBlk (_, v); ValInt n] ->
+  (** FIXME: wrap exception *)
+  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
+  (** FIXME: wrap exception *)
+  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
+  (** FIXME: wrap exception *)
+  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
+  (** FIXME: wrap exception *)
+  wrap (fun () -> Value.of_char (Bytes.get s n))
+| _ -> 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
+
+(** unit -> constr *)
+let prm_goal : ml_tactic = function
+| [_] ->
+  Proofview.Goal.enter_one { enter = fun gl ->
+    let concl = Tacmach.New.pf_nf_concl gl in
+    return (Value.of_constr concl)
+  }
+| _ -> 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 { enter = fun gl ->
+    Refine.generic_refine ~unsafe:false c gl
+  } >>= 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
 
-(** ML types *)
+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 "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 "goal") prm_goal
+let () = Tac2env.define_primitive (pname "hyp") prm_hyp
+let () = Tac2env.define_primitive (pname "refine") prm_refine
 
-let val_tag t = match val_tag t with
-| Val.Base t -> t
-| _ -> assert false
-
-let tag_constr = val_tag (topwit Stdarg.wit_constr)
+(** ML types *)
 
 let constr_flags () =
   let open Pretyping in
@@ -142,28 +419,15 @@ let constr_flags () =
     expand_evars = true
   }
 
-(** In Ltac2, the notion of "current environment" only makes sense when there is
-    at most one goal under focus. Contrarily to Ltac1, instead of dynamically
-    focussing when we need it, we raise a non-backtracking error when it does
-    not make sense. *)
-exception NonFocussedGoal
-
-let () = register_handler begin function
-| NonFocussedGoal -> str "Several goals under focus"
-| _ -> raise Unhandled
-end
-
-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)
-  | _ :: _ :: _ ->
-    Proofview.tclLIFT (Proofview.NonLogical.raise NonFocussedGoal)
+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 =
@@ -172,17 +436,40 @@ let to_lvar ist =
   let lfun = Id.Map.map map ist in
   { empty_lvar with ltac_genargs = lfun }
 
-let () =
+let interp_constr flags ist (c, _) =
   let open Pretyping in
-  let interp ist (c, _) = pf_apply begin fun env sigma ->
+  pf_apply begin fun env sigma ->
+  Proofview.V82.wrap_exceptions begin fun () ->
     let ist = to_lvar ist in
-    let (sigma, c) = understand_ltac (constr_flags ()) env sigma ist WithoutTypeConstraint c in
-    let c = Val.Dyn (tag_constr, c) 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 in
+  end
+  end
+
+let () =
+  let open Pretyping in
+  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 open Pretyping in
+  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
diff --git a/tac2core.mli b/tac2core.mli
index 14bde483c1..27144bc6e2 100644
--- a/tac2core.mli
+++ b/tac2core.mli
@@ -22,13 +22,32 @@ 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
+
 end
diff --git a/tac2entries.ml b/tac2entries.ml
index 4098324f12..93ad0ceb0b 100644
--- a/tac2entries.ml
+++ b/tac2entries.ml
@@ -338,8 +338,7 @@ let register_prim_alg name params def =
   let def = { typdef_local = false; typdef_expr = def } in
   ignore (Lib.add_leaf id (inTypDef def))
 
-let coq_prefix = DirPath.make (List.map Id.of_string ["Ltac2"; "ltac2"; "Coq"])
-let coq_def n = KerName.make2 (MPfile coq_prefix) (Label.make n)
+let coq_def n = KerName.make2 Tac2env.coq_prefix (Label.make n)
 
 let t_list = coq_def "list"
 
diff --git a/tac2env.ml b/tac2env.ml
index bdb8f41ef8..17c70d2e44 100644
--- a/tac2env.ml
+++ b/tac2env.ml
@@ -203,3 +203,8 @@ 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"]))
diff --git a/tac2env.mli b/tac2env.mli
index bcfa70487a..96174e8c92 100644
--- a/tac2env.mli
+++ b/tac2env.mli
@@ -95,3 +95,8 @@ type 'a ml_object = {
 
 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. *)
diff --git a/tac2expr.mli b/tac2expr.mli
index b9b649e481..c3c1e56dea 100644
--- a/tac2expr.mli
+++ b/tac2expr.mli
@@ -131,7 +131,7 @@ type valexpr =
   (** Immediate integers *)
 | ValBlk of tag * valexpr array
   (** Structured blocks *)
-| ValStr of string
+| ValStr of Bytes.t
   (** Strings *)
 | ValCls of closure
   (** Closures *)
diff --git a/tac2intern.ml b/tac2intern.ml
index 10fcde6efa..23f8325da8 100644
--- a/tac2intern.ml
+++ b/tac2intern.ml
@@ -18,8 +18,7 @@ open Tac2expr
 
 (** Hardwired types and constants *)
 
-let coq_prefix = DirPath.make (List.map Id.of_string ["Ltac2"; "ltac2"; "Coq"])
-let coq_type n = KerName.make2 (MPfile coq_prefix) (Label.make n)
+let coq_type n = KerName.make2 Tac2env.coq_prefix (Label.make n)
 
 let t_int = coq_type "int"
 let t_string = coq_type "string"
diff --git a/tac2interp.ml b/tac2interp.ml
index fedbb13e7d..d508b0c967 100644
--- a/tac2interp.ml
+++ b/tac2interp.ml
@@ -15,6 +15,8 @@ open Tac2expr
 
 exception LtacError of KerName.t * valexpr
 
+let val_exn = Geninterp.Val.create "ltac2:exn"
+
 type environment = valexpr Id.Map.t
 
 let empty_environment = Id.Map.empty
@@ -35,7 +37,7 @@ let return = Proofview.tclUNIT
 
 let rec interp ist = function
 | GTacAtm (AtmInt n) -> return (ValInt n)
-| GTacAtm (AtmStr s) -> return (ValStr s)
+| 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) ->
@@ -44,7 +46,7 @@ let rec interp ist = function
 | GTacApp (f, args) ->
   interp ist f >>= fun f ->
   Proofview.Monad.List.map (fun e -> interp ist e) args >>= fun args ->
-  interp_app ist f args
+  interp_app f args
 | GTacLet (false, el, e) ->
   let fold accu (na, e) =
     interp ist e >>= fun e ->
@@ -94,11 +96,11 @@ let rec interp ist = function
   let tpe = Tac2env.interp_ml_object tag in
   tpe.Tac2env.ml_interp ist e >>= fun e -> return (ValExt e)
 
-and interp_app ist f args = match f with
+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 ist f args
+  | [], _ :: _ -> interp ist e >>= fun f -> interp_app f args
   | _ :: _, [] ->
     let cls = { clos_env = ist; clos_var = ids; clos_exp = e } in
     return (ValCls cls)
diff --git a/tac2interp.mli b/tac2interp.mli
index b11ee36012..7fe78a9460 100644
--- a/tac2interp.mli
+++ b/tac2interp.mli
@@ -10,10 +10,18 @@ open Genarg
 open Names
 open Tac2expr
 
-exception LtacError of KerName.t * valexpr
-
 type environment = valexpr Id.Map.t
 
 val empty_environment : environment
 
 val interp : environment -> glb_tacexpr -> valexpr Proofview.tactic
+
+val interp_app : valexpr -> valexpr list -> valexpr Proofview.tactic
+
+(** {5 Exceptions} *)
+
+exception LtacError of KerName.t * valexpr
+(** Ltac2-defined exceptions *)
+
+val val_exn : Exninfo.iexn Geninterp.Val.typ
+(** Toplevel representation of Ltac2 exceptions *)
diff --git a/vo.itarget b/vo.itarget
index 776404ad79..5777585681 100644
--- a/vo.itarget
+++ b/vo.itarget
@@ -1 +1,8 @@
+Init.vo
+Int.vo
+String.vo
+Array.vo
+Control.vo
+Message.vo
+Constr.vo
 Ltac2.vo