| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-05-05 | Merge PR#605: Report a useful error for dependent induction | Maxime Dénès | |
| 2017-05-05 | Merge PR#454: Printing unfocussed goals and toward a pg plugin. | Maxime Dénès | |
| 2017-05-05 | Merge PR#593: Functional choice <-> [inhabited] and [forall] commute | Maxime Dénès | |
| 2017-05-05 | Remove unused open. | Maxime Dénès | |
| 2017-05-05 | Merge PR#544: Anonymous universes | Maxime Dénès | |
| 2017-05-04 | Warning removed. | Pierre Courtieu | |
| 2017-05-04 | labelizing arguments | Pierre Courtieu | |
| 2017-05-04 | Adding an option "Printing Unfocused". | Pierre Courtieu | |
| Off by default. + small refactoring of emacs hacks in printer.ml. | |||
| 2017-05-03 | Merge PR#541: Fixing "decide equality" bug #5449 | Maxime Dénès | |
| 2017-05-03 | Merge PR#588: Allow interactive editing of {C,}Morphisms in PG | Maxime Dénès | |
| 2017-05-03 | Merge PR#386: Better editing of the standard library in coqtop/PG | Maxime Dénès | |
| 2017-05-03 | Merge PR#602: Fix more warnings | Maxime Dénès | |
| 2017-05-03 | Merge PR#404: patch for printing types of let bindings | Maxime Dénès | |
| 2017-05-03 | Report a useful error for dependent induction | Tej Chajed | |
| The dependent induction tactic notation is in the standard library but not loaded by default, leading to a parser error message that is confusing and unhelpful. This commit adds a notation for dependent induction to Init that fails and reports [Require Import Coq.Program.Equality.] is required to use [dependent induction]. | |||
| 2017-05-03 | Reorganize comment documentation of ChoiceFacts.v | Gaetan Gilbert | |
| Shortnames and natural language descriptions of principles are moved next to each principle. The table of contents is moved to after the principle definitions. Extra definitions are moved to the definition section (eg DependentFunctionalChoice) Compatibility notations have been moved to the end of the file. Details: The following used to be announced but were neither defined or used, and have been removed: - OAC! - Ext_pred = extensionality of predicates - Ext_fun_prop_repr = choice of a representative among extensional functions to Prop GuardedFunctionalRelReification was announced with shortname GAC! but shortname GFR_fun was used next to it. Only the former has been retained. Shortnames and descriptions have been invented for InhabitedForallCommute DependentFunctionalRelReification ExtensionalPropositionRepresentative ExtensionalFunctionRepresentative Some modification of headlines | |||
| 2017-05-03 | Type@{_} should not produce a flexible algebraic universe. | Gaetan Gilbert | |
| Otherwise [(fun x => x) (Type : Type@{_})] becomes [(fun x : Type@{i+1} => x) (Type@{i} : Type@{i+1})] breaking the invariant that terms do not contain algebraic universes (at the lambda abstraction). | |||
| 2017-05-03 | Allow flexible anonymous universes in instances and sorts. | Gaetan Gilbert | |
| The addition to the test suite showcases the usage. | |||
| 2017-05-03 | Merge PR#411: Mention template polymorphism in the documentation. | Maxime Dénès | |
| 2017-05-02 | applied the patch for printing types of let bindings by @herbelin | Abhishek Anand (@brixpro-home) | |
| 2017-05-02 | Remove dead code in native compiler. | Maxime Dénès | |
| 2017-05-02 | Fix two new unused opens. | Maxime Dénès | |
| 2017-05-02 | Remove unused module definition after merging PR#592. | Maxime Dénès | |
| 2017-05-02 | Merge PR#592: Fix bug #5501: Universe polymorphism breaks proof involving auto. | Maxime Dénès | |
| 2017-05-02 | Merge PR#582: Fix warnings | Maxime Dénès | |
| 2017-05-02 | Merge PR#596: Fix for bug 5507. Mispelt de Bruijn. | Maxime Dénès | |
| 2017-05-02 | Merge PR#595: Avoiding registering files from _build_ci for computing ↵ | Maxime Dénès | |
| dependencies | |||
| 2017-05-01 | More consistent writing of de Bruijn. | Théo Zimmermann | |
| 2017-05-01 | Fix for bug 5507. Mispelt de Bruijn. | Théo Zimmermann | |
| 2017-05-01 | Avoiding registering files from _build_ci when not calling Makefile.ci. | Hugo Herbelin | |
| 2017-04-30 | Functional choice <-> [inhabited] and [forall] commute | Gaetan Gilbert | |
| 2017-04-30 | Fix bug #5501: Universe polymorphism breaks proof involving auto. | Pierre-Marie Pédrot | |
| A universe substitution was lacking as the normalized evar map was dropped. | |||
| 2017-04-30 | Fixing "decide equality"'s bug #5449. | Hugo Herbelin | |
| The code was assuming that the terms t and u for which {t=u}+{t<>u} is proved were distinct. We refine an internal "generalize" of "u" so that it works on the two precise occurrences to abstract, even if other occurrences of u occur as subterm of t too. We also reuse the global constants found in the statement rather than reconstructing them (this seems better in case the global constants eventually get polymorphic universes?). | |||
| 2017-04-29 | Suppress warning message in stdlib. | Guillaume Melquiond | |
| 2017-04-28 | Revert "Renaming allow_patvar flag of intern_gen into pattern_mode." | Maxime Dénès | |
| This reverts commit 7bdfa1a4e46acf11d199a07bfca0bc59381874c3. | |||
| 2017-04-28 | Revert "Using a more explicit algebraic type for evars of kind "MatchingVar"." | Maxime Dénès | |
| I'm sure this was pushed by accident, since testing shows immediately that it breaks the compilation of the ssreflect plugin, hence all developments relying on it in Travis. | |||
| 2017-04-28 | Allow interactive editing of {C,}Morphisms in PG | Jason Gross | |
| 2017-04-28 | Add .dir-locals.el and _CoqProject files for emacs stdlib editing | Jason Gross | |
| These set up PG to use the local coqtop, and the local coqlib, when editing files in the stdlib. As per https://github.com/coq/coq/pull/386#issuecomment-279012238, we can use `_CoqProject` for `theories/Init`, and this allows CoqIDE to edit those files. However, we cannot use it for `theories/`, because a `_CoqProject` file will override a `.dir-locals.el` in the same directory, and there is no way to get PG to pick up a valid `-coqlib` from `_CoqProject` (because it'll take the path relative to the current directory, not relative to the directory of `_CoqProject`). | |||
| 2017-04-28 | Using a more explicit algebraic type for evars of kind "MatchingVar". | Hugo Herbelin | |
| A priori considered to be a good programming style. | |||
| 2017-04-28 | Renaming allow_patvar flag of intern_gen into pattern_mode. | Hugo Herbelin | |
| This highlights that this is a binary mode changing the interpretation of "?x" rather than additionally allowing patvar. | |||
| 2017-04-28 | Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of ↵ | Maxime Dénès | |
| let-ins | |||
| 2017-04-27 | Post-rebase warnings (unused opens and 2 unused values) | Gaetan Gilbert | |
| 2017-04-27 | Enable more warnings, and add -warn-error configure flag | Gaetan Gilbert | |
| 2017-04-27 | Fix 4.04 warnings | Gaetan Gilbert | |
| 2017-04-27 | Remove uses of [Flags.make_silent] | Gaetan Gilbert | |
| 2017-04-27 | Warning 29: non escaped end of line may be non portable | Gaetan Gilbert | |
| 2017-04-27 | Remove unused [open] statements | Gaetan Gilbert | |
| 2017-04-27 | Micromega: do not use Filename.temp_dir_path, remove unused values | Gaetan Gilbert | |
| 2017-04-27 | Remove unused constructors | Gaetan Gilbert | |
| 2017-04-27 | Add [_] prefix to unused values which maybe should be kept | Gaetan Gilbert | |
| 2017-04-27 | Remove some unused values and types | Gaetan Gilbert | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |