aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/assumptions.mli
diff options
context:
space:
mode:
Diffstat (limited to 'library/assumptions.mli')
-rw-r--r--library/assumptions.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/library/assumptions.mli b/library/assumptions.mli
index e5d2a977c..f91412013 100644
--- a/library/assumptions.mli
+++ b/library/assumptions.mli
@@ -13,7 +13,7 @@ open Environ
(** A few declarations for the "Print Assumption" command
@author spiwack *)
type context_object =
- | Variable of identifier (** A section variable or a Let definition *)
+ | Variable of Id.t (** A section variable or a Let definition *)
| Axiom of constant (** An axiom or a constant. *)
| Opaque of constant (** An opaque constant. *)
| Transparent of constant (** A transparent constant *)