| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-09-09 | Removing the now useless field env_named_val from named_context_val. | Pierre-Marie Pédrot | |
| This field was only used by the VM before, but since the previous patches, this part of the code relies on the map instead. | |||
| 2016-09-09 | More efficient implementation of map_named_val. | Pierre-Marie Pédrot | |
| 2016-09-09 | Fast access environment in CClosure. | Pierre-Marie Pédrot | |
| 2016-09-09 | Tentative fast-access named env | Pierre-Marie Pédrot | |
| 2016-09-09 | Packing the named_context_val in a proper record and marking it private. | Pierre-Marie Pédrot | |
| 2016-09-09 | Make it explicit when paths are added to the ML search paths. | Guillaume Melquiond | |
| When Mltop.add_rec_path was called to add paths to the loadpath, it was also adding the top directory to the mlpath. In particular, "theories" was added to the mlpath although it was explicitly marked "~with_ml:false". The "plugins" and "user-contribs" subdirectories were scanned twice, once for filling the loadpath and then for filling the mlpath. This patch adds an argument to Mltop.add_rec_path to explicitly control which paths from the loadpath are added to the mlpath (none, the top one, all of them). The "top" option was the single old behavior; the "none" option is used for "theories"; the "all" option is used to avoid duplicate scanning for "plugins" and "user-contribs". | |||
| 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 | A proposal for recommended uniformity of style in programming Coq. | Hugo Herbelin | |
| Starting listing some recommendations in using the API. | |||
| 2016-09-09 | Removing the last uses of Pptactic in the lower layers. | Pierre-Marie Pédrot | |
| 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 | Unplugging Pptactic from Ppvernac. | Pierre-Marie Pédrot | |
| 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 | Making Proof_global terminator generic in external tactics. | Pierre-Marie Pédrot | |
| 2016-09-08 | Making Hints generic in the use of external tactics. | Pierre-Marie Pédrot | |
| 2016-09-08 | Unplugging Tacexpr in several interface files. | Pierre-Marie Pédrot | |
| 2016-09-08 | Making Vernacexpr independent from Tacexpr. | Pierre-Marie Pédrot | |
| 2016-09-08 | Merge PR #244. | Pierre-Marie Pédrot | |
| 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.6' | Pierre-Marie Pédrot | |
| 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.6' | Pierre-Marie Pédrot | |
| 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. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |