Port DataStruct

Makefile

@@ -7,7 +7,6 @@ MODULES_DOC   := $(MODULES_PROSE) $(MODULES_CODE)
 MODULES       := $(MODULES_NODOC) $(MODULES_DOC)
 VS            := $(MODULES:%=src/%.v)
 VS_DOC        := $(MODULES_DOC:%=%.v)
-GLOBALS       := .coq_globals
 TEMPLATES     := $(MODULES_CODE:%=templates/%.v)
 
 .PHONY: coq clean doc dvi html templates install cpdt.tgz
@@ -17,13 +16,13 @@ coq: Makefile.coq
 
 Makefile.coq: Makefile $(VS)
 	coq_makefile $(VS) \
-		COQC = "coqc -I src -dump-glob $(GLOBALS)" \
+		COQC = "coqc -I src" \
 		COQDEP = "coqdep -I src" \
 		-o Makefile.coq
 
 clean:: Makefile.coq
 	make -f Makefile.coq clean
-	rm -f Makefile.coq .depend $(GLOBALS) cpdt.tgz \
+	rm -f Makefile.coq .depend cpdt.tgz \
 		latex/*.sty latex/cpdt.* templates/*.v
 	rm -f *.aux *.dvi *.log
 
@@ -51,7 +50,6 @@ latex/%.pdf: latex/%.dvi
 html: Makefile $(VS) src/toc.html
 	mkdir -p html
 	cd src ; coqdoc --interpolate $(VS_DOC) \
-		--glob-from ../$(GLOBALS) \
 		-d ../html
 	cp src/toc.html html/
 

src/DepList.v

@@ -31,14 +31,14 @@ Section ilist.
 
   Implicit Arguments icons [n].
 
-  Fixpoint index (n : nat) : Type :=
+  Fixpoint fin (n : nat) : Type :=
     match n with
       | O => Empty_set
-      | S n' => option (index n')
+      | S n' => option (fin n')
     end.
 
-  Fixpoint get (n : nat) : ilist n -> index n -> A :=
-    match n return ilist n -> index n -> A with
+  Fixpoint get (n : nat) : ilist n -> fin n -> A :=
+    match n return ilist n -> fin n -> A with
       | O => fun _ idx => match idx with end
       | S n' => fun ls idx =>
         match idx with

src/Generic.v

@@ -217,7 +217,7 @@ Section ok.
   Definition datatypeDenoteOk :=
     forall P : T -> Prop,
       (forall c (m : member c dt) (x : nonrecursive c) (r : ilist T (recursive c)),
-        (forall i : index (recursive c), P (get r i))
+        (forall i : fin (recursive c), P (get r i))
         -> P ((hget dd m) x r))
       -> forall v, P v.