coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Clean-up : removal of Proof_type.tactic_expr	letouzey	2012-10-06
*	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey	2012-10-02
*	More cleaning on Utils and CList. Some parts of the code being	ppedrot	2012-09-17
*	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot	2012-09-14
*	This patch removes unused "open" (automatically generated from	regisgia	2012-09-14
*	Updating headers.	herbelin	2012-08-08
*	Dump references	pboutill	2012-08-05
*	Fix order of introduction of hints to preserve most-recent-first semantics.	msozeau	2012-07-06
*	Fixing previous commit.	ppedrot	2012-06-28
*	Fixing info_auto / info_trivial display.	ppedrot	2012-06-28
*	Forward-port fixes from 8.4 (15358, 15353, 15333).	msozeau	2012-06-04
*	Getting rid of Pp.msg	ppedrot	2012-05-30
*	More uniformisation in Pp.warn functions.	ppedrot	2012-05-30
*	global_reference migrated from Libnames to new Globnames, less deps in gramma...	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
*	locus.mli for occurrences+clauses, misctypes.mli for various little things	letouzey	2012-05-29
*	remove undocumented and scarcely-used tactic auto decomp	letouzey	2012-04-23
*	info_trivial, info_auto, info_eauto, and debug (trivial\|auto)	letouzey	2012-03-30
*	Remove code of obsolete tactics : superauto, autotdb, cdhyp, dhyp, dconcl	letouzey	2012-03-30
*	Noise for nothing	pboutill	2012-03-02
*	Added a flag to control the use of typing when instantiating applied	herbelin	2011-12-17
*	Merge subinstances branch by me and Tom Prince.	msozeau	2011-11-17
*	Auto: removal of ?use_core_db obsolete now that we have nocore	letouzey	2011-11-04
*	Add type annotations around all calls to Libobject.declare_object	letouzey	2011-11-02
*	Auto: avoid storing clausenv (and hence env, evar_map, universes) in vo	letouzey	2011-10-26
*	Fix bug #2227	msozeau	2011-10-18
*	auto with nocore : disable the use of the core database (wish #2188)	letouzey	2011-09-23
*	Fixes bug #2587 (Print Hint gives anomaly when no focused subgoals)	aspiwack	2011-08-16
*	Auto: replace generic compare on pri_auto_tactic by pri_auto_tactic_ord	puech	2011-07-29
*	Generalizing flag use_evars_pattern_unification into a flag	herbelin	2011-06-18
*	Added a flag to restrict conversion in tactic unification on the	herbelin	2011-06-13
*	Added a new flag for freezing evars in tactic unification. Used this	herbelin	2011-06-12
*	Moved allow_K to a unification flag	herbelin	2011-06-10
*	Merge branch 'subclasses' into coq-trunk	msozeau	2011-05-05
*	This is used in the rippling plugin. This also allows fixing bug #2188.	msozeau	2011-04-20
*	Add a flag to control betaiota reduction during unification to maintain backw...	msozeau	2011-04-18
*	- Add modulo_delta_types flag for unification to allow full	msozeau	2011-03-13
*	- Allow to set a particular transparent_state for the local hint	msozeau	2011-03-04
*	- Use transparency information all the way through unification and	msozeau	2011-02-17
*	- Fix treatment of globality flag for typeclass instance hints (they	msozeau	2011-02-14
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23
*	An experimental support for open constrs in hints and in "using"	herbelin	2010-10-31
*	Slight code cleaning in auto.ml (made code of make_exact_entry and	herbelin	2010-10-31
*	Automatically translate hints of the form "c _ ... _" into "c". Besides	herbelin	2010-10-23
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	Added eta-expansion in kernel, type inference and tactic unification,	herbelin	2010-09-20
*	Improved printing of Unfoldable constants in hints databases (used	herbelin	2010-09-02
*	oops. commited files I shouldn't have. reverting on r13341	barras	2010-07-28