coq - The formal proof system

Age	Commit message (Expand)	Author
2012-06-22	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot
2012-06-14	Internalization of pattern is done in two phases.	pboutill
2012-05-29	Extend become a mli-only file in intf/	letouzey
2012-05-29	No more Univ in grammar.cma	letouzey
2012-05-29	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey
2012-05-29	Glob_term: minor formatting	letouzey
2012-05-29	Pattern as a mli-only file, operations in Patternops	letouzey
2012-05-29	New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr	letouzey
2012-05-29	Glob_term now mli-only, operations now in Glob_ops	letouzey
2012-05-29	Tacexpr as a mli-only, the few functions there are now in Tacops	letouzey
2012-05-29	locus.mli for occurrences+clauses, misctypes.mli for various little things	letouzey
2012-05-29	Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd	letouzey
2012-05-29	Decl_kinds becomes a pure mli file, remaining ops in new file kindops.ml	letouzey
2012-05-29	Vernacexpr is now a mli-only file, locality stuff now in locality.ml	letouzey