coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \| \| \| \|	Tactic notation printing accesses all the token data.	Pierre-Marie Pédrot	2016-01-16
* \| \| \| \|	Removing constr generic argument.	Pierre-Marie Pédrot	2016-01-14
* \| \| \| \|	Removing ident and var generic arguments.	Pierre-Marie Pédrot	2016-01-14
* \| \| \| \|	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
* \| \| \| \| \|	Use streams rather than strings to handle bullet suggestions.	Guillaume Melquiond	2016-01-02
* \| \| \| \| \|	Remove some unused functions.	Guillaume Melquiond	2016-01-02
* \| \| \| \| \|	Reduce dependencies of interface files.	Guillaume Melquiond	2016-01-02
* \| \| \| \| \|	Remove useless rec flags.	Guillaume Melquiond	2016-01-02
* \| \| \| \| \|	Simplification of grammar_prod_item type.	Pierre-Marie Pédrot	2016-01-02
* \| \| \| \| \|	Separation of concern in TacAlias API.	Pierre-Marie Pédrot	2016-01-02
* \| \| \| \| \|	Do not compose List.length with List.filter.	Guillaume Melquiond	2015-12-31
* \| \| \| \| \|	External tactics and notations now accept any tactic argument.	Pierre-Marie Pédrot	2015-12-30
* \| \| \| \| \|	Removing the special status of open_constr generic argument.	Pierre-Marie Pédrot	2015-12-28
* \| \| \| \| \|	Tentative API fix for tactic arguments to be fed to tclWITHHOLES.	Pierre-Marie Pédrot	2015-12-27
* \| \| \| \| \|	Removing auto from the tactic AST.	Pierre-Marie Pédrot	2015-12-24
* \| \| \| \| \|	Do not compose "str" and "to_string" whenever possible.	Guillaume Melquiond	2015-12-22
* \| \| \| \| \|	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
\|/ / / / /
* \| \| \| \|	CLEANUP: the definition of the "Constrexpr.case_expr" type was simplified	Matej Kosik	2015-12-18
* \| \| \| \|	CLEANUP: Vernacexpr.VernacDeclareTacticDefinition	Matej Kosik	2015-12-18
* \| \| \| \|	CLEANUP: Removing "Vernacexpr.VernacNop" variant to which no Vernacular comma...	Matej Kosik	2015-12-18
* \| \| \| \|	CLEANUP: Vernacexpr.vernac_expr	Matej Kosik	2015-12-18
* \| \| \| \|	Tying the loop in tactic printing API.	Pierre-Marie Pédrot	2015-12-18
* \| \| \| \|	Getting rid of some hardwired generic arguments.	Pierre-Marie Pédrot	2015-12-17
* \| \| \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-08
\|\\| \| \| \|
* \| \| \| \|	Moving extended_rel_vect/extended_rel_list to the kernel.	Hugo Herbelin	2015-12-05
* \| \| \| \|	Getting rid of the dynamic node of the tactic AST.	Pierre-Marie Pédrot	2015-12-04
* \| \| \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-03
\|\ \ \ \ \
\| \| * \| \| \|	Improving over printing of let-tuple (see #4447).	Hugo Herbelin	2015-12-03
\| \|/ / / /
\| * \| \| \|	Dead code from August 2014 in apply in.	Hugo Herbelin	2015-12-02
* \| \| \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-05
\|\\| \| \| \|
\| * \| \| \|	Adding syntax "Show id" to show goal named id (shelved or not).	Hugo Herbelin	2015-11-02
\| \| * \| \|	Make the code of compare functions linear in the number of constructors.	Arnaud Spiwack	2015-10-29
* \| \| \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-29
\|\\| \| \| \| \| \|/ / / \|/\| \| \|
\| * \| \|	Univs: local names handling.	Matthieu Sozeau	2015-10-28
\| * \| \|	Printing of @{} instances for polymorphic references in Print and About.	Matthieu Sozeau	2015-10-28
* \| \| \|	Type delayed_open_constr is now monotonic.	Pierre-Marie Pédrot	2015-10-19
* \| \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-09
\|\\| \| \|
\| * \| \|	Axioms now support the universe binding syntax.	Pierre-Marie Pédrot	2015-10-08
\| * \| \|	Goptions: new value type: optional string	Enrico Tassi	2015-10-08
\| * \| \|	Univs: add Strict Universe Declaration option (on by default)	Matthieu Sozeau	2015-10-07
* \| \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-06
\|\\| \| \|
\| * \| \|	Univs: fix printing bug #3797.	Matthieu Sozeau	2015-10-05
\| \| \| *	Show assumptions of well-foundedness in `Print Assumptions`	Arnaud Spiwack	2015-09-25
* \| \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-09-25
\|\\| \| \|
\| \| \| *	Add a flag in `VernacFixpoint` and `VernacCoFixpoint` to control assuming gua...	Arnaud Spiwack	2015-09-25