3 files changed, 30 insertions, 0 deletions
diff --git a/theories/Constr.v b/theories/Constr.v
index 072c613920..d8d222730e 100644
--- a/theories/Constr.v
+++ b/theories/Constr.v
@@ -57,6 +57,13 @@ Ltac2 @ external closenl : ident list -> int -> constr -> constr := "ltac2" "con
 (** [closenl [x₁;...;xₙ] k c] abstracts over variables [x₁;...;xₙ] and replaces them with
     [Rel(k); ...; Rel(k+n-1)] in [c]. If two names are identical, the one of least index is kept. *)
 
+Ltac2 @ external case : inductive -> case := "ltac2" "constr_case".
+(** Generate the case information for a given inductive type. *)
+
+Ltac2 @ external constructor : inductive -> int -> constructor := "ltac2" "constr_constructor".
+(** Generate the i-th constructor for a given inductive type. Indexing starts
+    at 0. Panics if there is no such constructor. *)
+
 End Unsafe.
 
 Ltac2 @ external in_context : ident -> constr -> (unit -> unit) -> constr := "ltac2" "constr_in_context".
diff --git a/theories/Env.v b/theories/Env.v
new file mode 100644
index 0000000000..7e36aa7990
--- /dev/null
+++ b/theories/Env.v
@@ -0,0 +1,22 @@
+(************************************************************************)
+(*  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 Ltac2.Init.
+Require Import Std.
+
+Ltac2 @ external get : ident list -> Std.reference option := "ltac2" "env_get".
+(** Returns the global reference corresponding to the absolute name given as
+    argument if it exists. *)
+
+Ltac2 @ external expand : ident list -> Std.reference list := "ltac2" "env_expand".
+(** Returns the list of all global references whose absolute name contains
+    the argument list as a prefix. *)
+
+Ltac2 @ external path : Std.reference -> ident list := "ltac2" "env_path".
+(** Returns the absolute name of the given reference. Panics if the reference
+    does not exist. *)
diff --git a/theories/Ltac2.v b/theories/Ltac2.v
index 7b2f592ac6..3fe71f4c65 100644
--- a/theories/Ltac2.v
+++ b/theories/Ltac2.v
@@ -18,4 +18,5 @@ Require Ltac2.Control.
 Require Ltac2.Fresh.
 Require Ltac2.Pattern.
 Require Ltac2.Std.
+Require Ltac2.Env.
 Require Export Ltac2.Notations.