aboutsummaryrefslogtreecommitdiff
path: root/user-contrib
diff options
context:
space:
mode:
authorSamuel Gruetter2021-03-23 15:59:48 -0400
committerSamuel Gruetter2021-03-23 15:59:48 -0400
commit1657b1156c29d969f1e8a1b5785e17d5984ea7a6 (patch)
treed6484337c5717ea00037d85a1edc31b46d7da40c /user-contrib
parentd3f78cad1532f000106ed0c0b8be2ac384ce1d3a (diff)
fix documentation of Ltac2.Env.expand
Diffstat (limited to 'user-contrib')
-rw-r--r--user-contrib/Ltac2/Env.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/user-contrib/Ltac2/Env.v b/user-contrib/Ltac2/Env.v
index d7c5e693f6..9ab95e6d03 100644
--- a/user-contrib/Ltac2/Env.v
+++ b/user-contrib/Ltac2/Env.v
@@ -16,7 +16,7 @@ Ltac2 @ external get : ident list -> Std.reference option := "ltac2" "env_get".
Ltac2 @ external expand : ident list -> Std.reference list := "ltac2" "env_expand".
(** Returns the list of all global references whose absolute name contains
- the argument list as a prefix. *)
+ the argument list as a suffix. *)
Ltac2 @ external path : Std.reference -> ident list := "ltac2" "env_path".
(** Returns the absolute name of the given reference. Panics if the reference