coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[api] Move universe syntax to `Glob_term`	Emilio Jesus Gallego Arias	2018-05-08
*	[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.	Emilio Jesus Gallego Arias	2018-05-04
*	[api] Relocate `intf` modules according to dependency-order.	Emilio Jesus Gallego Arias	2018-04-23
*	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	2012-05-29
*	Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd	letouzey	2012-05-29
*	Glob_term.predicate_pattern: No number of parameters with letins.	pboutill	2012-03-02
*	Noise for nothing	pboutill	2012-03-02
*	Added an pattern / occurence syntax for vm_compute.	ppedrot	2012-01-30
*	Remove dynamic stuff from constr_expr and glob_constr	glondu	2011-10-28
*	Take benefit of eta-expansion so that "ex P" is displayed "exists x, P x".	herbelin	2011-04-15
*	More {raw => glob} changes for consistency	glondu	2010-12-24
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23