aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Program
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-02-23 11:26:51 +0100
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-02-23 13:37:52 +0100
commitdf2f50db3703b4f7f88f00ac382c7f3f1efaceb3 (patch)
treec11084a17eec2bc25bdcbba715aa1ba50b108272 /theories/Program
parent705bf896bfc552e95403d097fe9b8031c598d88b (diff)
Fix some typos in comments.
Diffstat (limited to 'theories/Program')
-rw-r--r--theories/Program/Utils.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v
index e39128cb8..65fe87801 100644
--- a/theories/Program/Utils.v
+++ b/theories/Program/Utils.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(** Various syntaxic shortands that are useful with [Program]. *)
+(** Various syntactic shorthands that are useful with [Program]. *)
Require Export Coq.Program.Tactics.