Mercurial > cpdt > repo

diff src/MoreDep.v @ 569:0ce9829efa3b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Back to working in Coq 8.4
author Adam Chlipala <adam@chlipala.net>
date Sun, 20 Jan 2019 15:28:23 -0500
parents 81d63d9c1cc5
children 1dc1d41620b6
line wrap: on
line diff
--- a/src/MoreDep.v	Sun Jan 20 15:16:29 2019 -0500
+++ b/src/MoreDep.v	Sun Jan 20 15:28:23 2019 -0500
@@ -647,7 +647,7 @@
 
   (** We modify Coq's default choice of implicit arguments for [makeRbtree], so that we do not need to specify the [c] and [n] arguments explicitly in later calls. *)
 
-  Arguments makeRbtree [c n].
+  Arguments makeRbtree [c n] _.
 
   (** Finally, we define [insert] as a simple composition of [ins] and [makeRbtree]. *)
 
@@ -917,7 +917,7 @@
   Defined.
 End split.
 
-Arguments split [P1 P2].
+Arguments split [P1 P2] P1_dec P2_dec s.
 
 (* begin hide *)
 Lemma app_empty_end : forall s, s ++ "" = s.