Commit 6ecf2b67 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

update proofs

parent ed9c5846
......@@ -460,6 +460,8 @@ Qed.
Lemma outer_M_fix_Zlength : forall i j a b o, 0 <= i -> 0 <= j -> Zlength (outer_M_fix i j a b o) = Zlength o.
Proof. convert_length_to_Zlength outer_M_fix_length. Qed.
(* Lemma outer_M_fix_step : forall (i j : Z) (a b o : list Z),
0 <= i ->
0 <= j ->
......
......@@ -8,11 +8,11 @@ DIRS= Libs ListsOp Op Car
INCLUDE= $(foreach a,$(DIRS),$(if $(wildcard $(a)), -Q $(a) $(a)))
PRELUDE = ../Prelude
COQSTDPP = ../Prelude
# for Prelude
ifdef PRELUDE
EXTFLAGS:=$(EXTFLAGS) -Q $(PRELUDE) Prelude
ifdef COQSTDPP
EXTFLAGS:=$(EXTFLAGS) -Q $(COQSTDPP) Prelude
endif
# for SSReflect
......
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