aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-05-16Stop using auto with * in two proofs.Théo Zimmermann
auto with * is an overkill for people who do not care to understand what they really need. In these two cases, one lemma which was available in the typeclass_instances hint db.
2017-05-16Merge PR#626: Add documentation for Set Ltac Batch DebugMaxime Dénès
2017-05-16Merge PR#629: A couple of simple updates for TravisMaxime Dénès
2017-05-13[travis] Update OCaml to 4.04.1Emilio Jesus Gallego Arias
2017-05-13[travis] Move VST to required suite.Emilio Jesus Gallego Arias
2017-05-11Add documentation for Set Ltac Batch DebugJason Gross
2017-05-11Merge PR#594: An example showing the benefit of EconstrMaxime Dénès
2017-05-11Merge PR#373: A refined solution to the beta-iota discrepancies between 8.4 ↵Maxime Dénès
and 8.5/8.6 "refine"
2017-05-11Merge PR#572: Replacing costly merges in UGraph.Maxime Dénès
2017-05-11Remove an unused open introduced by the previous commit.Maxime Dénès
2017-05-11Merge PR#201: Transparent abstractMaxime Dénès
2017-05-09Merge PR#619: Fix warnings in top_printersMaxime Dénès
2017-05-09Merge PR#612: Set Ltac Batch DebugMaxime Dénès
2017-05-09Merge PR#606: Added an option Set Debug CbvMaxime Dénès
2017-05-09Merge PR#621: Prevent user-defined ring morphisms from ever being evaluated.Maxime Dénès
2017-05-09Merge PR#615: coqtop -help: don't die if coqlib can't be foundMaxime Dénès
2017-05-09Merge PR#617: [toplevel] Fix a couple of logical errors in error printing.Maxime Dénès
2017-05-09Prevent user-defined ring morphisms from ever being evaluated.Guillaume Melquiond
2017-05-08Fix warnings in top_printersGaetan 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-05Remove dead code and unused open.Maxime Dénès
2017-05-05Merge PR#558: Adding a fold_glob_constr_with_binders combinatorMaxime Dénès
2017-05-05Remove two unused opens.Maxime Dénès
2017-05-05Merge PR#598: Removing dead code in Autorewrite.Maxime Dénès
2017-05-05Documenting Option.List.find.Hugo Herbelin
2017-05-05Cosmetic: unifying style within option.ml.Hugo Herbelin
2017-05-05Upgrading some local function as a general-purpose combinator Option.List.map.Hugo Herbelin
2017-05-05Adding a test-suite pattern-unification example that Econstr fixed.Hugo Herbelin
2017-05-05Merge PR#610: Improve documentation of assert / pose proof / specialize.Maxime Dénès
2017-05-05Merge PR#605: Report a useful error for dependent inductionMaxime Dénès
2017-05-05coqtop -help: don't die if coqlib can't be foundGaetan Gilbert
2017-05-05Merge PR#454: Printing unfocussed goals and toward a pg plugin.Maxime Dénès
2017-05-05Merge PR#593: Functional choice <-> [inhabited] and [forall] commuteMaxime Dénès
2017-05-05Remove unused open.Maxime Dénès
2017-05-05Merge PR#544: Anonymous universesMaxime Dénès
2017-05-04Adding an option "Set Ltac Batch Debug" to additionally run Ltac debug in ↵Hugo Herbelin
batch mode.
2017-05-04Improve 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-04Warning removed.Pierre Courtieu
2017-05-04labelizing argumentsPierre Courtieu
2017-05-04Adding an option "Printing Unfocused".Pierre Courtieu
Off by default. + small refactoring of emacs hacks in printer.ml.
2017-05-03Merge PR#541: Fixing "decide equality" bug #5449Maxime Dénès
2017-05-03Merge PR#588: Allow interactive editing of {C,}Morphisms in PGMaxime Dénès
2017-05-03Merge PR#386: Better editing of the standard library in coqtop/PGMaxime Dénès
2017-05-03Merge PR#602: Fix more warningsMaxime Dénès
2017-05-03Merge PR#404: patch for printing types of let bindingsMaxime Dénès
2017-05-03Added an option Set Debug Cbv.Hugo Herbelin
2017-05-03Report a useful error for dependent inductionTej 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-03Reorganize comment documentation of ChoiceFacts.vGaetan 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-03Type@{_} 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-03Allow flexible anonymous universes in instances and sorts.Gaetan Gilbert
The addition to the test suite showcases the usage.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 23:09:18 +0000