diff options
| author | Gaëtan Gilbert | 2018-10-10 13:37:46 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-10-16 15:52:52 +0200 |
| commit | 5bf063c15468bb81f0f48b583f600250cd829aee (patch) | |
| tree | 69e33cf3dd53ab18b8a359d0c2ab6f0041dc9abd /engine/univGen.mli | |
| parent | 404291584e861cc0f41a5585280143d2df78bd26 (diff) | |
UnivGen.constr_of_glob_univ -> Constr.mkRef
Diffstat (limited to 'engine/univGen.mli')
| -rw-r--r-- | engine/univGen.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/engine/univGen.mli b/engine/univGen.mli index 4cfbb94775..82ec9f3e64 100644 --- a/engine/univGen.mli +++ b/engine/univGen.mli @@ -63,6 +63,7 @@ val fresh_universe_context_set_instance : ContextSet.t -> val global_of_constr : constr -> GlobRef.t puniverses val constr_of_global_univ : GlobRef.t puniverses -> constr +[@@ocaml.deprecated "Use [Constr.mkRef]"] val extend_context : 'a in_universe_context_set -> ContextSet.t -> 'a in_universe_context_set |