coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Squashed commit of the following:	Amin Timany	2017-06-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Except I have disabled the minimization of universes after sections as it seems to interfere with the STM machinery causing files like test-suite/vio/print.v to loop when processed asynchronously. This is very peculiar and needs more investigation as the aforementioned file does not have any sections or any universe polymorphic definitions! commit fc785326080b9451eb4700b16ccd3f7df214e0ed Author: Amin Timany <amintimany@gmail.com> Date: Mon Apr 24 17:14:21 2017 +0200 Revert STL to monomorphic commit 62b573fb13d290d8fe4c85822da62d3e5e2a6996 Author: Amin Timany <amintimany@gmail.com> Date: Mon Apr 24 17:02:42 2017 +0200 Try unifying universes before apply subtyping commit ff393742c37b9241c83498e84c2274967a1a58dc Author: Amin Timany <amintimany@gmail.com> Date: Sun Apr 23 13:49:04 2017 +0200 Compile more of STL with universe polymorphism commit 5c831b41ebd1fc32e2dd976697c8e474f48580d6 Author: Amin Timany <amintimany@gmail.com> Date: Tue Apr 18 21:26:45 2017 +0200 Made more progress on compiling the standard library commit b8550ffcce0861794116eb3b12b84e1158c2b4f8 Author: Amin Timany <amintimany@gmail.com> Date: Sun Apr 16 22:55:19 2017 +0200 Make more number theoretic modules monomorphic commit 29d126d4d4910683f7e6aada2a25209151e41b10 Author: Amin Timany <amintimany@gmail.com> Date: Fri Apr 14 16:11:48 2017 +0200 WIP more of standard library compiles Also: Matthieu fixed a bug in rewrite system which was faulty when introducing new morphisms (Add Morphism) command. commit 23bc33b843f098acaba4c63c71c68f79c4641f8c Author: Amin Timany <amintimany@gmail.com> Date: Fri Apr 14 11:39:21 2017 +0200 WIP: more of the standard library compiles We have implemented convertibility of constructors up-to mutual subtyping of their corresponding inductive types. This is similar to the behavior of template polymorphism. commit d0abc5c50d593404fb41b98d588c3843382afd4f Author: Amin Timany <amintimany@gmail.com> Date: Wed Apr 12 19:02:39 2017 +0200 WIP: trying to get the standard library compile with universe polymorphism We are trying to prune universes after section ends. Sections add a load of universes that are not appearing in the body, type or the constraints.
*	Make unification use subtyping info of inductives	Amin Timany	2017-06-16
\|
*	Fix cum/conv for inductive types	Amin Timany	2017-06-16
\| \| \| \| \|	Fall back to the equating levels in case inductive is not fully applied instead of failing.
*	Use inductive subtyping for conv/cumul	Amin Timany	2017-06-16
\|
*	Change the place of inference after sect discharge	Amin Timany	2017-06-16
\|
*	Subtyping inference for inductoves and records	Amin Timany	2017-06-16
\| \| \| \|	Also reinferred after sections discharge
*	Add subtyping inference for inductive types	Amin Timany	2017-06-16
\|
*	Correct subtyping check for constructors	Amin Timany	2017-06-16
\|
*	Fix typo in error message	Amin Timany	2017-06-16
\|
*	Check subtyping of inductive types in Kernel	Amin Timany	2017-06-16
\|
*	Using UInfoInd for universes in inductive types	Amin Timany	2017-06-16
\| \| \| \| \| \| \| \| \|	It stores both universe constraints and subtyping information for blocks of inductive declarations. At this stage the there is no inference or checking implemented. The subtyping information simply encodes equality of levels for the condition of subtyping.
*	New datastructure for universes of inductive types	Amin Timany	2017-06-16
\|
*	Extend definition of inductives to include subtyping info	Amin Timany	2017-06-16
\|
*	Merge PR#748: [stm] More fixes for nested commands [bugzilla 5589]	Maxime Dénès	2017-06-15
\|\
* \	Merge PR#778: Revert "[travis] temporary UniMath overlay"	Maxime Dénès	2017-06-15
\|\ \
* \ \	Merge PR#719: Constrexpr.Numeral without bigint	Maxime Dénès	2017-06-15
\|\ \ \
* \ \ \	Merge PR#769: [lib] Remove obsolete state-management function add_frozen_state	Maxime Dénès	2017-06-15
\|\ \ \ \
* \| \| \| \|	fix dev/base_include (thanks Zimmi48)	Pierre Letouzey	2017-06-15
\| \| \| \| \|
* \| \| \| \|	Makefile.build : restore (temporarily?) the anti-cmi-corruption hacks	Pierre Letouzey	2017-06-15
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Due to the recent conversion of many .mli-only files into .ml files (hugely debatable impact of the API introduction), parallel make may fail badly again (always the same race between ocamlc and ocamlopt for .cmi). Still working on a proper fix, but meanwhile let's reintroduce the old hacks against these corruptions.
* \| \| \| \|	Merge PR#375: Deprecation	Maxime Dénès	2017-06-15
\|\ \ \ \ \
* \| \| \| \| \|	Move Fiat to allowed failures.	Maxime Dénès	2017-06-15
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	For now, Fiat still relies on 8.4 compatibility.
* \| \| \| \| \|	Remove bedrock from test suite.	Maxime Dénès	2017-06-15
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Bedrock relies on the 8.4 compat flag that we are removing, and we heard from MIT that they did not plan to port bedrock to more recent versions of Coq.
* \| \| \| \| \|	Remove dependency on -compat flag in coq_makefile test suite.	Maxime Dénès	2017-06-15
\| \| \| \| \| \|
* \| \| \| \| \|	Merge PR#749: Normalize deprecation notices of ./configure	Maxime Dénès	2017-06-14
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR#753: Fix bug 5026 (the stdlib shouldn't define inconsistent notations).	Maxime Dénès	2017-06-14
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR#758: [toplevel] Print error header on fatal batch error.	Maxime Dénès	2017-06-14
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR#763: [proof] Deprecate redundant wrappers.	Maxime Dénès	2017-06-14
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR#765: Remove obsolete Show commands	Maxime Dénès	2017-06-14
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR#739: completing a sentence in a comment	Maxime Dénès	2017-06-14
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR#738: [kernel] Improve proof using message, fixes bugzilla #3613	Maxime Dénès	2017-06-14
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").	Maxime Dénès	2017-06-14
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR#673: Two fixes about zify (bugs #5336 and #5439)	Maxime Dénès	2017-06-14
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR#448: Do not recompute twice the whnf of terms in conversion.	Maxime Dénès	2017-06-14
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR#622: Change the default flag value for Refine.refine	Maxime Dénès	2017-06-14
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR#703: New version of the selective-unfolding PR	Maxime Dénès	2017-06-14
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR#771: [travis overlay] Partially Revert 013c0232953f1f58	Maxime Dénès	2017-06-14
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[print] Allow Selective Printing of Notations	Emilio Jesus Gallego Arias	2017-06-14
\| \|/ / / / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We add new API to the printer to allows toggling the printing of individual notations and scopes: ```ocaml val toggle_scope_printing : scope:Notation_term.scope_name -> activate:bool -> unit val toggle_notation_printing : ?scope:Notation_term.scope_name -> notation:Constrexpr.notation -> activate:bool -> unit ``` This API is meant to be used by ML plugins. [this commit includes some refactoring by EJGA]
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Temporary overlays because fewer plugins are loaded at startup.	Maxime Dénès	2017-06-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR#220: Less init plugins	Maxime Dénès	2017-06-14
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[travis] overlay for fiat-crypto (a Require Import FunInd)	Pierre Letouzey	2017-06-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[travis] overlays for CompCert and VST (an extra Require Export FunInd)	Pierre Letouzey	2017-06-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[travis] fix Software Foundation (one added Require Extraction)	Pierre Letouzey	2017-06-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[travis] fix CoLoR by inserting some Require Import FunInd	Pierre Letouzey	2017-06-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Recdef do now a Require Export FunInd (better compat)	Pierre Letouzey	2017-06-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Grammar hacks to get nice errors about non-loaded plugins (extr,recdef)	Pierre Letouzey	2017-06-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Since previous commit, some plugins are not loaded initially anymore : extraction, funind. To ease this transition toward a mandatory Require, we hack here the vernac grammar in order to get customized error messages telling what to Require instead of the dreadful "Illegal begin of vernac". Normally, these fake grammar entries are overloaded later by the grammar extensions in these plugins. This code is meant to be removed in a few releases, when this transition is considered finished. NB : In a first attempt, a similar trick was tried in g_tactics.ml4 to provide customized error message for "functional induction" and "functional inversion", but this was leading to anomalies.
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	API: exports Mltop.module_is_known to both API.mli and grammar_API.mli	Pierre Letouzey	2017-06-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Prelude : no more autoload of plugins extraction and recdef	Pierre Letouzey	2017-06-14
\|/ / / / / / / / / / / / / / / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The user now has to manually load them, respectively via: Require Extraction Require Import FunInd The "Import" in the case of FunInd is to ensure that the tactics functional induction and functional inversion are indeed in scope. Note that the Recdef.v file is still there as well (it contains complements used when doing Function with measures), and it also triggers a load of FunInd.v. This change is correctly documented in the refman, and the test-suite has been adapted.
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Makefile.build : cleanup now that micromega.ml isn't generated + sync check ↵	Pierre Letouzey	2017-06-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	of this file There is now a warning if the content of micromega.ml isn't what MExtraction.v would produce.
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	Notation.declare_rawnumeral_interpreter	Pierre Letouzey	2017-06-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This new function is similar to declare_numeral_interpreter, but works on a lower level : instead of bigint, numbers are represented as string of their decimal digits (plus a boolean sign)
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	G_prim: the bigint entry keeps numbers in raw strings	Pierre Letouzey	2017-06-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|