coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
* \|	Boxing the Goal.enter primitive into a record type.	Pierre-Marie Pédrot	2015-10-20
\| \|
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-19
\|\\|
* \|	Type delayed_open_constr is now monotonic.	Pierre-Marie Pédrot	2015-10-19
\| \|
* \|	Function debug mode more formatted.	Pierre Courtieu	2015-10-19
\| \|
\| *	Partly fixes #3225. Removed some old experimental stuff in funind.	Pierre Courtieu	2015-10-19
\| \|
* \|	Constraining refine to monotonic functions.	Pierre-Marie Pédrot	2015-10-18
\| \|
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-15
\|\\|
\| *	Exporting the original unprocessed hint in the hint running function.	Pierre-Marie Pédrot	2015-10-14
\| \|
\| *	Fix some typos.	Guillaume Melquiond	2015-10-13
\| \|
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-09
\|\\|
\| *	f_equal fix continued: do a refresh_universes as before.	Matthieu Sozeau	2015-10-08
\| \|
\| *	Fix bug #4069: f_equal regression.	Matthieu Sozeau	2015-10-07
\| \|
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-02
\|\\|
\| *	Univs: fix after rebase (from_ctx/from_env)	Matthieu Sozeau	2015-10-02
\| \|
\| *	Univs: fix evar_map initialization in newring.	Matthieu Sozeau	2015-10-02
\| \|
\| *	Univs: fix evar_map leaks bugs in Function	Matthieu Sozeau	2015-10-02
\| \| \| \| \| \| \| \| \| \| \| \|	The evar_map's that are used to typecheck terms must now always be initialized with the global universe graphs using Evd.from_env, so any failure to initialize and thread evar_map's correctly results in errors.
\| *	Univs: fix an evar leak in congruence	Matthieu Sozeau	2015-10-02
\| \|
* \|	Removing uselessly duplicated function in Evd.	Pierre-Marie Pédrot	2015-09-27
\| \|
* \|	Merge branch 'v8.5' into trunk	Maxime Dénès	2015-09-17
\|\\|
\| *	Univs: Add universe binding lists to definitions	Matthieu Sozeau	2015-09-14
\| \| \| \| \| \| \| \| \| \|	... lemmas and inductives to control which universes are bound and where in universe polymorphic definitions. Names stay outside the kernel.
* \|	Opacifying the proof_terminator type.	Pierre-Marie Pédrot	2015-09-08
\| \|
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-09-06
\|\\|
\| *	Improve directives for Haskell extraction of nat.	Maxime Dénès	2015-09-03
\| \|
\| *	Fix [Z.div] and add [Z.modulo] in ExtrHaskellZNum.v	Nickolai Zeldovich	2015-09-03
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The previous extraction of [Z.div] for Haskell did not properly handle divide-by-zero. Fix it by introducing an explicit [if] statement in the generated Haskell code. Also, introduce a similar extraction rule for [Z.modulo], with the same check for modulo-by-zero.
\| *	Fix [Nat.div] and add [Nat.modulo] in ExtrHaskellNatNum.v	Nickolai Zeldovich	2015-09-03
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The previous extraction of [Nat.div] for Haskell did not properly handle divide-by-zero. Fix it by introducing an explicit [if] statement in the generated Haskell code. Also, introduce a similar extraction rule for [Nat.modulo], with the same check for modulo-by-zero.
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-07-27
\|\\|
\| *	Extraction: fix primitive projection extraction.	Matthieu Sozeau	2015-07-22
\| \| \| \| \| \| \| \|	Use expand projection to come back to the projection-as-constant encoding, dealing with parameters correctly.
* \|	Merge branch 'v8.5' into trunk	Pierre Letouzey	2015-06-22
\|\\|
\| *	Add efficient extraction of [nat], [Z], and [string] to Haskell	Nickolai Zeldovich	2015-06-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This mirrors the existing extraction libraries for OCaml. One wart: the extraction for [string] requires that the Haskell code imports Data.Bits and Data.Char. Coq has no way to add extra import statements to the extracted code. So we have to rely on the user to somehow import these libraries (e.g., using the -pgmF ghc option). See also https://coq.inria.fr/bugs/show_bug.cgi?id=4189 Message to github robot: this commit closes #65
* \|	micromega : fix silly timeout	Frédéric Besson	2015-06-06
\| \|
* \|	micromega : options to limit proof search	Frédéric Besson	2015-05-26
\| \|
* \|	Merge v8.5 into trunk	Hugo Herbelin	2015-05-15
\|\\| \| \| \| \| \| \| \| \| \| \| \| \|	Conflicts: tactics/eauto.ml4 (merging eauto.ml4 and adapting coq_micromega.ml to new typing.ml API)
\| *	Safer typing primitives.	Pierre-Marie Pédrot	2015-05-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Some functions from pretyping/typing.ml and their derivatives were potential source of evarmap leaks, as they dropped their resulting evarmap. This commit clarifies the situation by renaming them according to a unsafe_* scheme. Their sound variant is likewise renamed to their old name. The following renamings were made. - Typing.type_of -> unsafe_type_of - Typing.e_type_of -> type_of - A new e_type_of function that matches the e_ prefix policy - Tacmach.pf_type_of -> pf_unsafe_type_of - A new safe pf_type_of function. All uses of unsafe_* functions should be eventually eliminated.
\| *	Rationalizing a bit the interface of Hints.	Pierre-Marie Pédrot	2015-05-11
\| \|
\| *	Fix bug #4212, congruence forgetting about some universe constraints.	Matthieu Sozeau	2015-05-05
\| \|
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-05-05
\|\\|
* \|	maintenance micromega plugin	Frédéric Besson	2015-04-28
\| \| \| \| \| \| \| \| \| \| \| \|	- add a nra tactic (similar to nia) for non-linear real arithmetic tactic - fix a long-standing bug in the reification code - port to the new proof-engine
\| *	Remove almost all the uses of string concatenation when building error messages.	Guillaume Melquiond	2015-04-23
\| \| \| \| \| \| \| \| \| \| \| \|	Since error messages are ultimately passed to Format, which has its own buffers for concatenating strings, using concatenation for preparing error messages just doubles the workload and increases memory pressure.
\| *	Using tclZEROMSG instead of tclZERO in several places.	Pierre-Marie Pédrot	2015-04-23
\| \|
\| *	Declarative mode: remaining goals are "given up" when closing blocks.	Arnaud Spiwack	2015-04-22
\| \| \| \| \| \|	Restores the intended behaviour from v8.3 and earlier.
\| *	Remove dirty debug printing from funind.	Maxime Dénès	2015-04-15
\| \|
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-04-15
\|\\|
\| *	Function now supports puniveres	jforest	2015-04-14
\| \|
\| *	better debug in recdef	jforest	2015-04-14
\| \|
\| *	Opaque implementation of auto tactics.	Pierre-Marie Pédrot	2015-04-14
\| \| \| \| \| \| \| \| \| \| \| \|	We provide an eliminator ensuring that the AST will be used to build a tactic, so that we can stuff arbitrary things inside. An escape function is also provided for backward compatibility.
\| *	correction of a bug reported by Tristan Crolard	jforest	2015-04-13
\| \|
\| *	Fixing bug #4186.	Pierre-Marie Pédrot	2015-04-13
\| \|
\| *	Fix #3590 for good this time, by changing the API, change's argument now	Matthieu Sozeau	2015-04-10
\| \| \| \| \| \| \| \| \| \| \| \|	takes a variable substitution for matched variables in the (lhs) pattern, and uses the existing ist structure to pretype the rhs correcly, without having to deal with the volatile evars.
* \|	Merge branch 'v8.5' into trunk	Pierre Letouzey	2015-04-09
\|\\|
\| *	JSON extraction: make explicit each group of mutually-recursive fixpoints	Nickolai Zeldovich	2015-04-09
\| \|