| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-02-27 | Adding a new folder corresponding to the low-level part of the pretyper | Pierre-Marie Pédrot | |
| together with the tactic monad. The move is not complete yet, because some file candidates for this directory have almost useless dependencies in other ones that should not be moved. | |||
| 2015-02-26 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-02-24 | Univs: Fix Check calling the kernel to retype in the wrong environment. | Matthieu Sozeau | |
| Fixes bug #4089. | |||
| 2015-02-23 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-02-19 | Adding a possible DEPRECATED flag to VERNAC EXTEND statements. | Pierre-Marie Pédrot | |
| 2015-02-18 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-02-18 | Fix bug #4046. | Matthieu Sozeau | |
| 2015-02-17 | Remove Whelp commands. | Maxime Dénès | |
| Although these commands were never deprecated, they have been unusable for some time now, since they send requests to an Italian server which is no longer alive. | |||
| 2015-02-16 | Fix bug #3960: potential evar instance categorized as an unresolvable | Matthieu Sozeau | |
| goal in Instance. Also remove some dead code. | |||
| 2015-02-16 | Using same code for browsing physical directories in coqtop and coqdep. | Hugo Herbelin | |
| In particular: - abstracting the code using calls to Unix opendir, stat, and closedir, - uniformly using warnings when a directory does not exist (coqtop was ignoring silently and coqdep was exiting via handle_unix_error), - uniformly expecting paths in Unix format and warning otherwise. | |||
| 2015-02-15 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-02-14 | Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior | Enrico Tassi | |
| Of course such proofs cannot be processed asynchronously | |||
| 2015-02-13 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-02-13 | Better error message for nested module application. | Maxime Dénès | |
| Fixes #3809. | |||
| 2015-02-12 | Fix typos about .vio files (thanks Arthur for spotting them) | Enrico Tassi | |
| 2015-02-12 | Revert "Using same code for browsing physical directories in coqtop and coqdep." | Hugo Herbelin | |
| (Sorry, was not intended to be pushed) This reverts commit 5268efdefb396267bfda0c17eb045fa2ed516b3c. | |||
| 2015-02-12 | Revert "Capital letter in plugins." (Sorry, was not intended to be pushed) | Hugo Herbelin | |
| This reverts commit bff2b36cb0e2dbd02c4f181fba545a420e847767. | |||
| 2015-02-12 | Capital letter in plugins. | Hugo Herbelin | |
| 2015-02-12 | Using same code for browsing physical directories in coqtop and coqdep. | Hugo Herbelin | |
| In particular: - abstracting the code using calls to Unix opendir, stat, and closedir, - uniformly using warnings when a directory does not exist (coqtop was ignoring silently and coqdep was exiting via handle_unix_error). | |||
| 2015-02-11 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-02-11 | Tactic Notation: use stable unique key for notations (Close: 3970) | Enrico Tassi | |
| This is a fixup of commit 2e09a22b that used uniquely generated kernel names but forgot to substitute them. | |||
| 2015-02-10 | Fixing #4017, #3726 (use of implicit arguments was lost in multiple variable ↵ | Hugo Herbelin | |
| declarations). | |||
| 2015-02-10 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-02-05 | Properly set module names in presence of -Q. (Fix for bug #3958) | Guillaume Melquiond | |
| This is done by adding a fourth type of loadpath, the ones that are neither implicit nor root, for the subdirectories of a -Q root. Note: this means that scanning for available directories is no longer done on the fly for -Q, but once and for all, as with -R. | |||
| 2015-02-04 | Optimized Import/Export the same way as Require Import/Export was | Hugo Herbelin | |
| optimized. Now "Import Arith ZArith" imports only once the libraries reexported by both Arith and ZArith. (No side effect can be inserted here, so that this looks compatible). | |||
| 2015-02-04 | Tactic Notation: use stable unique key for notations (Close: 3970) | Enrico Tassi | |
| 2015-02-03 | Revert "Tactic Notation: use stable unique key for notations (Close: 3970)" | Enrico Tassi | |
| This reverts commit 2e09a22baeb93c57e6d8388313dc638349679910. | |||
| 2015-02-03 | Tactic Notation: use stable unique key for notations (Close: 3970) | Enrico Tassi | |
| 2015-02-03 | spit module path using / as directory separator | Enrico Tassi | |
| I know it seems wrong but if you call coq to get a path, you are likely to pass it around, and this makes the dir separator of windows "\" disappear immediately being interpreted as an escape character. In cygwin "/" is also understood as a directory separator. | |||
| 2015-02-02 | Removing dead code. | Pierre-Marie Pédrot | |
| 2015-01-29 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-01-29 | Prevent spurious warnings about Arguments. | Guillaume Melquiond | |
| The Arguments command tends to emit the following warning even when properly used: This command is just asserting the number and names of arguments of cons. If this is what you want add ': assert' to silence the warning. If you want to clear implicit arguments add ': clear implicits'. If you want to clear notation scopes add ': clear scopes' In fact, even ': assert' does not silence it, contrarily to what the message suggests. | |||
| 2015-01-25 | Merge branch 'v8.5' into trunk. | Pierre-Marie Pédrot | |
| 2015-01-24 | Equality Schemes options: reverting commit ff9f94634 which is | Hugo Herbelin | |
| obviously inconsistent with the decisions taken in commits 2e8fb20e04da and 0bc569026048 about bugs #2550 and #3606. Now having options Boolean Equality Schemes and Decidable Equality Schemes. | |||
| 2015-01-24 | Isolate a function for printing evar sets. | Hugo Herbelin | |
| 2015-01-23 | Merge branch 'v8.5' into trunk | Maxime Dénès | |
| 2015-01-21 | Add the possibility of defining opaque terms with program. | mlasson | |
| 2015-01-21 | Embedding the index of the ML tactic entry in the Tacexpr AST. | Pierre-Marie Pédrot | |
| This will allow to get rid of the fragile mechanism of discriminating which entry to call depending on the dynamic type of its arguments. | |||
| 2015-01-18 | Univs: proper printing of global and local universe names (only | Matthieu Sozeau | |
| printing functions touched in the kernel). | |||
| 2015-01-18 | Make native compiler handle universe polymorphic definitions. | Maxime Dénès | |
| One remaining issue: aliased constants raise an anomaly when some unsubstituted universe variables remain. VM may suffer from the same problem. | |||
| 2015-01-17 | Univs: proper printing of global and local universe names (only | Matthieu Sozeau | |
| printing functions touched in the kernel). | |||
| 2015-01-17 | Make native compiler handle universe polymorphic definitions. | Maxime Dénès | |
| One remaining issue: aliased constants raise an anomaly when some unsubstituted universe variables remain. VM may suffer from the same problem. | |||
| 2015-01-15 | Make -print-mod-uid accept a list of files. | Maxime Dénès | |
| Solves an efficiency problem in Makefiles generated by coq_makefile. | |||
| 2015-01-13 | Made -print-mod-uid more silent and robust. | Maxime Dénès | |
| This is a follow-up on Pierre's 5d80a385. | |||
| 2015-01-12 | Add -no-native-compiler flag to list dumped by --help. | Maxime Dénès | |
| 2015-01-12 | Update headers. | Maxime Dénès | |
| 2015-01-11 | Avoiding a redundant information in unification error message. | Hugo Herbelin | |
| 2015-01-08 | Avoiding introducing yet another convention in naming files. | Hugo Herbelin | |
| 2015-01-06 | rename: vi -> vio | Enrico Tassi | |
| 2015-01-06 | Fix some documentation typos. | Guillaume Melquiond | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |