# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1548016103 18000
# Node ID 0ce9829efa3b41a67fbb6eed962af138e88e6756
# Parent  81d63d9c1cc511beb4ed8fec4822f1116d12816e
Back to working in Coq 8.4

diff -r 81d63d9c1cc5 -r 0ce9829efa3b src/DataStruct.v
--- a/src/DataStruct.v	Sun Jan 20 15:16:29 2019 -0500
+++ b/src/DataStruct.v	Sun Jan 20 15:28:23 2019 -0500
@@ -243,10 +243,10 @@
 
 (* begin thide *)
 Arguments HNil [A B].
-Arguments HCons [A B x ls].
+Arguments HCons [A B x ls] _ _.
 
 Arguments HFirst [A elm ls].
-Arguments HNext [A elm x ls].
+Arguments HNext [A elm x ls] _.
 (* end thide *)
 
 (** By putting the parameters [A] and [B] in [Type], we enable fancier kinds of polymorphism than in mainstream functional languages.  For instance, one use of [hlist] is for the simple heterogeneous lists that we referred to earlier. *)
@@ -481,7 +481,7 @@
 
 End fhlist.
 
-Arguments fhget [A B elm ls].
+Arguments fhget [A B elm ls] _ _.
 
 (** How does one choose between the two data structure encoding strategies we have presented so far?  Before answering that question in this chapter's final section, we introduce one further approach. *)
 
@@ -592,7 +592,7 @@
 
 End tree.
 
-Arguments Node [A n].
+Arguments Node [A n] _.
 
 (** We can redefine [sum] and [inc] for our new [tree] type.  Again, it is useful to define a generic fold function first.  This time, it takes in a function whose domain is some [ffin] type, and it folds another function over the results of calling the first function at every possible [ffin] value. *)
 
@@ -608,7 +608,7 @@
     end.
 End rifoldr.
 
-Arguments rifoldr [A B] f i [n].
+Arguments rifoldr [A B] f i [n] _.
 
 Fixpoint sum (t : tree nat) : nat :=
   match t with
@@ -708,7 +708,7 @@
     end.
 End cond.
 
-Arguments cond [A] default [n].
+Arguments cond [A] default [n] _ _.
 (* end thide *)
 
 (** Now the expression interpreter is straightforward to write. *)
@@ -797,7 +797,7 @@
     end.
 End cfoldCond.
 
-Arguments cfoldCond [t] default [n].
+Arguments cfoldCond [t] default [n] _ _.
 (* end thide *)
 
 (** Like for the interpreters, most of the action was in this helper function, and [cfold] itself is easy to write. *)
diff -r 81d63d9c1cc5 -r 0ce9829efa3b src/DepList.v
--- a/src/DepList.v	Sun Jan 20 15:16:29 2019 -0500
+++ b/src/DepList.v	Sun Jan 20 15:28:23 2019 -0500
@@ -198,11 +198,11 @@
 End hlist.
 
 Arguments HNil [A B].
-Arguments HCons [A B x ls].
-Arguments hmake [A B].
+Arguments HCons [A B x ls] _ _.
+Arguments hmake [A B] f ls.
 
 Arguments HFirst [A elm ls].
-Arguments HNext [A elm x ls].
+Arguments HNext [A elm x ls] _.
 
 Infix ":::" := HCons (right associativity, at level 60).
 Infix "+++" := happ (right associativity, at level 60).
@@ -233,4 +233,4 @@
   Qed.
 End hmap.
 
-Arguments hmap [A B1 B2] f [ls].
+Arguments hmap [A B1 B2] f [ls] hl.
diff -r 81d63d9c1cc5 -r 0ce9829efa3b src/Equality.v
--- a/src/Equality.v	Sun Jan 20 15:16:29 2019 -0500
+++ b/src/Equality.v	Sun Jan 20 15:28:23 2019 -0500
@@ -214,7 +214,7 @@
     end.
 End fhlist.
 
-Arguments fhget [A B elm ls].
+Arguments fhget [A B elm ls] _ _.
 
 (* begin hide *)
 (* begin thide *)
@@ -235,7 +235,7 @@
       | _ :: _ => fun hls => (f (fst hls), fhmap _ (snd hls))
     end.
 
-  Arguments fhmap [ls].
+  Arguments fhmap [ls] _.
 
   (* begin hide *)
   (* begin thide *)
@@ -496,7 +496,7 @@
       | _ :: _ => fun hls1 hls2 => (fst hls1, fhapp _ _ (snd hls1) hls2)
     end.
 
-  Arguments fhapp [ls1 ls2].
+  Arguments fhapp [ls1 ls2] _ _.
 
   (* EX: Prove that fhapp is associative. *)
 (* begin thide *)
@@ -676,7 +676,7 @@
 (* end thide *)
 End fhapp.
 
-Arguments fhapp [A B ls1 ls2].
+Arguments fhapp [A B ls1 ls2] _ _.
 
 (** This proof strategy was cumbersome and unorthodox, from the perspective of mainstream mathematics.  The next section explores an alternative that leads to simpler developments in some cases. *)
 
diff -r 81d63d9c1cc5 -r 0ce9829efa3b src/MoreDep.v
--- 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.
diff -r 81d63d9c1cc5 -r 0ce9829efa3b src/ProgLang.v
--- a/src/ProgLang.v	Sun Jan 20 15:16:29 2019 -0500
+++ b/src/ProgLang.v	Sun Jan 20 15:28:23 2019 -0500
@@ -105,7 +105,7 @@
 
   | Let : forall G t1 t2, term G t1 -> term (t1 :: G) t2 -> term G t2.
 
-  Arguments Const [G].
+  Arguments Const [G] _.
 
   (** Here are two example term encodings, the first of addition packaged as a two-argument curried function, and the second of a sample application of addition to constants. *)
 
@@ -266,7 +266,7 @@
                 end
     end.
 
-  Arguments insertAtS [t] x [G].
+  Arguments insertAtS [t] x [G] n _.
 
   (** Next we prove that [liftVar] is correct.  That is, a lifted variable retains its value with respect to a substitution when we perform an analogue to lifting by inserting a new mapping into the substitution. *)
 
@@ -355,9 +355,9 @@
     | Let : forall t1 t2, term t1 -> (var t1 -> term t2) -> term t2.
   End var.
 
-  Arguments Var [var t].
-  Arguments Const [var].
-  Arguments Abs [var dom ran].
+  Arguments Var [var t] _.
+  Arguments Const [var] _.
+  Arguments Abs [var dom ran] _.
 
   (** Coq accepts this definition because our embedded functions now merely take _variables_ as arguments, instead of arbitrary terms.  One might wonder whether there is an easy loophole to exploit here, instantiating the parameter [var] as [term] itself.  However, to do that, we would need to choose a variable representation for this nested mention of [term], and so on through an infinite descent into [term] arguments.
 
diff -r 81d63d9c1cc5 -r 0ce9829efa3b src/Universes.v
--- a/src/Universes.v	Sun Jan 20 15:16:29 2019 -0500
+++ b/src/Universes.v	Sun Jan 20 15:28:23 2019 -0500
@@ -1165,7 +1165,7 @@
     destruct n; simpl; unfold error; congruence.
   Defined.
 
-  Arguments nth_error_nil [A n x].
+  Arguments nth_error_nil [A n x] _.
 
   Lemma Some_inj : forall A (x y : A),
     Some x = Some y