Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] standard library Coq.Sorting.Heap treesort

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] standard library Coq.Sorting.Heap treesort


chronological Thread 
  • From: Jean-Marc Notin <notin AT lix.polytechnique.fr>
  • To: gang chen <gangchen_sh AT yahoo.com>
  • Cc: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] standard library Coq.Sorting.Heap treesort
  • Date: Fri, 19 Oct 2007 11:52:59 +0200
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
> sig2 and its notation are defined in the Datatypes.v file in the
> standard library.
> 
Oups ! It is not in Datatypes.v, but in Specif.v...

-- 
Jean-Marc Notin 
<notin AT lix.polytechnique.fr>



Archive powered by MhonArc 2.6.16.

Top of Page