coq - The formal proof system

Age	Commit message (Collapse)	Author
2017-09-11	Merge PR #1032: Make our CI policy clearer and more explicit	Maxime Dénès

2017-09-11	Disable OSX signing for temporary artifacts.	Maxime Dénès
	The OSX binaries were signed twice with a fake identity, leading to some obscure errors on Travis in some cases. We disable code signing for Travis artifacts. For released packages, a proper signing will be applied manually.
2017-09-11	Merge PR #1038: Fix Typo in Doc for `Set Parsing Explicit`	Maxime Dénès

2017-09-11	Merge PR #1035: Fix the introduction of SSR refman chapter.	Maxime Dénès

2017-09-11	Merge PR #1029: Fix a refine anomaly "Evar defined twice".	Maxime Dénès

2017-09-11	Merge PR #1014: Add option index entry for NativeCompute Profiling	Maxime Dénès

2017-09-11	Merge PR #1004: Document primitive projections in more detail	Maxime Dénès

2017-09-11	Merge PR #987: In Array.smartmap, read and write from same array	Maxime Dénès

2017-09-11	In stm, fixing a typo about flushing debugging messages.	Hugo Herbelin

2017-09-11	Typo in the header of ide_slave.ml.	Hugo Herbelin

2017-09-11	Coqide: adding a separating space in some debugging messages.	Hugo Herbelin
	This prevents seeing things like MsgDirectory which are actually intended to be two distinct words.
2017-09-09	If backtrace is missing, don't print it.	Pierre-Marie Pédrot

2017-09-09	Update backtraces only when the Ltac2 Backtrace flag is set.	Pierre-Marie Pédrot

2017-09-09	Fix coq/ltac2#26: Ltac1 gives no backtraces.	Pierre-Marie Pédrot

2017-09-09	Fix coq/ltac2#18: Terms should show a backtrace when Set Ltac2 Backtrace is set.	Pierre-Marie Pédrot

2017-09-09	Moving Ltac2 backtraces to the Exninfo mechanism.	Pierre-Marie Pédrot
	I don't know why, but on CoqIDE this triggers a printing of the backtrace twice. This is not reproducible with coqtop.
2017-09-09	Fix coq/ltac2#25: Control.case should not be able to catch Control.throw.	Pierre-Marie Pédrot
	When crossing constr boundaries, we mark exceptions as being fatal not to catch them.
2017-09-08	Fix Typo in Doc for `Set Parsing Explicit`	staffehn

2017-09-08	Normalizing universes before performing term comparison.	Pierre-Marie Pédrot
	This code was probably slightly wrong w.r.t. to a semantics defined as equivalent to first full-blown normalization followed by kernel term equality. Or at least, it was adding redundant constraints.
2017-09-08	Using EConstr equality check in unification.	Pierre-Marie Pédrot
	The code from Universes what essentially a duplicate of the one from EConstr, but they were copied for historical reasons. Now, this is not useful anymore, so that we remove the implementation from Universes and rely on the one from EConstr.
2017-09-08	Using a dedicated argument for tactic quotations.	Pierre-Marie Pédrot
	This prevents having to go through an expensive phase of goal-building, when we can simply type-check the term.
2017-09-08	Fix the introduction of SSR refman chapter.	Théo Zimmermann

2017-09-08	Parse directly to Sorts.family when appropriate.	Gaëtan Gilbert
	When we used to parse to a glob_sort but always give an empty list in the GType case we can now parse directly to Sorts.family.
2017-09-08	Move README.ci and link to it from CONTRIBUTING.	Théo Zimmermann

2017-09-08	Update CI policy.	Théo Zimmermann

2017-09-08	Fix coq/ltac2#27: ... is not a particularly helpful printing of an error ↵	Pierre-Marie Pédrot
	message.
2017-09-08	Fix coq/ltac2#24: There should be a way to turn an exn into a message.	Pierre-Marie Pédrot

2017-09-08	Fix coq/ltac2#22: Argument to Tactic_failure should be printed.	Pierre-Marie Pédrot
	We implement a printer for toplevel values and use it for exceptions in particular.
2017-09-07	Slightly better printing for anonymous closures.	Pierre-Marie Pédrot

2017-09-07	Fix coq/ltac2#21: Backtraces should print Ltac2 closures.	Pierre-Marie Pédrot

2017-09-07	Merge PR #997: coqdoc: Support comments in verbatim output	Maxime Dénès

2017-09-07	Fix BZ#5655 by avoiding the creation of a cleaner thread for empty queues.	Maxime Dénès
	While this is a good workaround, Enrico has a minimal example of the underlying issue that we will send to the OCaml team.
2017-09-07	Merge PR #1016: 2 Typos in 'Add Parametric Morphism' Documentation	Maxime Dénès

2017-09-07	Merge PR #968: Better error messages on the CI	Maxime Dénès

2017-09-07	dev/build/windows/makecoq_mingw.sh: install camlp5's META file	Enrico Tassi

2017-09-07	Merge PR #931: Parametrize module body	Maxime Dénès

2017-09-07	Merge PR #914: Making the detyper lazy	Maxime Dénès

2017-09-07	Merge PR #904: Add build_coq_or to API.Coqlib	Maxime Dénès

2017-09-07	Trying to properly propagate errors in Windows CI script.	Maxime Dénès

2017-09-07	Communicate the backtrace through the monad.	Pierre-Marie Pédrot

2017-09-06	Fix coq/ltac2#23: Int.compare should not be uniformly 0.	Pierre-Marie Pédrot
	Stupid typo.
2017-09-06	Using higher-order representation for closures.	Pierre-Marie Pédrot

2017-09-06	Parameterizing over parameters in ML functions from Tac2core.	Pierre-Marie Pédrot

2017-09-06	The interp_app function now takes a closure as an argument.	Pierre-Marie Pédrot

2017-09-06	Moving Tac2ffi before Tac2interp.	Pierre-Marie Pédrot

2017-09-06	Introducing abstract data representations.	Pierre-Marie Pédrot

2017-09-06	use get_arguments, String.concat, remove -I	Paul Steckler

2017-09-06	Fix a refine anomaly "Evar defined twice".	Pierre-Marie Pédrot
	Because the argument given to refine may mess with the evarmap, the goal being refined can be solved by side-effect after the term filler is computed. If this happens, we simply don't perform the refining operation.
2017-09-06	Code factorization.	Pierre-Marie Pédrot

2017-09-06	weakens an hypothesis of Rle_Rpower	Yves Bertot