aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Uniformity of style for selecting plural or not; spacing for comma.Gravatar Hugo Herbelin2017-05-13
|
* Typo in a comment of plugin Quote.Gravatar Hugo Herbelin2017-05-13
|
* Aligning on standard layout of CHANGES.Gravatar Hugo Herbelin2017-05-13
|
* Merge PR#594: An example showing the benefit of EconstrGravatar Maxime Dénès2017-05-11
|\
* \ Merge PR#373: A refined solution to the beta-iota discrepancies between 8.4 ↵Gravatar Maxime Dénès2017-05-11
|\ \ | | | | | | | | | and 8.5/8.6 "refine"
* \ \ Merge PR#572: Replacing costly merges in UGraph.Gravatar Maxime Dénès2017-05-11
|\ \ \
* | | | Remove an unused open introduced by the previous commit.Gravatar Maxime Dénès2017-05-11
| | | |
* | | | Merge PR#201: Transparent abstractGravatar Maxime Dénès2017-05-11
|\ \ \ \
* \ \ \ \ Merge PR#619: Fix warnings in top_printersGravatar Maxime Dénès2017-05-09
|\ \ \ \ \
* \ \ \ \ \ Merge PR#612: Set Ltac Batch DebugGravatar Maxime Dénès2017-05-09
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR#606: Added an option Set Debug CbvGravatar Maxime Dénès2017-05-09
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR#621: Prevent user-defined ring morphisms from ever being evaluated.Gravatar Maxime Dénès2017-05-09
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR#615: coqtop -help: don't die if coqlib can't be foundGravatar Maxime Dénès2017-05-09
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR#617: [toplevel] Fix a couple of logical errors in error printing.Gravatar Maxime Dénès2017-05-09
|\ \ \ \ \ \ \ \ \ \
| | | * | | | | | | | Prevent user-defined ring morphisms from ever being evaluated.Gravatar Guillaume Melquiond2017-05-09
| |_|/ / / / / / / / |/| | | | | | | | |
| | | | | * | | | | Fix warnings in top_printersGravatar Gaetan Gilbert2017-05-08
| |_|_|_|/ / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Note that [@@@ocaml.warning "-32"] caused an error with Drop. It was put there because I didn't realise the warning was about a real issue.
| * | | | | | | | [toplevel] Fix a couple of logical errors in error printing.Gravatar Emilio Jesus Gallego Arias2017-05-05
|/ / / / / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In 4abb41d008fc754f21916dcac9cce49f2d04dd6d we switched back to use exceptions for error printing. However a couple of mistakes were present in that commit: - We wrongly absorbed the exception on `Vernac.compile`. However, it should be propagated as the caller will correctly print the error now. This introduced a critical bug as now `coqc` return the wrong exit status on error, breaking all sort of things. - We printed parsing exceptions twice; now it is not necessary to print the exception in the parsing handler as it will be propagated. I've checked this commit versus all previously reported bugs and it seems to work; we should definitively add a test-suite case to check that the exit code of `coqc` is correct, plus several other cases such as bugs https://coq.inria.fr/bugs/show_bug.cgi?id=5467 https://coq.inria.fr/bugs/show_bug.cgi?id=5485 https://coq.inria.fr/bugs/show_bug.cgi?id=5484 etc... See also PR #583
* | | | | | | | Remove dead code and unused open.Gravatar Maxime Dénès2017-05-05
| | | | | | | |
* | | | | | | | Merge PR#558: Adding a fold_glob_constr_with_binders combinatorGravatar Maxime Dénès2017-05-05
|\ \ \ \ \ \ \ \
* | | | | | | | | Remove two unused opens.Gravatar Maxime Dénès2017-05-05
| | | | | | | | |
* | | | | | | | | Merge PR#598: Removing dead code in Autorewrite.Gravatar Maxime Dénès2017-05-05
|\ \ \ \ \ \ \ \ \
| | | | | | | | | * Documenting Option.List.find.Gravatar Hugo Herbelin2017-05-05
| | | | | | | | | |
| | | | | | | | | * Cosmetic: unifying style within option.ml.Gravatar Hugo Herbelin2017-05-05
| | | | | | | | | |
| | | | | | | | | * Upgrading some local function as a general-purpose combinator Option.List.map.Gravatar Hugo Herbelin2017-05-05
| | | | | | | | | |
| | | | | | | | | * Adding a test-suite pattern-unification example that Econstr fixed.Gravatar Hugo Herbelin2017-05-05
| |_|_|_|_|_|_|_|/ |/| | | | | | | |
* | | | | | | | | Merge PR#610: Improve documentation of assert / pose proof / specialize.Gravatar Maxime Dénès2017-05-05
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR#605: Report a useful error for dependent inductionGravatar Maxime Dénès2017-05-05
|\ \ \ \ \ \ \ \ \ \
| | | | | * | | | | | coqtop -help: don't die if coqlib can't be foundGravatar Gaetan Gilbert2017-05-05
| |_|_|_|/ / / / / / |/| | | | | | | | |
* | | | | | | | | | Merge PR#454: Printing unfocussed goals and toward a pg plugin.Gravatar Maxime Dénès2017-05-05
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR#593: Functional choice <-> [inhabited] and [forall] commuteGravatar Maxime Dénès2017-05-05
|\ \ \ \ \ \ \ \ \ \ \
* | | | | | | | | | | | Remove unused open.Gravatar Maxime Dénès2017-05-05
| | | | | | | | | | | |
* | | | | | | | | | | | Merge PR#544: Anonymous universesGravatar Maxime Dénès2017-05-05
|\ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | * | | | Adding an option "Set Ltac Batch Debug" to additionally run Ltac debug in ↵Gravatar Hugo Herbelin2017-05-04
| |_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | batch mode.
| | | | | * | | | | | | Improve documentation of assert / pose proof / specialize.Gravatar Théo Zimmermann2017-05-04
| |_|_|_|/ / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commits documents the as clause of specialize and that the as clause of pose proof is optional. It also mentions a feature of assert ( := ) that was available since 8.5 and was mentionned by @herbelin in: https://github.com/coq/coq/pull/248#issuecomment-297970503
| | | * | | | | | | | Warning removed.Gravatar Pierre Courtieu2017-05-04
| | | | | | | | | | |
| | | * | | | | | | | labelizing argumentsGravatar Pierre Courtieu2017-05-04
| | | | | | | | | | |
| | | * | | | | | | | Adding an option "Printing Unfocused".Gravatar Pierre Courtieu2017-05-04
| |_|/ / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Off by default. + small refactoring of emacs hacks in printer.ml.
* | | | | | | | | | Merge PR#541: Fixing "decide equality" bug #5449Gravatar Maxime Dénès2017-05-03
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR#588: Allow interactive editing of {C,}Morphisms in PGGravatar Maxime Dénès2017-05-03
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR#386: Better editing of the standard library in coqtop/PGGravatar Maxime Dénès2017-05-03
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR#602: Fix more warningsGravatar Maxime Dénès2017-05-03
|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR#404: patch for printing types of let bindingsGravatar Maxime Dénès2017-05-03
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | * | | | Added an option Set Debug Cbv.Gravatar Hugo Herbelin2017-05-03
| |_|_|_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | |
| | | | | | | | * | | | | | Report a useful error for dependent inductionGravatar Tej Chajed2017-05-03
| |_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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].
| | | | | | | * | | | | | Reorganize comment documentation of ChoiceFacts.vGravatar Gaetan Gilbert2017-05-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
| | | | | | * | | | | | | Type@{_} should not produce a flexible algebraic universe.Gravatar Gaetan Gilbert2017-05-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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).
| | | | | | * | | | | | | Allow flexible anonymous universes in instances and sorts.Gravatar Gaetan Gilbert2017-05-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The addition to the test suite showcases the usage.
* | | | | | | | | | | | | Merge PR#411: Mention template polymorphism in the documentation.Gravatar Maxime Dénès2017-05-03
|\ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | |
| | * | | | | | | | | | | applied the patch for printing types of let bindings by @herbelinGravatar Abhishek Anand (@brixpro-home)2017-05-02
| |/ / / / / / / / / / / |/| | | | | | | | | | |
| | * | | | | | | | | | Remove dead code in native compiler.Gravatar Maxime Dénès2017-05-02
| | | | | | | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 21:16:24 +0000