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
*	This patch removes unused "open" (automatically generated from	regisgia	2012-09-14
*	Updating headers.	herbelin	2012-08-08
*	The tactic remember now accepts a final eqn:H option (grant wish #2489)	letouzey	2012-07-09
*	induction/destruct : nicer syntax for generating equations (solves #2741)	letouzey	2012-07-09
*	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot	2012-06-22
*	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
*	Noise for nothing	pboutill	2012-03-02
*	Applying Tom Prince's patch to support parametric "constructor n" in	herbelin	2011-10-25
*	Added support for referring to subterms of the goal by pattern.	herbelin	2011-09-26
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Fixed a bug in pretty-printing "induction" and "destruct" due to a	herbelin	2010-06-13
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Removing redundant internal variants of apply tactic and simplification of ML...	herbelin	2010-04-14
*	Fixing bug #2146 (broken selection of occurrences in "change").	herbelin	2009-12-30
*	Generic support for open terms in tactics	herbelin	2009-12-21
*	Only one "in" clause in "destruct" even for a multiple "destruct".	herbelin	2009-09-20
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	- Add more precise error localisation when one of the application fails	herbelin	2009-08-04
*	Added "etransitivity".	herbelin	2009-08-03
*	Fixed a typo in "info" for tactic "right".	herbelin	2009-08-02
*	Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0	herbelin	2009-06-06
*	Fixing bug #2308 ("instantiate" tactic did not comply with	herbelin	2009-04-24
*	Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"	herbelin	2009-03-16
*	About "apply in":	herbelin	2008-12-09
*	Fix bug #1977 by allowing the [apply] variants to take an [open_constr]	msozeau	2008-10-23
*	Add a type argument to letin_tac instead of using casts and recomputing	msozeau	2008-09-12
*	Évolutions diverses et variées.	herbelin	2008-08-04
*	- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)	herbelin	2008-06-10
*	- Extension de "generalize" en "generalize c as id at occs".	herbelin	2008-06-08
*	Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve	herbelin	2008-04-25
*	Bugs, nettoyage, et améliorations diverses	herbelin	2008-04-13
*	Ajout "simple apply" et "simple eapply" pour apply sans unfold	herbelin	2008-04-01
*	f_equal, revert, specialize in ML, contradict in better Ltac (+doc)	letouzey	2008-03-07
*	Factorisation des opérations sur le type option de Util dans un module	aspiwack	2007-12-05
*	Ajout de eelim, ecase, edestruct et einduction (expérimental).	herbelin	2007-10-03
*	extension of the rename tactic: the following is now allowed:	letouzey	2007-07-06
*	Nouvelle stratégie d'unification des types des with-bindings dans	herbelin	2007-05-22
*	- Propagation des evars non résolues vers les with_bindings; permet par exemple	herbelin	2007-05-20
*	Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.	herbelin	2007-04-28
*	Changement dans le kernel :	bgregoir	2006-12-11
*	Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...	herbelin	2006-05-30
*	Standardisation nom option_app en option_map	herbelin	2006-04-27
*	- Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses	herbelin	2006-01-16
*	Added 'clear - id' to clear all hypotheses except the ones dependent in the s...	herbelin	2005-03-07
*	COMMITED BYTECODE COMPILER	barras	2004-10-20
*	Nouvelle en-tête	herbelin	2004-07-16