| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-04-02 | Puts all the "import" statements first so as to accommodate the latest GHC. | Nickolai Zeldovich | |
| 2015-04-02 | Fix some typos. | Guillaume Melquiond | |
| 2015-04-02 | Avoid outputting stray "Local" keywords in HTML documentation. | Guillaume Melquiond | |
| 2015-04-02 | Define Any in Haskell extraction when Tunknown is used. | Nickolai Zeldovich | |
| Commit 84c2433a introduced the Any type alias as the Haskell extracted version of MiniML's Tunknown. However, the code to define the Any type alias was generated conditional on usf.magic. As it turns out, sometimes Tunknown appears even if usf.magic is false (i.e., even if MLmagic does not appear anywhere in the AST). This produced Haskell code that would not compile; e.g.: % coqtop Coq < Extraction Language Haskell. Coq < Extraction Library Datatypes. The file Datatypes.hs has been created by extraction. % ghc Datatypes.hs [1 of 1] Compiling Datatypes ( Datatypes.hs, Datatypes.o ) Datatypes.hs:261:17: Not in scope: type constructor or class `Any' Datatypes.hs:261:24: Not in scope: type constructor or class `Any' The fix is straightforward: produce the code that defines the Any type alias if usf.tunknown is true. | |||
| 2015-04-02 | Fix compilation of documentation broken by the addition of MMapAVL. | Guillaume Melquiond | |
| 2015-04-02 | CoqIDE: simpler way of reopening/reclosing a proof (Close: 4168) | Enrico Tassi | |
| No "read-only" terminator. If no terminator is present the UI complains. If the terminator is different, STM warns but continues. The STM warns that the "check the document" button will not honor the terminator change, and what to do to avoid that. Technically, one cannot turn (a posteriori) an axiom into a theorem and vice versa. Could be done, but not with a small patch. | |||
| 2015-04-02 | Make sure that hyperref creates the proper links to the documentation indexes. | Guillaume Melquiond | |
| 2015-04-02 | Remove Mltop.add_path as it is no longer possible to import files from ↵ | Guillaume Melquiond | |
| subdirectories. Using Mltop.add_path instead of Mltop.add_rec_path causes the following kind of behavior: $ coqtop -nois Coq < Require Import Coq.Init.Datatypes. Error: Cannot find a physical path bound to logical path Coq.Init. The only case where its use is still warranted is the implicit "." path. It shall not be recursive because Coq might be called from about anywhere. This patch also removes -I-as since its behavior is no longer the one from 8.4 so it is not worth keeping it around. | |||
| 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 | Merge branch 'v8.5' into trunk | Enrico Tassi | |
| 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. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |