coq - The formal proof system

Age	Commit message (Collapse)	Author
2013-12-04	Fix g_derive.ml4.	Arnaud Spiwack
	My bad, I forgot to fix the classification before comitting.
2013-12-04	Derive plugin.	Arnaud Spiwack
	A small plugin to support program deriving (à la Richard Bird) in Coq. It's fairly simple: Require Coq.Derive.Derive. Derive f From g Upto eq As h. Produces a goal (actually two, but the first one is automatically shelved): \|- eq g ?42 And closing the proof produces two definitions: f is instantiated with the value of ?42 (it's always transparent). And h is instantiated with the content of the proof (it is transparent or opaque depending on whether the proof was closed with Defined or Qed).