coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
* \|	Merge PR #6550: Remove outdated note about rlwrap in setup.txt	Maxime Dénès	2018-01-22
\|\ \ \| \|/ \|/\|
\| *	Stop talking about debian in "A note about rlwrap"	Gaëtan Gilbert	2018-01-08
\| \| \| \| \| \| \| \|	Debian stable version is 0.42-3 right now.
* \|	Merge PR #6501: Document use of ocamldebug from the command line in ↵	Maxime Dénès	2018-01-08
\|\ \ \| \|/ \|/\| \| \|	Cygwin/Windows
\| *	Add instructions for debugging from the command line (and in Windows)	Jim Fehrle	2017-12-29
\| \| \| \| \| \| \| \|	Avoid generating \r characters in generated dev/ocamldebug-coq (affects Windows)
* \|	[API] remove large file containing duplicate interfaces	Enrico Tassi	2017-12-27
\| \| \| \| \| \| \| \| \| \|	... in favor of having Public/Internal sub modules in each and every module grouping functions according to their intended client.
* \|	[ide] [doc] Document tweak to Query call.	Emilio Jesus Gallego Arias	2017-12-26
\|/
*	Merge PR #6413: [econstr] Switch constrintern API to non-imperative style.	Maxime Dénès	2017-12-18
\|\
\| *	[econstr] Switch constrintern API to non-imperative style.	Emilio Jesus Gallego Arias	2017-12-15
\| \| \| \| \| \| \| \| \| \|	We remove a lot of uses of `evar_map` ref in `vernac`, cleanup step desirable to progress with EConstr there.
* \|	Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.	Maxime Dénès	2017-12-14
\|\ \ \| \|/ \|/\|
\| *	[build] Remove coqmktop in favor of ocamlfind.	Emilio Jesus Gallego Arias	2017-12-10
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We remove coqmktop in favor of a couple of simple makefile rules using ocamlfind. In order to do that, we introduce a new top-level file that calls the coqtop main entry. This is very convenient in order to use other builds systems such as `ocamlbuild` or `jbuilder`. An additional consideration is that we must perform a side-effect on init depending on whether we have an OCaml toplevel available [byte] or not. We do that by using two different object files, one for the bytecode version other for the native one, but we may want to review our choice. We also perform some smaller cleanups taking profit from ocamlfind.
* \|	[api] Remove yet another type alias.	Emilio Jesus Gallego Arias	2017-12-09
\| \|
\| *	[lib] Rename Profile to CProfile	Emilio Jesus Gallego Arias	2017-12-09
\|/ \| \| \| \|	New module introduced in OCaml 4.05 I think, can create problems when linking with the OCaml toplevel for `Drop`.
*	[lib] [api] Introduce record for `object_prefix`	Emilio Jesus Gallego Arias	2017-11-29
\| \| \| \| \|	This is a minor cleanup adding a record in a try to structure the state living in `Lib`.
*	Change OCAMLRUNPARAM warning to mention OCaml 4.06	Paul Steckler	2017-11-13
\|
*	[api] Remove 8.7 ML-deprecated functions.	Emilio Jesus Gallego Arias	2017-11-07
\|
*	Merge PR #6047: A generic printer for ltac values	Maxime Dénès	2017-11-03
\|\
* \	Merge PR #6027: Mention the migration from Bugzilla to GitHub issues in ↵	Maxime Dénès	2017-11-03
\|\ \ \| \| \| \| \| \| \| \| \|	dev/doc/changes.
* \ \	Merge PR #6024: Update of Coq version history	Maxime Dénès	2017-11-03
\|\ \ \
\| \| \| *	Using a specific function to register vernac printers.	Hugo Herbelin	2017-11-02
\| \|_\|/ \|/\| \|
\| \| *	Mention the migration from Bugzilla to GitHub issues in dev/doc/changes.	Théo Zimmermann	2017-10-27
\| \| \|
* \| \|	Passing around the flag for injection so that tactics calling inj at	Hugo Herbelin	2017-10-26
\| \|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	ML level can set the flags themselves. In particular, using injection and discriminate with option "Keep Proofs Equalities" when called from "decide equality" and "Scheme Equality". This fixes bug #5281.
\| *	Updating version history wrt 8.7.	Hugo Herbelin	2017-10-26
\| \|
\| *	Updating version history wrt 8.6.	Hugo Herbelin	2017-10-26
\| \|
\| *	Updating version history wrt 8.5.	Hugo Herbelin	2017-10-26
\|/
*	[configure] Support for flambda flags.	Emilio Jesus Gallego Arias	2017-10-10
\| \| \| \| \| \| \| \| \|	We add a new option to configure `-flambda-opts` to allow passing custom flags to flambda. Example: ``` ./configure -flambda-opts "-O3 -unbox-closures" ```
*	Extract changes to the XML protocol from its doc	Théo Zimmermann	2017-10-06
\|
*	Make the XML protocol doc more version-independent	Théo Zimmermann	2017-10-06
\|
*	Improve documentation of Status message.	Maxime Dénès	2017-09-19
\|
*	Merge PR #939: [general] Merge parsing with highparsing, put toplevel at the ↵	Maxime Dénès	2017-09-15
\|\ \| \| \| \| \| \|	top of the linking chain.
* \	Merge PR #962: Move dev/doc/changes to Markdown.	Maxime Dénès	2017-09-15
\|\ \
* \ \	Merge PR #999: For BZ#5688, mention hanging issue in ocamldebug and workaround	Maxime Dénès	2017-08-31
\|\ \ \
\| * \| \|	mention issue with OCAMLRUNPARAM and ocamldebug	Paul Steckler	2017-08-29
\| \| \| \|
\| \| \| *	[general] Merge parsing with highparsing, put toplevel at the top of the ↵	Emilio Jesus Gallego Arias	2017-08-29
\| \| \|/ \| \|/\| \| \| \| \| \| \|	linking chain.
* \| \|	Adapt debugging doc to configure/Makefile changes.	Théo Zimmermann	2017-08-29
\| \| \|
* \| \|	Move debugging to Markdown.	Théo Zimmermann	2017-08-29
\|/ / \| \| \| \|	With a minimal diff (so I'm not putting quotes ` ` around all the code).
\| *	Move dev/doc/changes to Markdown.	Théo Zimmermann	2017-08-29
\|/ \| \| \| \|	And remove old French part. And move part about the plugin API to the right section.
*	Merge PR #819: Cleanup old things	Maxime Dénès	2017-08-29
\|\
* \|	Mention tclINDEPENDENTL (#349) in dev/doc/changes.	Théo Zimmermann	2017-08-16
\| \|
\| *	Remove obsolete files	Gaëtan Gilbert	2017-08-01
\| \| \| \| \| \| \| \| \| \|	db_printers just isn't used. api.txt is superseded by the API OCaml interface.
\| *	Add .v extension to dev/doc/notes-on-conversion	Gaëtan Gilbert	2017-08-01
\|/ \| \| \|	This gives syntax highlighting in Coq-aware editors.
*	Merge PR #775: [toplevel] Remove long ago deprecated and NOOP options.	Maxime Dénès	2017-08-01
\|\
* \	Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t instead	Maxime Dénès	2017-07-31
\|\ \
* \ \	Merge PR #852: Makefile: fails if some .vo or .cm* file has no source	Maxime Dénès	2017-07-28
\|\ \ \
\| \| \| *	[toplevel] Remove long ago deprecated and NOOP options.	Emilio Jesus Gallego Arias	2017-07-27
\| \|_\|/ \|/\| \| \| \| \| \| \| \|	Minor clean up, no sense in having these as they do nothing.
\| \| *	deprecate Pp.std_ppcmds type alias	Matej Košík	2017-07-27
\| \| \|
* \| \|	Merge PR #886: Fixing what was presumably a typo in the naming conventions file	Maxime Dénès	2017-07-26
\|\ \ \ \| \|_\|/ \|/\| \|
* \| \|	[API] Remove `open API` in ml files in favor of `-open API` flag.	Emilio Jesus Gallego Arias	2017-07-17
\| \| \|
\| * \|	Fixing what was presumably a typo in the naming conventions file.	Hugo Herbelin	2017-07-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Indeed, "forall x, op x x = x" in not in the list, while this is one of the two standard meanings of idempotence. So, knowing that x, y, ... and not n are used elsewhere for variables names, and elt for constants. Moreover, it is probable that before using consistently x, y and z, I had also used m and n, sometimes. So, a convergent probability that it is (just) a typo.
* \| \|	Fix a typo in dev/changes.	Pierre-Marie Pédrot	2017-07-14
\| \| \|
* \| \|	Document the changes in API brought by this series of patches.	Pierre-Marie Pédrot	2017-07-14
\|/ /