Commit 7fa1a2b3 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

add more libs

parent 2a0d7022
......@@ -54,7 +54,7 @@ Proof.
try assumption ; rewrite Hcarr2;
rewrite <- car25519_eq_car25519_Zlength by assumption;
eapply (doubleCar_ext_str (16.lst l1) _ 303) ;
try omega ;
try omega ;
try (eapply bounds.le_lt_trans ; [eapply Hbounds | | ] ; compute ; reflexivity);
try (rewrite car25519_eq_car25519_Zlength by auto ; try rewrite Hcarr1 ; reflexivity).
Qed.
......@@ -6,6 +6,10 @@ Import ListNotations.
Lemma ListSame : forall A (h1 h2: A) (q1 q2:list A), h1 :: q1 = h2 :: q2 <-> h1 = h2 /\ q1 = q2.
Proof. boum. Qed.
Lemma nth_drop : forall A (n:nat) (l:list A) (d: A), n < length l -> drop n l = nth n l d :: drop (S n) l.
Proof. induction n ; destr_boum l. Qed.
Arguments nth_drop [A] _ _ _ _.
(*
Lemma app_nill_r : forall (A:Type) (l:list A), l ++ nil = l.
Proof. boum. Qed.
......
......@@ -31,7 +31,7 @@ DEPFLAGS:=$(COQFLAGS)
COQC=$(COQBIN)coqc
COQTOP=$(COQBIN)coqtop
COQDEP=$(COQBIN)coqdep $(DEPFLAGS)
COQDOC=$(COQBIN)coqdoc
COQDOC=$(COQBIN)coqdoc -d doc -g -utf8 $(DEPFLAGS)
COQVERSION= 8.5pl1 or-else 8.5pl2 or-else 8.5pl3 or-else 8.6beta1 or-else 8.6
COQV=$(shell $(COQC) -v)
......@@ -93,7 +93,7 @@ Car: .loadpath $(CAR_FILES:%.v=Car/%.vo)
doc:
mkdir -p doc
$(COQDOC) -d doc $(FILES)
$(COQDOC) $(FILES)
dep:
@$(COQDEP) $(filter $(wildcard *.v */*.v */*/*.v),$(FILES))
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment