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 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'src')

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 () =
-- 
cgit v1.2.3