diff options
| author | Pierre-Marie Pédrot | 2018-11-19 10:00:50 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-19 10:05:50 +0100 |
| commit | 93300e662b6e7571619508e6f6d47b963d5300d1 (patch) | |
| tree | 16af6107831d3dad62f141d88a69181ff9e08918 | |
| parent | 3ba8647971c441307dd61bc67dc2c3705b345b56 (diff) | |
Add a function to generate fresh reference instances.
| -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. *) |