| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-04-07 | Transfering the initial goals from the proofview to the proof object. | Pierre-Marie Pédrot | |
| They were just passed along in the tactics. | |||
| 2014-04-06 | Removing unused functions in Refiner. | Pierre-Marie Pédrot | |
| 2014-04-06 | Actually using the [modify] primitive. | Pierre-Marie Pédrot | |
| 2014-04-06 | Adding an [modify] function to the tactic monad. It allows to modify | Pierre-Marie Pédrot | |
| the current state without having to use both get, bind and set. | |||
| 2014-04-06 | Add tool for fully qualifying Require statements. | Guillaume Melquiond | |
| 2014-04-06 | Change handling of loadpath and mlpath. | Guillaume Melquiond | |
| - Option -I no longer handles loadpath, only mlpath. This is the same behavior as coq_makefile. Option -I-as is unchanged. - Option -R no longer recursively adds to mlpath; only the root directory is added. - user-contrib/ and xdg directories are no longer recursively added to the loadpath. - theories/ and plugins/ are no longer recursively added to the loadpath when option -nois is passed. - All the preconfigured directories are still recursively added to the mlpath though. | |||
| 2014-04-05 | Completing text of the question on conservativity of CIC over CC (bug #2697). | Hugo Herbelin | |
| 2014-04-05 | Test for bug #3142, actually duplicate of #3262. | Hugo Herbelin | |
| 2014-04-05 | Fixing bug #3228 (fixing precedence of ltac variables over variables in env). | Hugo Herbelin | |
| 2014-04-05 | Printers for ltac environments. | Hugo Herbelin | |
| 2014-04-05 | closing bug 3037 | Julien Forest | |
| 2014-04-04 | Fix for bug #3107. | Guillaume Melquiond | |
| 2014-04-04 | fixing Function doc | Julien Forest | |
| 2014-04-04 | Recognize "Instance" in coqwc. (Fix for bug #2551) | Guillaume Melquiond | |
| 2014-04-04 | Closing bug #3164 | Julien Forest | |
| 2014-04-04 | Prevent verbatim text from leaking out of comments. (See bug #2882) | Guillaume Melquiond | |
| 2014-04-04 | Fixing coqchk. It was my fault, I misused canonical and user equalities | Pierre-Marie Pédrot | |
| when defining cache hash tables in Closure. Why it was working in 3.12 is a mystery to me. | |||
| 2014-04-04 | Fixing #3262 which revealed a non-progressing, hence looping, | Hugo Herbelin | |
| refinement of evars (in filter_candidates). Incidentally introduced a copy of type "option", "update", which highlights the specific intention of "updating" or not. | |||
| 2014-04-04 | Support other forms of "Proof" in coqwc. (Fix for bug #2735) | Guillaume Melquiond | |
| 2014-04-04 | Remove option -g as it is non-portable yet does not have any effect on the ↵ | Guillaume Melquiond | |
| test-suite. (Fix for bug #3024) | |||
| 2014-04-03 | Clean up the .merlin | Thomas Refis | |
| I added a .merlin in ide/ who inherits everything from the root .merlin and also adds the dependency to lablgtk, which I removed from the root file. These way people not working on that part of the code won't get bothered if they don't have that package. I removed the S/B entry for plugins which was useless, indeed there is no ML file in that directory and merlin doesn't scan the subdirectories recursively (as you know). I also removed the S/B entry for checker since most of the files of this directory are also present in kernel and that was the cause of a lot errors on merlin's side (think "inconsistent assumptions"). On top of that, no part of the tree depends on checker (I back that assertion by a grep of the *.d files of the tree) so these lines in the .merlin were actually useless. The only part of the tree where you need to know what's in checker/ is when you are working in checker/ itself, but since merlin automatically adds the directory of the file under edition in its source and load paths nothing else is needed. There might still be problems after this patch, but they should be less of them. Considering my poor knowledge of the codebase there might be other conflicts I have missed. | |||
| 2014-04-02 | A debug printer for Evd.Filter.t | Pierre Boutillier | |
| 2014-04-02 | Add a test case for bug 3251 | Jason Gross | |
| It was closed in 5b39c3535f7b3383d89d7b844537244a4e7c0eca. | |||
| 2014-04-02 | STM: be more resilient to explicit Back + Sideff commands (closes: 3251) | Enrico Tassi | |
| 2014-04-02 | Fix Bug 3131 + Really drop mentions of info in refman. | Pierre Boutillier | |
| 2014-04-02 | Fix Bug 3217 | Pierre Boutillier | |
| Normalize the term to see if there are arguments to daclare implicits only if at least one argument occurs in the non normal form | |||
| 2014-04-02 | Better error message when found more than once object of name ... | Pierre Boutillier | |
| 2014-04-01 | Evars introduced by Proofview refining are flagged as GoalEvar. For some | Pierre-Marie Pédrot | |
| reasons, some code depends on it. | |||
| 2014-04-01 | Updated debugging printers | Hugo Herbelin | |
| 2014-04-01 | Propagating conversion_problem towards (postponed) evar/evar problems. | Hugo Herbelin | |
| Incidentally simplifies where evar/evar problems are treated (in evar_define and imitate rather than solve_simple_eqn). | |||
| 2014-04-01 | Fixing bug #2900 (evar/evar unif was supposed to be treated in | Hugo Herbelin | |
| solve_simple_eqn but in case the second evar was hidden behind a local variable, it arrived in evar_define and imitate, wrongly assuming progress). | |||
| 2014-03-31 | Removing the Change_evar refiner rule. | Pierre-Marie Pédrot | |
| 2014-03-31 | Removing dead code in Tactics. | Pierre-Marie Pédrot | |
| 2014-03-28 | Using the new refine interface to define ML tactics. | Pierre-Marie Pédrot | |
| 2014-03-28 | Lighter interface for creating refining tactics. | Pierre-Marie Pédrot | |
| 2014-03-28 | Newline on -slash warning in coqdep. | Pierre-Marie Pédrot | |
| 2014-03-28 | Define Tactics.bring_hyps in the new monad. | Pierre-Marie Pédrot | |
| 2014-03-27 | Removing tactic compatibility layer from Eqdecide. | Pierre-Marie Pédrot | |
| 2014-03-27 | Cosmetic changes in Equality. | Pierre-Marie Pédrot | |
| 2014-03-26 | Adding a tclEFFECTS primitive allowing to push STM side-effects in tactics. | Pierre-Marie Pédrot | |
| 2014-03-26 | Removing Tacmach compatibility layer in Equality. | Pierre-Marie Pédrot | |
| 2014-03-26 | Removing tactic compatibility layer in Equality. | Pierre-Marie Pédrot | |
| 2014-03-26 | Removing Tacmach compatibility layer in Inv. | Pierre-Marie Pédrot | |
| 2014-03-26 | Removing tactic compatibility layer from Inv. | Pierre-Marie Pédrot | |
| 2014-03-26 | STM: when an error occurs in a worker send back a bunch of states | Enrico Tassi | |
| In this way when the user fixes the script only a small part of the broken proof has to be recomputed on master. The density of states sent back decreases as they get far from the error. I.e. counting from the error, the worker sends back states at distance 0 1 2 3 5 7 10 14 19 26 35 47... | |||
| 2014-03-26 | CoqIDE: better error reporting for Qed on incomplete proof | Enrico Tassi | |
| 2014-03-26 | test for apply + TC resolution | Enrico Tassi | |
| 2014-03-26 | Adding an interface to Eqdecide and putting the grammar rules in a dedicated | Pierre-Marie Pédrot | |
| file. | |||
| 2014-03-26 | Moving some tactic code to the new engine. | Pierre-Marie Pédrot | |
| 2014-03-24 | Revert "Makefile: the initial build of grammar.cma is now directory-driven" | Pierre Letouzey | |
| This reverts commit f694544d016b085b3cd10007b9f7716ae2c3b022. This commit was wrong, since (at least) the highparsing part depends on the toplevel directory. I still didn't had time to fix that, so in the meantime let's revert it. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |