Commit fb40295d authored by POTTIER Francois's avatar POTTIER Francois
Browse files

Commented out the place that loops in CFDemos.

parent 98bb9a44
......@@ -151,11 +151,14 @@ Proof.
auto.
auto.
(* short *)
(* TEMPORARY this call to [hsimpl] loops,
and the calls to [auto] above do nothing
hsimpl.
auto.
auto.
auto.
Qed.
*)
Abort.
Lemma hclean_demo_1 : forall A (x X:A) H1 H2 H3 B (F:~~B) Q,
is_local F ->
......@@ -181,6 +184,3 @@ Proof.
skip.
Qed.
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