Commit 6b4a743c authored by charguer's avatar charguer

compile 8.5rc1 but not examples

parent 5773f39d
(* open Aux (* required for cfml to do the require in Coq, in the current implementation *) *)
open Aux (* required for cfml to do the require in Coq, in the current implementation *)
open NullPointers
......
EXAMPLE_DIRS=\
DemoMake \
DemoMake \
Compose \
Memoization \
CPSappend \
......@@ -11,6 +11,7 @@ EXAMPLE_DIRS=\
SelfBalancedHeap \
BinaryTrees
#
# Dijkstra
# FingerTree \
# Sieve \
......
......@@ -29,7 +29,10 @@ Proof. apply (Build_Rep eq). congruence. Defined.
Instance list_rep : forall `{Rep a A}, Rep (list a) (list A).
Proof.
intros. apply (Build_Rep (fun l L => Forall2 rep l L)).
induction x; introv H1 H2; inverts H1; inverts H2; prove_rep.
admit.
(* TODO: coqbug in 8.5rc1
induction x; introv H1 H2; inverts H1; inverts H2; prove_rep.
*)
Defined.
Lemma list_rep_cons : forall `{Rep a A} l L x X,
......@@ -53,7 +56,10 @@ Proof.
| None, None => True
| Some x, Some X => rep x X
| _,_ => False end)).
admit.
(* TODO: coqbug in 8.5rc1
intros [x|] [X|] [Y|] H1 H2; prove_rep.
*)
Defined.
Hint Extern 1 (@rep (list _) _ _ _ _) => simpl.
......
......@@ -201,9 +201,9 @@ Proof. auto. Qed.
(* ** tools for post-conditions *)
Ltac is_evar_as_bool E :=
constr:($(first
constr:(ltac:(first
[ is_evar E; exact true
| exact false ])$).
| exact false ])).
Ltac get_post tt :=
match goal with |- ?E =>
......
Markdown is supported
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