| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-04-02 | Make "Add LoadPath" behave accordingly to its documentation. | Guillaume Melquiond | |
| "Add LoadPath" is documented as acting as -Q, not as -I-as. Note that "Add Rec LoadPath" should be used when compatibility with 8.4 matters. | |||
| 2015-04-02 | Fix documentation of -R and -Q. | Guillaume Melquiond | |
| 2015-04-02 | Make it possible for -R to override the existing implicit setting of a path. | Guillaume Melquiond | |
| Without this commit, passing "-R theories Coq" to "coqtop -nois" has no effect since "-Q theories Coq" has already been done implicitly. | |||
| 2015-04-02 | Display the proper error message when Require fails to find a library. | Guillaume Melquiond | |
| 2015-04-02 | MMapAVL: some improved proofs + fix a forgotten Admitted | Pierre Letouzey | |
| 2015-04-02 | MMapAVL: implementing MMapInterface via AVL trees | Pierre Letouzey | |
| 2015-04-02 | ZArith/Int.v: some modernizations | Pierre Letouzey | |
| 2015-04-02 | MMapPositive: some improvements | Pierre Letouzey | |
| Most of them are backports of improvements already there in FSetPositive when compared with the original FMapPositive file. | |||
| 2015-04-01 | Accomodating #4166 (providing "Require Import OmegaTactic" as a | Hugo Herbelin | |
| replacement for 8.4's "Require Omega"). | |||
| 2015-04-01 | Fixing a few typos + some uniformization of writing in doc. | Hugo Herbelin | |
| 2015-04-01 | More clarifications on loadpaths. | Pierre-Marie Pédrot | |
| 2015-04-01 | Documenting "From * Require *" and clearing a bit the loadpath chapter. | Pierre-Marie Pédrot | |
| 2015-04-01 | From X Require Y looks for X with absolute path, disregarding -R. | Pierre-Marie Pédrot | |
| 2015-04-01 | Fixing inclusion of user contrib directory in the loadpath. | Pierre-Marie Pédrot | |
| 2015-04-01 | Fixing test-suite. | Pierre-Marie Pédrot | |
| 2015-04-01 | Removing a probably incorrect on-the-fly require in a tactic. | Pierre-Marie Pédrot | |
| Also removed the require function it was using, as it is absent from the remaining of the code. | |||
| 2015-03-31 | Removing references to deprecated syntax -I/-R -as. | Pierre-Marie Pédrot | |
| 2015-03-31 | Removing the unused root flag from loadpaths. | Pierre-Marie Pédrot | |
| 2015-03-31 | Fixing test-suite. | Pierre-Marie Pédrot | |
| 2015-03-31 | A more reasonable implementation of Loadpath. | Pierre-Marie Pédrot | |
| The new behaviour is simple: either a path is in the loadpaths or it is not. No more wild expansions of paths! This should not affect -R and -Q, but it does change the semantics of -I -as. Still, there are no more users of it and it only does so in a subtle way. | |||
| 2015-03-31 | Declarative mode: fix proof modes. | Arnaud Spiwack | |
| `end proof` changes the proof mode to `"Classic"`. | |||
| 2015-03-31 | Declarative mode: fix vernac classification. | Arnaud Spiwack | |
| So that the commands are assigned the appropriate status of syntax-changing or not, as well as the proof mode they are setting. | |||
| 2015-03-31 | Declarative mode: plug the specialised printers back. | Arnaud Spiwack | |
| It will not work in CoqIDE though, which handles printing its own way. It's a general remark that we have many ways of printing things in Coq and we should look for a unified structured framework to be shared between interfaces. | |||
| 2015-03-31 | Better formatting of messages in proofs. | Arnaud Spiwack | |
| 2015-03-31 | Generalisation of the "end command" argument of the goal printer. | Arnaud Spiwack | |
| This is meant to help integrate the printers of the declarative mode. | |||
| 2015-03-31 | Fix various typos in documentation | Matěj Grabovský | |
| Closes #57. | |||
| 2015-03-31 | Do not escape "'" when outputting to html, especially not using "´". | Guillaume Melquiond | |
| 2015-03-30 | grammar: export constr_eval | Enrico Tassi | |
| 2015-03-30 | grammar: export hypident | Enrico Tassi | |
| This is necessary to make ssr compile with both camlp4/5 | |||
| 2015-03-30 | camlp4: grep away warnings in output/* tests | Enrico Tassi | |
| 2015-03-30 | coq_makefile: fix compilation with camlp4 | Enrico Tassi | |
| 2015-03-30 | fix code and bound for SWITCH instruction. | Benjamin Gregoire | |
| 2015-03-29 | Ensuring more invariants in Constr_matching. | Pierre-Marie Pédrot | |
| 2015-03-29 | Adding test for bug #4165. | Pierre-Marie Pédrot | |
| 2015-03-29 | Fixing bug #4165. | Pierre-Marie Pédrot | |
| The context matching function was dropping the surrounding context in let-ins. | |||
| 2015-03-27 | Normalize scope names before storing them in vo files. (Fix for bug #4162) | Guillaume Melquiond | |
| Note that I do not understand why the delimiter map is incomplete on loading and thus was causing a failure. So, while the patch is the proper way to deal with notation scopes, there might be another bug lurking in this file. | |||
| 2015-03-27 | Putting the From parameter of the Require command into the AST. | Pierre-Marie Pédrot | |
| 2015-03-27 | STM: refine the notion of "simply a tactic" | Enrico Tassi | |
| When a worker sends back a system state to master, it tries to just send a delta. If the command is a simple tactic, then only the proof state changes. Now, what is a simple tactic? 1. a tactic 2. that does not change the environment Check 1. was surely incomplete. Now it is: VernacSolve _ | VernacFocus _ | VernacUnfocus | VernacBullet _ Is it complete? | |||
| 2015-03-27 | Properly handle extra "clean" targets with coq_makefile. | Guillaume Melquiond | |
| 2015-03-27 | use a more compact representation of non-constant constructors | Benjamin Gregoire | |
| for which there corresponding tag are greater than max_variant_tag. The code is a merge with the patch proposed by Bruno on github barras/coq commit/504c753d7bb104ff4453fa0ede21c870ae2bb00c | |||
| 2015-03-26 | allows the vm to deal with inductive type with 8388607 constant constructors ↵ | Benjamin Gregoire | |
| and 8388851 non-constant constructor. | |||
| 2015-03-26 | fix compilation | Benjamin Gregoire | |
| 2015-03-26 | Fix bug 4157, | Benjamin Gregoire | |
| change the representation of inductive constructor when there is too many non constant constructors in the inductive type Conflicts: kernel/cbytegen.ml | |||
| 2015-03-26 | add coqdep in distributed_exec, else make does not work. | Benjamin Gregoire | |
| 2015-03-26 | STM: change how proof mode switching commands are handled (decl_mode) | Enrico Tassi | |
| This is likely to make nested proofs containing proof modes switch broken, but fixes the problems Arnaud has in his branch. It is possible that the classification function we have today is not fine grained enough. If a command that changes the proof mode has as the only global effect changing the proof mode, then the current code is fine. If it has a more global effect that persists after the proof is over but has no impact on the proof itself, then the old code is fine. As far as I can get, the proof mode switching commands have a global effect (changing parser) but also a proof effect (un/focusing). We don't have a classification for these. Today a command having a global effect is played twice: on the proof branch an on master. Of course if such command cannot work on master (where there is no finished proof for example) we need a special treatment for it. | |||
| 2015-03-25 | Fix vm compiler to refuse to compile code making use of inductives with | Matthieu Sozeau | |
| more than 245 constructors (unsupported by OCaml's runtime). | |||
| 2015-03-25 | More clever representation of substituted Cemitcode. | Pierre-Marie Pédrot | |
| Module substitution is made nodewise, allowing to drop it for opaque terms in the VM. This saves a few useless substitutions. | |||
| 2015-03-25 | Summary: fix code to detect functional values in summary | Enrico Tassi | |
| 2015-03-25 | STM: avoid processing asynchronously empty proofs (Close: #4134) | Enrico Tassi | |
| 2015-03-25 | Exporting memory representation of STM tasks for votour. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |