diff options
| -rw-r--r-- | src/tac2core.ml | 8 | ||||
| -rw-r--r-- | theories/Env.v | 5 |
2 files changed, 13 insertions, 0 deletions
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. *) |