aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--ltac/g_ltac.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4
index a3895e3401..215763d5a5 100644
--- a/ltac/g_ltac.ml4
+++ b/ltac/g_ltac.ml4
@@ -176,7 +176,7 @@ GEXTEND Gram
tactic_arg_compat:
[ [ a = tactic_arg -> a
| c = Constr.constr -> (match c with CRef (r,None) -> Reference r | c -> ConstrMayEval (ConstrTerm c))
- (* Unambigous entries: tolerated w/o "ltac:" modifier *)
+ (* Unambiguous entries: tolerated w/o "ltac:" modifier *)
| "()" -> TacGeneric (genarg_of_unit ()) ] ]
;
(* Can be used as argument and at toplevel in tactic expressions. *)