| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-09-29 | Typo in coqdep man | Gaëtan Gilbert | |
| 2017-09-29 | Remove some duplication between Typeops and Nativenorm. | Gaëtan Gilbert | |
| 2017-09-28 | Remove trivial TODO comment (constants can't be template poly now). | Gaëtan Gilbert | |
| 2017-09-26 | Merge PR #688: Binding universe constraints in Definition/Inductive/etc... | Maxime Dénès | |
| 2017-09-25 | Merge PR #1085: Fix BZ#5755 (incorrect treatment of let-ins in parameters of ↵ | Maxime Dénès | |
| inductive types) | |||
| 2017-09-25 | Merge PR #1083: Fixing bug in building _rect scheme for inductive types with ↵ | Maxime Dénès | |
| let-ins and non-recursively uniform parameters | |||
| 2017-09-25 | Merge PR #1079: Avoid generated names for html pages of the reference manual ↵ | Maxime Dénès | |
| (bug #4742). | |||
| 2017-09-25 | Merge PR #1068: Fixing #5749 (bug in fold_constr_with_binders introduced in ↵ | Maxime Dénès | |
| 4e70791). | |||
| 2017-09-25 | Merge PR #1057: Reporting locations in error messages about notation formats. | Maxime Dénès | |
| 2017-09-25 | Merge PR #1060: An optimization of tactic constructor | Maxime Dénès | |
| 2017-09-25 | Merge PR #1075: Re-enable checker error messages | Maxime Dénès | |
| 2017-09-23 | Discharge.ml: cosmetic renaming of some variables. | Hugo Herbelin | |
| The point is to emphasize stronglier when we are talking about contexts or about arguments. | |||
| 2017-09-23 | Fixing #5755 (discharging of inductive types not correct with let-ins). | Hugo Herbelin | |
| The number of effective parameters was used where the number of declarations in the signature of parameters should have been used. | |||
| 2017-09-23 | Fixing #5749 (bug in fold_constr_with_binders introduced in 4e70791). | Hugo Herbelin | |
| 2017-09-23 | Fixing _rect bug for inductive types with let-ins and non-rec uniform params. | Hugo Herbelin | |
| The bug was caused by an inconsistency in different part of the code for deciding where cutting the context in between recursively uniform parameters and non-recursively uniform ones when let-ins were in the middle. We fix it by using uniformly "context_chop". | |||
| 2017-09-22 | Avoid generated names for html pages of the reference manual (bug #4742). | Guillaume Melquiond | |
| 2017-09-22 | Merge PR #1055: Remove STM vernaculars | Maxime Dénès | |
| 2017-09-22 | Merge PR #1065: In gitlab set TRAVIS_BRANCH so user overlays will work as ↵ | Maxime Dénès | |
| expected. | |||
| 2017-09-22 | Merge PR #1074: Fix BZ#5750 (recovering ability to print the hole of a ↵ | Maxime Dénès | |
| context obtained by ltac pattern-matching) | |||
| 2017-09-22 | Merge PR #1071: Mark "Set Tactic Compat Context" as deprecated. | Maxime Dénès | |
| 2017-09-22 | Merge PR #1070: Remove remaining occurrences of -just-parsing. | Maxime Dénès | |
| 2017-09-22 | Merge PR #1064: coq_makefile: dont show errors from failed (ignored) rmdir | Maxime Dénès | |
| 2017-09-22 | Merge PR #1063: [flags] Flag `open Flags` | Maxime Dénès | |
| 2017-09-22 | Merge PR #1061: Fix appveyor build | Maxime Dénès | |
| 2017-09-21 | Fix -silent flag of coqchk after ff918e4. | Maxime Dénès | |
| 2017-09-21 | Adapt checker to change in locations. | Maxime Dénès | |
| 2017-09-21 | Proposing meta names more distinguishable from evar names than ?M42. | Hugo Herbelin | |
| Using "?INTERNAL#42" with a # to emphasize a meaningless re-parsability. Tough maybe it signals too much an unelegant debugging flavor? | |||
| 2017-09-21 | A possible fix to BZ#5750 (ability to print context of ltac subterm match). | Hugo Herbelin | |
| The main fix is to use is_ident_soft. The rest of the commit is to provide something a bit more appealing than "?M-1". | |||
| 2017-09-21 | [checker] Add missing Feedback printer (BZ#5587) | Emilio Jesus Gallego Arias | |
| This fixes longstanding bug likely introduced in the first `pp` to `Feedback` migration, namely the checker didn't register a feedback printer, thus no calls to `Feedback.msg_*` were printed in the checker. This closes bug: https://coq.inria.fr/bugs/show_bug.cgi?id=5587 We fix this by adding a custom printer to the checker, this is correct as the checker owns now the full console, however a cleanup should happen in any of these two directions: - all the calls to feedback are removed, and the checker always uses its own printing mechanism. - all the calls to `Format/Printf` are removed and the checker always uses the `Feedback` mechanism. Currently, I have no opinion on this. | |||
| 2017-09-21 | Do not reinstall preinstalled packages under AppVeyor. | Maxime Dénès | |
| It seems that reinstalling gcc can leave Cygwin in a strange state, where invocations of gcc fail suddenly. I haven't figure out exactly why, but this seems to fix it. | |||
| 2017-09-21 | Print Cygwin setup output rather than logging in to a file. | Maxime Dénès | |
| 2017-09-21 | Mark "Set Tactic Compat Context" as deprecated. | Guillaume Melquiond | |
| It was introduced in 8.5 for compatibility with a 8.4 bug. | |||
| 2017-09-21 | Remove remaining occurrences of -just-parsing. | Guillaume Melquiond | |
| 2017-09-20 | In gitlab set TRAVIS_BRANCH so user overlays will work as expected. | Gaëtan Gilbert | |
| 2017-09-20 | coq_makefile: dont show errors from failed (ignored) rmdir | Ralf Jung | |
| 2017-09-20 | [flags] Flag `open Flags` | Emilio Jesus Gallego Arias | |
| An incoming commit is removing some toplevel-specific global flags in favor of local toplevel state; this commit flags `Flags` use so it becomes clearer in the code whether we are relying on some "global" settable status in code. A good candidate for further cleanup is the pattern: `Flags.if_verbose Feedback.msg_info` | |||
| 2017-09-19 | An optimization of tactic constructor. | Hugo Herbelin | |
| As was questioned on Stack Overflow and discussed on Gitter, reduction of the conclusion of the goal was done up to n+1 times for a failing call to "constructor" on an inductive type of n constructors. We do it at most once. Reworking the layout of the code at the same time. | |||
| 2017-09-19 | Merge PR #1036: Unify EConstr.t equality | Maxime Dénès | |
| 2017-09-19 | Improve documentation of Status message. | Maxime Dénès | |
| 2017-09-19 | Remove STM vernaculars. | Maxime Dénès | |
| 2017-09-19 | Add XML protocol support for Wait. | Maxime Dénès | |
| 2017-09-19 | Merge PR #1050: Avoid extra failure in the "constructor" tactic (bug #5666). | Maxime Dénès | |
| 2017-09-19 | Merge PR #1043: Disable OSX signing for temporary artifacts. | Maxime Dénès | |
| 2017-09-19 | Document UState.universe_context. | Gaëtan Gilbert | |
| 2017-09-19 | Don't lose names in UState.universe_context. | Gaëtan Gilbert | |
| We dont care about the order of the binder map ([map] in the code) so no need to do tricky things with it. | |||
| 2017-09-19 | test-suite: polymorphism | Matthieu Sozeau | |
| 2017-09-19 | proof_global: cleanup and comment close_proof | Matthieu Sozeau | |
| evd: Move constrain_variables to an operation on UState Necessary to check universe declarations correctly for deferred proofs in particular. | |||
| 2017-09-19 | Allow declaring universe binders with no constraints with @{|} | Gaëtan Gilbert | |
| 2017-09-19 | Allow declaring universe constraints at definition level. | Matthieu Sozeau | |
| Introduce a "+" modifier for universe and constraint declarations to indicate that these can be extended in the final definition/proof. By default [Definition f] is equivalent to [Definition f@{+|+}], i.e universes can be introduced and constraints as well. For [f@{}] or [f@{i j}], the constraints can be extended, no universe introduced, to maintain compatibility with existing developments. Use [f@{i j | }] to indicate that no constraint (nor universe) can be introduced. These kind of definitions could benefit from asynchronous processing. Declarations of universe binders and constraints also works for monomorphic definitions. | |||
| 2017-09-19 | Allow empty instance parsing @{} | Matthieu Sozeau | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |