aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@college-de-france.fr>2019-08-02 10:48:27 +0200
committerXavier Leroy <xavier.leroy@college-de-france.fr>2019-08-07 10:37:28 +0200
commitefb5f52493345a1e17cc10b56023dfe00beb6074 (patch)
treeb9ea3ff5813168e9bea240145462d90bcd7a010f
parent136d25dcbf2829e63c20b96acf86d34c94474fde (diff)
downloadcompcert-efb5f52493345a1e17cc10b56023dfe00beb6074.tar.gz
compcert-efb5f52493345a1e17cc10b56023dfe00beb6074.zip
Coq 8.10 compatibility: tweak Argument command
-rw-r--r--lib/Maps.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/Maps.v b/lib/Maps.v
index cfb866ba..9e44a7fe 100644
--- a/lib/Maps.v
+++ b/lib/Maps.v
@@ -190,7 +190,7 @@ Module PTree <: TREE.
| Leaf : tree A
| Node : tree A -> option A -> tree A -> tree A.
- Arguments Leaf [A].
+ Arguments Leaf {A}.
Arguments Node [A].
Scheme tree_ind := Induction for tree Sort Prop.