| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-09-27 | [stm] Warn about costly Undo operations in batch mode [BZ#5677] | Emilio Jesus Gallego Arias | |
| Undo & friends is very expensive in batch mode as backtracking state is not kept and thus should be recomputed. We thus warn the user. | |||
| 2017-09-27 | [stm] Remove unused "Proof using" data in `Sync` tags. | Emilio Jesus Gallego Arias | |
| This was not used anywhere; it looks like dead code from some previous attempt. `get_hint_ctx` looks also very very suspicious. | |||
| 2017-09-27 | Browser userscript to turn BZ#XXXX occurences into links. | Gaëtan Gilbert | |
| 2017-09-27 | Avoid looping when searching for CoqProject. | Maxime Dénès | |
| This could happen with paths on Windows, or even relative paths on all OSs. Fixes #5730: CoqIDE becomes unresponsive on file open. | |||
| 2017-09-27 | Moving setting of "cleared" evar flag directly in Evd.restrict. | Hugo Herbelin | |
| In particular, this fixes #5757 which used restrict_evar to refine the information on the source of an evar, and which should have set the "cleared" flag. Also renaming flag "restricted" since it is not only about "clear". I guess this is what we want in general, but I did not survey all uses of restrict_evar so, maybe, this should be refined further. | |||
| 2017-09-27 | Fixing an old bug in collecting evars with cleared context. | Hugo Herbelin | |
| The function Proofview.undefined was collecting twice the evars that had advanced. Consequently, the functions Proofview.unshelve and Proofview.with_shelf were possibly doing the same. | |||
| 2017-09-27 | Fixing an old bug in collecting evars with cleared context. | Hugo Herbelin | |
| The function Proofview.undefined was collecting twice the evars that had advanced. Consequently, the functions Proofview.unshelve and Proofview.with_shelf were possibly doing the same. | |||
| 2017-09-26 | Merge PR #688: Binding universe constraints in Definition/Inductive/etc... | Maxime Dénès | |
| 2017-09-26 | look for Obligation num or Next Obligation to start proof | Paul Steckler | |
| 2017-09-26 | Adding quotations for the assert family of tactics. | Pierre-Marie Pédrot | |
| 2017-09-26 | Small language of combinators for lookaheads in parsing. | Pierre-Marie Pédrot | |
| 2017-09-26 | Slightly more straightforward notation for (e)apply. | Pierre-Marie Pédrot | |
| 2017-09-26 | Properly display the "only" prefix for selectors (bug #5760). | Guillaume Melquiond | |
| This commit also fixes range selectors being incorrectly displayed. | |||
| 2017-09-25 | BZ#5739, Allow level for leftmost nonterminal for printing-ony Notations | Paul Steckler | |
| 2017-09-25 | Fixing a little parsing bug with level 90 introduced in 3e70ea9c. | Hugo Herbelin | |
| Unfortunately, some manual synchronization is needed between the constr parser and the table of constr/pattern levels. We do this synchronization which was missing in the commit moving "x -> y" to a user-level notation. | |||
| 2017-09-25 | [doc] Update INSTALL to match reality. | Emilio Jesus Gallego Arias | |
| [c.f] https://coq.inria.fr/bugs/show_bug.cgi?id=4270 | |||
| 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 | After testing it in live, writing metas using an ?INTERNAL#42 style is ugly. | Hugo Herbelin | |
| Printing metas still happens relatively often. From the user point of view, no need to know that it is different from an evar, so the notation ?M42 as it was before is much lighter. As for developers looking for debugging information, they will easily suspect that it is internally a meta because of the "M". This reverts "Proposing meta names more distinguishable from evar names than ?M42." (dc5b8f1793c6f7104f0b4762d9887be255709ead). | |||
| 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 | Remove some unused parts of the reference manual. | Guillaume Melquiond | |
| 2017-09-22 | Avoid generated names for html pages of the reference manual (bug #4742). | Guillaume Melquiond | |
| 2017-09-22 | Himsg: Dropping nf_evars made obsolete by EConstr. | Hugo Herbelin | |
| 2017-09-22 | Cannot unify message: improve preventing repeating twice the same message. | Hugo Herbelin | |
| Call to nf_betaiota was done on one side of the comparison preventing the same message to be repeated twice but not on the other side. | |||
| 2017-09-22 | Make a test for coq_makefile portable. | Pierre-Marie Pédrot | |
| The validity of this test depended on Makefile issueing warnings in English. We simply force the global language of the shell to be C. | |||
| 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 | Report missing arguments in error message | Tej Chajed | |
| Augment the "Illegal tactic application" error message with the number of extra arguments passed. Fixes BZ#5753. | |||
| 2017-09-21 | Properly handle "coq_makefile -Q . Foo" (bug #5580). | Guillaume Melquiond | |
| 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 run Travis OS X packaging job on PRs | Théo Zimmermann | |
| This job was useless anyway because the depoly and pre-deploy phases were not run. | |||
| 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. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |