aboutsummaryrefslogtreecommitdiff
path: root/theories/Program
diff options
context:
space:
mode:
authorEnrico Tassi2015-02-23 17:14:05 +0100
committerEnrico Tassi2015-02-23 17:14:05 +0100
commite87ca456fb4cbe54f09e13f1e20d504d2699ac2b (patch)
tree41b358ee2deb7c614e39f7db27368f9626c19778 /theories/Program
parent28781f3fd6ae6e7f281f906721e8a028679ca089 (diff)
parentdf2f50db3703b4f7f88f00ac382c7f3f1efaceb3 (diff)
Merge branch 'v8.5' into trunk
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 e39128cb81..65fe87801a 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.