aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Exporting some functions of vars.ml as functions operating on EConstr.Gravatar Hugo Herbelin2017-05-19
|
* In EConstr, defining some "cast" functions earlier.Gravatar Hugo Herbelin2017-05-19
| | | | | | This allows to use a cast in subst_of_rel_context_instance. Also added more cast functions for further use.
* Moving "sym" on "eq" type to lib/util.ml.Gravatar Hugo Herbelin2017-05-19
|
* Moving code for miscellaneous tests to specific files.Gravatar Hugo Herbelin2017-05-10
| | | | | | | | | | | | | | | | | | The rule is that any file misc/*.sh will now be automatically executed from the test-file directory with appropriate environment variables set. The test can use any auxiliary material which is put in a directory of the same name as the test. This avoids making the main Makefile more or more complex. We loose some customization though (no more custom messages such as printing of the number of universes in the test about the number of necessary universes). We could preserve such customization if needed but I did not consider it was worth the effort. Warning: specific targets universes, deps-order, deps-checksum are removed by consistency. Do instead "make misc/universes.log", etc., or even "make misc" for all.
* A more regular naming of variables in test-suite Makefile.Gravatar Hugo Herbelin2017-05-10
|
* Adding tests for testing exit status and #use"include".Gravatar Hugo Herbelin2017-05-10
|
* Cleaning old untested not any more interesting testing files.Gravatar Hugo Herbelin2017-05-10
|
* 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
|\ \ \ \ \
* \ \ \ \ \ 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
| | | | | | | | |
| | * | | | | | | Fix two new unused opens.Gravatar Maxime Dénès2017-05-02
| | | | | | | | |
| | * | | | | | | Remove unused module definition after merging PR#592.Gravatar Maxime Dénès2017-05-02
| |/ / / / / / / |/| | | | | | |
* | | | | | | | Merge PR#592: Fix bug #5501: Universe polymorphism breaks proof involving auto.Gravatar Maxime Dénès2017-05-02
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR#582: Fix warningsGravatar Maxime Dénès2017-05-02
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR#596: Fix for bug 5507. Mispelt de Bruijn.Gravatar Maxime Dénès2017-05-02
|\ \ \ \ \ \ \ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 05:28:05 +0000