The Coq mailing list

[Lionel Elie Mamane <lionel AT mamane.lu>]

Hi,

Given this code:

Definition twopower: nat -> nat.
Admitted.

Definition log2': forall x:nat, {y:nat | twopower y <= x < twopower 
(y+1)}+{x=0}.
intros.
case x.
right; apply (refl_equal 0).
clear x; intros Px.
set (x:=(S Px)).
left.
refine (exist _ ((fix lg (n:nat) {struct n}:nat:= _ ) _) _).

I get at this refine an anomaly:

 Anomaly: Evar ?13 was not declared. Please report.

So I report it "par la présente".

Have fun,

-- 
Lionel