coq - The formal proof system

Age	Commit message (Expand)	Author
2014-08-18	Adding a new intro-pattern for "apply in" on the fly. Using syntax	Hugo Herbelin
2014-08-18	Reorganisation of intropattern code	Hugo Herbelin
2013-09-18	At least made the evar type opaque! There are still 5 remaining unsafe	ppedrot
2013-07-17	Declaremods: major refactoring, stop duplicating libobjects in modules	letouzey
2013-07-09	Revising r16550 about providing intro patterns for applying injection:	herbelin
2013-01-22	New implementation of the conversion test, using normalization by evaluation to	mdenes
2012-12-14	Modulification of identifier	ppedrot
2012-10-02	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey
2012-10-02	avoid referring to Term in constrexpr.mli and glob_term.mli	letouzey
2012-08-08	Updating headers.	herbelin
2012-08-07	Avoid Pp.std_ppcmds in Misctypes.sort_info	letouzey
2012-06-22	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot
2012-05-29	No more Univ in grammar.cma	letouzey
2012-05-29	Glob_term now mli-only, operations now in Glob_ops	letouzey
2012-05-29	locus.mli for occurrences+clauses, misctypes.mli for various little things	letouzey