| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-09-09 | Update csdp cache. | Pierre-Marie Pédrot | |
| This was making the test-suite fail on machines where csdp was not installed. | |||
| 2016-09-09 | Fix bug #3920 for good after 44ada64. | Pierre-Marie Pédrot | |
| The previous commit did not apply the beta reduction for compatibility on the correct goal. We rather apply it on the first generated subgoal. This fixes the ergo contrib. | |||
| 2016-09-08 | Fix Bug #5073 : regression of micromega plugin | Frédéric Besson | |
| esprit d'escalier : is now also fixed for R | |||
| 2016-09-08 | Avoid canonizing the same paths over and over. | Guillaume Melquiond | |
| The number of path canonizations was quadratic in the number of potential plugin directories. This patch makes it linear; on a standard Coq tree, this brings the number of chdir and getcwd system calls from more than 1,000 down to about 200 at startup. This also fixes a bug where the Cd vernacular command could cause plugins to break since relative paths were used to locate them. | |||
| 2016-09-08 | Fix Bug #5073 : regression of micromega plugin | Frédéric Besson | |
| The computed proof term is now more explicit exact (__arith P1 ... Pn X1 ... Xm) instead of apply (__arith P1 ... Pn) which unification could fail. | |||
| 2016-09-08 | Merge PR #271 into v8.6 | Pierre-Marie Pédrot | |
| 2016-09-07 | Fix a typo in the reference manual | Jason Gross | |
| 2016-09-07 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
| 2016-09-07 | CoqIDE: Errors are sticky (fix #4368) | Enrico Tassi | |
| 2016-09-07 | Removing useless tactic compatibility layer in Rewrite. | Pierre-Marie Pédrot | |
| 2016-09-07 | STM: if_verbose on "Checking task ..." (fix #4058) | Enrico Tassi | |
| 2016-09-07 | ltacprof: rec-calls are coaleshed | Enrico Tassi | |
| 2016-09-07 | micromega : more robust generation of proof terms | Frédéric Besson | |
| - Assert a purely arihtmetic sub-goal that is proved independently by reflexion. (This reduces the stress on the conversion test) - Does not use 'abstract' anymore (more natural proof-term) - Fix a parsing bug (certain terms in Prop where not recognized) | |||
| 2016-09-06 | A proposal to unify the messages given by Test and Print Options (#5062). | Hugo Herbelin | |
| 2016-09-06 | STM: queries give back a dummy safe_id in case of error (#5041) | Enrico Tassi | |
| 2016-09-06 | STM: sideff: report safe_id correctly (fix #4968) | Enrico Tassi | |
| 2016-09-06 | STM: nested Abort is like nested Qed (fix #4756) | Enrico Tassi | |
| There was an "optimization", since Abort is an empty side effect. But that optimization had an impact on the DAG shape. Now a nested proof, no matter if it is kept or dropped, is handled the same. | |||
| 2016-09-05 | coqide: use Document instead of tags to detect sentences to `Skip (#4829) | Enrico Tassi | |
| When one jumps from a focused area to a point after the focused zone, sentences that are already processed (in the Doc.context of the focused area) have not to be processed again (they are tagged as `Skip). Detection of such sentences was based on tags (i.e. colors) that is shaky. Now we use the sentence-marks as stored in the document data structure. | |||
| 2016-09-05 | Test file for #5065 - Anomaly: Not a proof by induction | Maxime Dénès | |
| 2016-09-05 | Fix #5065: Anomaly: Not a proof by induction | Maxime Dénès | |
| Using abstract can create beta-redexes or let-ins in the head of the proof terms. The code projecting out mutual lemmas was not robust enough. | |||
| 2016-09-05 | Fast path in push_rel_context_to_named_context. | Pierre-Marie Pédrot | |
| Essentially, we do not reconstruct the named_context_val when the rel_context is empty. | |||
| 2016-09-05 | profile_ltac: rewritten to be purely functional and STM aware | Enrico Tassi | |
| Changes: - data structures are purely functional (so retracting do work) - profiling data flows towards master using the feedback bus - master aggregates the data on printing | |||
| 2016-09-05 | xml_printer: use sensible names for putc and puts | Enrico Tassi | |
| They used to be called output and output' ... | |||
| 2016-09-05 | feedback: support multiple feedback listeners | Enrico Tassi | |
| So that a module can add his own and look at the traffic | |||
| 2016-09-05 | Summary: simpler API for process-local storage | Enrico Tassi | |
| 2016-09-04 | Do not normalize evars in Eauto.e_give_exact. | Pierre-Marie Pédrot | |
| This is not needed, as the terms are then checked up to unification or convertibility. | |||
| 2016-09-03 | Fixing what is probably a typo in Strict Proofs mode (#5062). | Hugo Herbelin | |
| 2016-09-02 | Fast path in whd_evar. | Pierre-Marie Pédrot | |
| Before computing the whd_evar-form of the arguments of an evar, we first check that it is indeed defined. | |||
| 2016-09-02 | Silence the CAMLP5 warnings on command line. | Pierre-Marie Pédrot | |
| They were mostly useless, and people complained about it. Not that because there is no API to make CAMLP4 silent, a CAMLP4-based Coq will still spit out its share of noisy warnings. | |||
| 2016-09-02 | Remove useless debug code. | Guillaume Melquiond | |
| 2016-09-02 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
| 2016-09-01 | Fix test-suite after Frédéric's 6231f07b2. | Maxime Dénès | |
| 2016-09-01 | Fixed Bug #5003 : more careful generalisation of dependent terms. | Frédéric Besson | |
| 2016-09-01 | More efficient data structure to check if a native file is loaded. | Maxime Dénès | |
| Spotted by PMP. | |||
| 2016-09-01 | Notation_ops.subst_glob_vars: substituting also in evar kind for | Hugo Herbelin | |
| consistency of the use of names. | |||
| 2016-09-01 | Short documentation, filling TODO's in evd.mli. | Hugo Herbelin | |
| 2016-09-01 | Fixing call to "lazy beta iota" in "refine" (restoring v8.4 behavior). | Hugo Herbelin | |
| (It was reducing also in hypotheses.) | |||
| 2016-09-01 | Moving log of "TacReduce"/"reduce" to Tactics.reduce so that internal | Hugo Herbelin | |
| calls are logged too. Using appropriate printer for reparsability of the output. | |||
| 2016-09-01 | Fixing name of internal refine ("simple refine"). | Hugo Herbelin | |
| 2016-08-31 | Fix Bug #5005 : micromega tactics is now robust to failure of 'abstract'. | Frédéric Besson | |
| If 'abstract' fails e.g. if there are existentials. The tactic runs an abstract-free alternative. | |||
| 2016-08-31 | Fix bug #5043: [Admitted] lemmas pick up section variables. | Pierre-Marie Pédrot | |
| We add a flag Keep Admitted Variables that allows to recover the legacy v8.4 behaviour of admitted lemmas. The statement of such lemmas did not depend on the current context variables. | |||
| 2016-08-30 | Fix bug #5051: Large outputs are garbled. | Pierre-Marie Pédrot | |
| Instead of relying on the current position of the cursor, we rather use a dedicated mark in the message view. | |||
| 2016-08-30 | Fixing output test-suite after warning for inner Requires. | Pierre-Marie Pédrot | |
| 2016-08-30 | Fix bug #4893: not_evar: unexpected failure in 8.5pl1. | Pierre-Marie Pédrot | |
| 2016-08-30 | plugin micromega : nra also handles non-linear rational arithmetic over Q ↵ | Frédéric Besson | |
| (Fixed #4985) Lqa.v defines the tactics lra and nra working over Q. Lra.v defines the tactics lra and nra working over R. | |||
| 2016-08-30 | Fix bug #3920: eapply masks an hypothesis name. | Pierre-Marie Pédrot | |
| The problem came from the fact that the legacy beta-reduction occurring after a rewrite was wrongly applied to the side-conditions of the rewriting step. We restrict it to the correct goal in this patch. | |||
| 2016-08-30 | Emit a warning on Require inside a module. | Maxime Dénès | |
| 2016-08-30 | Fix #4941 - ~/.coqrc file confusing locations | Maxime Dénès | |
| 2016-08-30 | Fix #4871 - interrupting par:abstract kills coqtop | Maxime Dénès | |
| Fix done with Enrico. | |||
| 2016-08-30 | Missing .PHONY targets. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |