| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-05-10 | Cleaning old untested not any more interesting testing files. | Hugo Herbelin | |
| 2017-05-09 | Merge PR#619: Fix warnings in top_printers | Maxime Dénès | |
| 2017-05-09 | Merge PR#612: Set Ltac Batch Debug | Maxime Dénès | |
| 2017-05-09 | Merge PR#606: Added an option Set Debug Cbv | Maxime Dénès | |
| 2017-05-09 | Merge PR#621: Prevent user-defined ring morphisms from ever being evaluated. | Maxime Dénès | |
| 2017-05-09 | Merge PR#615: coqtop -help: don't die if coqlib can't be found | Maxime Dénès | |
| 2017-05-09 | Merge PR#617: [toplevel] Fix a couple of logical errors in error printing. | Maxime Dénès | |
| 2017-05-09 | Prevent user-defined ring morphisms from ever being evaluated. | Guillaume Melquiond | |
| 2017-05-08 | Fix warnings in top_printers | Gaetan Gilbert | |
| 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. | |||
| 2017-05-05 | [toplevel] Fix a couple of logical errors in error printing. | Emilio Jesus Gallego Arias | |
| 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 | |||
| 2017-05-05 | Remove dead code and unused open. | Maxime Dénès | |
| 2017-05-05 | Merge PR#558: Adding a fold_glob_constr_with_binders combinator | Maxime Dénès | |
| 2017-05-05 | Remove two unused opens. | Maxime Dénès | |
| 2017-05-05 | Merge PR#598: Removing dead code in Autorewrite. | Maxime Dénès | |
| 2017-05-05 | Merge PR#610: Improve documentation of assert / pose proof / specialize. | Maxime Dénès | |
| 2017-05-05 | Merge PR#605: Report a useful error for dependent induction | Maxime Dénès | |
| 2017-05-05 | coqtop -help: don't die if coqlib can't be found | Gaetan Gilbert | |
| 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 | Adding an option "Set Ltac Batch Debug" to additionally run Ltac debug in ↵ | Hugo Herbelin | |
| batch mode. | |||
| 2017-05-04 | Improve documentation of assert / pose proof / specialize. | Théo Zimmermann | |
| 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 | |||
| 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 | Added an option Set Debug Cbv. | Hugo Herbelin | |
| 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 | Removing dead code in Autorewrite. | Pierre-Marie Pédrot | |
| Since 260965d, an imperative code was semantically the identity because the closure allocation was not performed at the right moment. Because of it intricacy, I cannot really tell the original motivations of this piece of code, although it looks like it was for there for pretty-printing of errors. Anyway, both because the code was dubious and its effect not observed, it cannot hurt to remove it. | |||
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |