| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-04-09 | Readback for int31 values from native compiler. | Maxime Dénès | |
| 2014-04-09 | Full support for int31 values in native compiler. | Maxime Dénès | |
| 2014-04-09 | Partial support for open terms in int31. | Maxime Dénès | |
| 2014-04-09 | Had to split Nativelambda in two files because of Retroknowledge | Maxime Dénès | |
| dependencies. | |||
| 2014-04-09 | Int31 literals in native compiler. | Maxime Dénès | |
| 2014-04-09 | Uint31 support. | Maxime Dénès | |
| 2014-04-08 | Add an option -Q (tentative name). | Guillaume Melquiond | |
| This option complements -I-as and -R. As the two other options, it adds a new loadpath, but contrarily to them, files are not looked into the directory unless fully qualified. | |||
| 2014-04-08 | Fix universe handling (bug introduced in vi2vo commit) | Enrico Tassi | |
| Inside a section, Let followed by a Proof. Qed. are handled as regular definitions, hence they have universe constraints coming from the type and from the body. Only the former set was returned to libstack, but both sets were added to the global universe graph. Hence, at section closing time, an incomplete set of universe constraints was added back to the global graph (End Section replays the libstack) and hence saved in the .vo file. coqchk was right in reporting missing constraints. | |||
| 2014-04-08 | printer for coqchk | Enrico Tassi | |
| 2014-04-07 | Revert part of eba6b75 as coq_makefile ignores -I if it overlaps with -R. ↵ | Guillaume Melquiond | |
| (Fix for Rocq/Rational.) | |||
| 2014-04-07 | Allowing proof view to be detached in CoqIDE. | Pierre-Marie Pédrot | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |