| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-10-01 | Moving ML types used by Ltac2 to their proper interface. | Pierre-Marie Pédrot | |
| 2017-09-30 | Abstracting away the primitive functions on valexpr datatype. | Pierre-Marie Pédrot | |
| 2017-09-29 | Remove a failwith "" | Gaëtan Gilbert | |
| 2017-09-29 | Remove unused Failure catch | Gaëtan Gilbert | |
| Unused since dc57718e98289b5d71a0a942d6a063d441dc6a54 as far as I can tell. | |||
| 2017-09-29 | Remove TODO comment (Evar.t is opaque) | Gaëtan Gilbert | |
| 2017-09-29 | Cleanup suggest_bullet | Gaëtan Gilbert | |
| 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-29 | start counting at 0... | Ralf Jung | |
| 2017-09-29 | [ide] Avoid duplicate error printing (BZ#5583) | Emilio Jesus Gallego Arias | |
| See the discussion in the bug tracker, basically the STM delays the feedback error message to a point where CoqIDE has forgotten about the sentence, thus we were processing such errors in the generic case, printing them twice as the Fail case will also do it. We could indeed revert back to the 8.6 strategy for error (print always from Fail and ignore Feedback), however I feel that time will be better spent by fixing the STM than adding more CoqIDE workarounds. | |||
| 2017-09-29 | [vernac] Remove `Qed exporting` syntax. | Emilio Jesus Gallego Arias | |
| We don't gain anything from the kernel yet as transparent constants _do_ require the `side_eff` exporting machinery. Next step, understand why. | |||
| 2017-09-29 | Iris CI: use opam to determine std++ git commit | Ralf Jung | |
| 2017-09-28 | Remove trivial TODO comment (constants can't be template poly now). | Gaëtan Gilbert | |
| 2017-09-28 | Efficient computation of the names contained in an environment. | Pierre-Marie Pédrot | |
| 2017-09-28 | Efficient fresh name generation relying on sets. | Pierre-Marie Pédrot | |
| The old algorithm was relying on list membership, which is O(n). This was nefarious for terms with many binders. We use instead sets in O(log n). | |||
| 2017-09-27 | Remove catch-all try with in the beautifier. | Théo Zimmermann | |
| 2017-09-27 | Beautifier gets its own formatter: fixes BZ#5704. | Théo Zimmermann | |
| 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. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |