The Coq mailing list

[Cedric Auger <Cedric.Auger AT lri.fr>]

Hi all, I know the subject doesn't mean anything; it is more a 
(irrelevant?) feature request than a real question:

Is there any good reason to restrict the use of Canonical Structure to 
toplevel?

---
Record Foo :=
{ bar : Type;
  foobar : bar -> Type;
  barfoo : forall b, foobar b -> bool;
  param1 : bar;
  param2 : forall b, foobar b
}

Definition eval_foo f := f.(barfoo) (f.(param1)) (f.(param2) (f.(param1))).

---
I think it could be handy to define eval_foo as:

Definition eval_foo f :=
 set f as canonical in
 barfoo param1 (param2 param1).

--
Cédric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay