coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
* \|	Stronger invariants on the use of the introduction pattern (pat1,...,patn).	Hugo Herbelin	2016-01-21
* \|	Fixing some problems with double induction.	Hugo Herbelin	2016-01-21
* \|	Code simplification in elim.ml.	Hugo Herbelin	2016-01-20
* \|	Fixing a bug with introduction patterns over inductive types containing let-ins.	Hugo Herbelin	2016-02-18
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
\| *	Fix bug #4420: check_types was losing universe constraints.	Matthieu Sozeau	2016-01-19
* \|	Moving val_cast to Tacinterp.	Pierre-Marie Pédrot	2016-01-17
* \|	Getting rid of the awkward unpack mechanism from Genarg.	Pierre-Marie Pédrot	2016-01-17
* \|	Removing constr generic argument.	Pierre-Marie Pédrot	2016-01-14
* \|	Removing ident and var generic arguments.	Pierre-Marie Pédrot	2016-01-14
* \|	Moving is_quantified_hypothesis to new proof engine.	Hugo Herbelin	2016-01-14
* \|	Update in the documentation of parts of the code of destruct/induction.	Hugo Herbelin	2016-01-14
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-13
\|\\|
\| *	Fix essential bug in new Keyed Unification mode reported by R. Krebbers.	Matthieu Sozeau	2016-01-12
* \|	CLEANUP: removing unused field	Matej Kosik	2016-01-11
* \|	merge	Matej Kosik	2016-01-11
\|\ \
\| * \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
\| \| *	Fix bug #3338 again, no progress is necessary for the success of rewrite_strat.	Matthieu Sozeau	2016-01-11
* \| \|	Fix bug 4479: "Error: Rewriting base foo does not exist." should be catchable.	Pierre-Marie Pédrot	2016-01-09
* \| \|	Monotonizing Ftactic.	Pierre-Marie Pédrot	2016-01-08
\| \| *	Fix bug #4480: progress was not checked for setoid_rewrite.	Matthieu Sozeau	2016-01-07
* \| \|	Remove some unused functions.	Guillaume Melquiond	2016-01-02
* \| \|	Remove duplicate definition.	Guillaume Melquiond	2016-01-02
* \| \|	Remove duplicate declarations.	Guillaume Melquiond	2016-01-02
* \| \|	Reduce dependencies of interface files.	Guillaume Melquiond	2016-01-02
* \| \|	Remove useless rec flags.	Guillaume Melquiond	2016-01-02
* \| \|	Separation of concern in TacAlias API.	Pierre-Marie Pédrot	2016-01-02
* \| \|	Moving apply_type to new proof engine.	Hugo Herbelin	2015-12-30
* \| \|	Taking into account generated typing constraints in tactic "generalize".	Hugo Herbelin	2015-12-30
* \| \|	External tactics and notations now accept any tactic argument.	Pierre-Marie Pédrot	2015-12-30
* \| \|	Implementing non-focussed generic arguments.	Pierre-Marie Pédrot	2015-12-28
* \| \|	Removing the special status of open_constr generic argument.	Pierre-Marie Pédrot	2015-12-28
* \| \|	Eradicating uses of open_constr in TACTIC EXTEND in favour of uconstr.	Pierre-Marie Pédrot	2015-12-28
* \| \|	Factorizing code for untyped constr evaluation.	Pierre-Marie Pédrot	2015-12-27
* \| \|	Removing dead code.	Pierre-Marie Pédrot	2015-12-27
* \| \|	Tentative API fix for tactic arguments to be fed to tclWITHHOLES.	Pierre-Marie Pédrot	2015-12-27
* \| \|	Moving basic generalization tactics upwards for possible use in "intros".	Hugo Herbelin	2015-12-25
* \| \|	Moving code of specialize so that it can accept "as" (no semantic change).	Hugo Herbelin	2015-12-25
* \| \|	Moving specialize to Proofview.tactic.	Hugo Herbelin	2015-12-25
* \| \|	Fixing a bug in the order of side conditions for introduction pattern -> and <-.	Hugo Herbelin	2015-12-25
* \| \|	Fixing an "injection as" bug in the presence of side conditions.	Hugo Herbelin	2015-12-25
* \| \|	Moving the ad hoc interpretation of "intros" as "intros **" from tacinterp.ml	Hugo Herbelin	2015-12-25
* \| \|	Removing auto from the tactic AST.	Pierre-Marie Pédrot	2015-12-24
* \| \|	Removing the last quoted auto tactic in Tauto.	Pierre-Marie Pédrot	2015-12-24
* \| \|	Finer-grained types for toplevel values.	Pierre-Marie Pédrot	2015-12-21
* \| \|	Removing ad-hoc interpretation rules for tactic notations and their genarg.	Pierre-Marie Pédrot	2015-12-21
* \| \|	Changing the toplevel type of the int_or_var generic type to int.	Pierre-Marie Pédrot	2015-12-21
* \| \|	Removing the now useless genarg generic argument.	Pierre-Marie Pédrot	2015-12-21
* \| \|	Using dynamic values in tactic evaluation.	Pierre-Marie Pédrot	2015-12-21
\|/ /