comparison src/Match.v @ 437:8077352044b2

A pass over all formatting, after big pile of coqdoc changes
author Adam Chlipala <adam@chlipala.net>
date Fri, 27 Jul 2012 16:47:28 -0400
parents 85e743564b22
children 0650420c127b
comparison
equal deleted inserted replaced
436:5d5e44f905c7 437:8077352044b2
400 (* end thide *) 400 (* end thide *)
401 401
402 (* EX: Write a list map function in Ltac. *) 402 (* EX: Write a list map function in Ltac. *)
403 403
404 (* begin hide *) 404 (* begin hide *)
405 (* begin thide *)
405 Definition mapp := (map, list). 406 Definition mapp := (map, list).
407 (* end thide *)
406 (* end hide *) 408 (* end hide *)
407 409
408 (** We can also use anonymous function expressions and local function definitions in Ltac, as this example of a standard list [map] function shows. *) 410 (** We can also use anonymous function expressions and local function definitions in Ltac, as this example of a standard list [map] function shows. *)
409 411
410 (* begin thide *) 412 (* begin thide *)