aboutsummaryrefslogtreecommitdiff
path: root/engine/uState.mli
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2020-09-01 11:51:41 +0200
committerPierre-Marie Pédrot2020-09-01 11:51:41 +0200
commit0d30f79268fea18ef99c040a859956f61c3d978a (patch)
tree26694ab196e67dde80cc8489236770bda59a061c /engine/uState.mli
parent46768229c5349aa92a8107cd0a6ded32fd22d768 (diff)
parent576c1153dae2b3660d35127862aeb3d528eb6d8d (diff)
Merge PR #12892: Update update_global_env usage
Reviewed-by: ejgallego Reviewed-by: gares Reviewed-by: ppedrot
Diffstat (limited to 'engine/uState.mli')
-rw-r--r--engine/uState.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/uState.mli b/engine/uState.mli
index 607c6c9452..7fec03e3b2 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -185,7 +185,7 @@ val check_mono_univ_decl : t -> universe_decl -> Univ.ContextSet.t
(** {5 TODO: Document me} *)
-val update_sigma_env : t -> Environ.env -> t
+val update_sigma_univs : t -> UGraph.t -> t
(** {5 Pretty-printing} *)