From 93300e662b6e7571619508e6f6d47b963d5300d1 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 19 Nov 2018 10:00:50 +0100
Subject: Add a function to generate fresh reference instances.

---
 src/tac2core.ml | 8 ++++++++
 theories/Env.v  | 5 +++++
 2 files changed, 13 insertions(+)

diff --git a/src/tac2core.ml b/src/tac2core.ml
index b6983ed869..890062a6d1 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -867,6 +867,14 @@ let () = define1 "env_path" reference begin fun r ->
     throw err_notfound
 end
 
+let () = define1 "env_instantiate" reference begin fun r ->
+  Proofview.tclENV >>= fun env ->
+  Proofview.tclEVARMAP >>= fun sigma ->
+  let (sigma, c) = Evd.fresh_global env sigma r in
+  Proofview.Unsafe.tclEVARS sigma >>= fun () ->
+  return (Value.of_constr c)
+end
+
 (** ML types *)
 
 let constr_flags () =
diff --git a/theories/Env.v b/theories/Env.v
index 7e36aa7990..c9b250f4ba 100644
--- a/theories/Env.v
+++ b/theories/Env.v
@@ -20,3 +20,8 @@ Ltac2 @ external expand : ident list -> Std.reference list := "ltac2" "env_expan
 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. *)
+
+Ltac2 @ external instantiate : Std.reference -> constr := "ltac2" "env_instantiate".
+(** Returns a fresh instance of the corresponding reference, in particular
+    generating fresh universe variables and constraints when this reference is
+    universe-polymorphic. *)
-- 
cgit v1.2.3