| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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. | |||
| 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 | |
| 2015-03-25 | Fully fixing bug #3491 (anomaly when building _rect scheme in the | Hugo Herbelin | |
| presence of let-ins and recursively non-uniform parameters). The bug was in the List.chop of Inductiveops.get_arity which was wrong in the presence of let-ins and recursively non-uniform parameters. The bug #3491 showed up because, in addition to have let-ins, it was wrongly detected as having recursively non-uniform parameters. Also added some comments in declarations.mli. | |||
| 2015-03-25 | Another example about the consequence of a wrong computation of the | Hugo Herbelin | |
| number of recursively uniform parameters in the presence of let-ins. In practice, more recursively non-uniform parameters were assumed and this was used especially for checking positivity of nested types, leading to refusing more nested types than necessary (see Inductive.v). | |||
| 2015-03-25 | Use kernel names instead of user names when looking for coercions. (Fix for ↵ | Guillaume Melquiond | |
| bug #4133) Note that, if someone was purposely modifying the user name of a type in order to disable a coercion, it no longer works. Hopefully, no one did. | |||
| 2015-03-25 | coqc: fix --help | Enrico Tassi | |
| 2015-03-25 | Correcting a bug introduced by universes polymorphism | jforest | |
| 2015-03-25 | correcting a bug with aliased when using Functional Scheme | forest | |
| 2015-03-24 | Updating test-suite (see previous commit). | Hugo Herbelin | |
| 2015-03-24 | Fixing computation of non-recursively uniform arguments in the | Hugo Herbelin | |
| presence of let-ins. This fixes #3491. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |