| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-06-28 | Reinstall Set Printing Universes option overwritten by Maxime! | Matthieu Sozeau | |
| 2015-06-26 | Share prop/set values in sorts.ml. | Matthieu Sozeau | |
| 2015-06-26 | Fix bug #4254 with the help of J.H. Jourdan | Matthieu Sozeau | |
| 1) We now _assign_ the smallest possible arities to mutual inductive types and eventually add leq constraints on the user given arities. Remove useless limitation on instantiating algebraic universe variables with their least upper bound if they have upper constraints as well. 2) Do not remove non-recursive variables when computing minimal levels of inductives. 3) Avoid modifying user-given arities if not necessary to compute the minimal level of an inductive. 4) We correctly solve the recursive equations taking into account the user-declared level. | |||
| 2015-06-26 | BUGFIX: Three fixes for the price of 1 in sorts.ml: | Matthieu Sozeau | |
| - Proper [family] implementation - Use the tailor made hash function for Sorts.t in two places. | |||
| 2015-06-26 | Add target to install dev files. | Matthieu Sozeau | |
| 2015-06-26 | Introduction of a "Undelimit Scope" command, undoing "Delimit Scope" | Lionel Rieg | |
| 2015-06-26 | Add a flag to deactivate guard checking in the kernel. | Arnaud Spiwack | |
| 2015-06-26 | Typos in my previous edition of the reference manual. | Assia Mahboubi | |
| 2015-06-26 | dev/tool/anomaly-traces-parser.el | Gabriel Scherer | |
| An .emacs-ready elisp snippet to parse location of Anomaly backtraces and jump to them conveniently from the Emacs *compilation* output. | |||
| 2015-06-26 | Some edition in the coq_makefile/_CoqProject section. | Assia Mahboubi | |
| There are still two items I do not undertand fully (the last one about -extra-phony, and the removal of external libraries at make clean time, that I could not reproduce on a toy example. | |||
| 2015-06-26 | Added _CoqProject to the index of the reference manual. | Assia Mahboubi | |
| 2015-06-25 | Add coqide syntax highlighting for `Assume`. | Arnaud Spiwack | |
| 2015-06-25 | Adding a more efficient representation of OCaml objects in votour. | Pierre-Marie Pédrot | |
| 2015-06-25 | Remove other types not carried by interpretations in `Tacexpr`. | Arnaud Spiwack | |
| 2015-06-25 | Remove useless `and_short_name` in interpreted level in `Tacexpr`. | Arnaud Spiwack | |
| 2015-06-25 | Wrapped the declare_object function to pretty-print anomalies at loading time. | Thomas Sibut-Pinote | |
| 2015-06-25 | Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly. | Thomas Sibut-Pinote | |
| This allows fatal_error to be used for printing anomalies at loading time. | |||
| 2015-06-25 | Adjust checker after `Assume [Positive]`. | Arnaud Spiwack | |
| 2015-06-24 | Make inductives that were assumed positive appear in `Print Assumptions`. | Arnaud Spiwack | |
| They appear as axioms of the form `Foo is positive`. | |||
| 2015-06-24 | When assuming an inductive type positive, then it is declared "unsafe" to ↵ | Arnaud Spiwack | |
| the interfaces. | |||
| 2015-06-24 | Add syntax entry to assume strict positivity of an inductive type. | Arnaud Spiwack | |
| The syntax is `Assume [Positive]` Inductive/CoInductive/Record…`. The square brackets are used to delimit what is actually a list, so that other such flags can be passed in the future (universes, guard condition…). | |||
| 2015-06-24 | Add corresponding field in `VernacInductive`. | Arnaud Spiwack | |
| Makes sure not to generate inductive schemes of assumed positive types. | |||
| 2015-06-24 | Add a corresponding field in `mutual_inductive_entry` (part 2). | Arnaud Spiwack | |
| The request for positivity to be assumed is honored. | |||
| 2015-06-24 | Add a corresponding field in `mutual_inductive_entry` (part 1). | Arnaud Spiwack | |
| The field in `mutual_inductive_entry` requires that a mutually inductive definition be checked or not, whereas the field in `mutual_inductive_body` asserts that it has or has not been. | |||
| 2015-06-24 | Add a field in `mutual_inductive_body` to represent mutual inductive whose ↵ | Arnaud Spiwack | |
| positivity is assumed. | |||
| 2015-06-24 | Extend test-suite for the positivity checker. | Arnaud Spiwack | |
| I wasn't very creative: I just added a single test by failure case in the positivity checker (plus one success). There should probably be tests with mutually inductives and co-inductives as well. | |||
| 2015-06-24 | More silent Makefile when looking for codesign. | Maxime Dénès | |
| May still be wrong on Windows, though. | |||
| 2015-06-24 | Fix test-suite after 1343b69221ce3eeb3154732e73bbdc0044b224a8. | Maxime Dénès | |
| 2015-06-24 | Less closures makes the GC happy. | Pierre-Marie Pédrot | |
| We lambda-lift by hand the graph traversal functions in Univ to allocate less closures. | |||
| 2015-06-24 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-06-24 | Add a space in cast since cast binds loosely. | Gregory Malecha | |
| Fixes bug 3936 This closes #73 | |||
| 2015-06-24 | improve --help documentation: the -m|--memory option was missing | Gabriel Scherer | |
| 2015-06-24 | when OCAML_GC_STATS points to a filepath, write Gc stats into it | Gabriel Scherer | |
| This interface is promoted by the operf-macro tool https://github.com/OCamlPro/operf-macro which allows to run benchmarks of time and memory usage of various OCaml programs. Coq already has two ways to get Gc infos: - the -m|--memory command-line flag prints the total heap words allocated - the "Print Debug Gc" command prints much more information, but in a Coq-implementation-defined format that is not suitable for across-programs comparison (also an environment variable allows to profile Coq runs on any .v, in an non-intrusive way) Note to the Github Robot: This closes #75 | |||
| 2015-06-24 | On-demand Require. | Pierre-Marie Pédrot | |
| Marshalled libraries are only loaded when needed and dropped thereafter. This might be costly for Require inside modules, but such a practice is discouraged anyway. | |||
| 2015-06-24 | Splitting the library representation on disk in two. | Pierre-Marie Pédrot | |
| The first part only contains the summary of the library, while the second one contains the effective content of it. | |||
| 2015-06-23 | obligations: wrap Ephemeron.get to make error more informative | Enrico Tassi | |
| A worker should never have to access the still-to-be-proved obligations. If that happens, raise an informative anomaly. | |||
| 2015-06-23 | Wrap the program_info type up in the ephemeron mechanism | Alec Faithfull | |
| This type contains a few unmarshallable fields, which can cause STM workers to break in unpleasant ways when running queries | |||
| 2015-06-23 | Fixing incompatibility introduced with simpl in commit 364decf59c1 (or | Hugo Herbelin | |
| maybe ca71714). Goal 2=2+2. match goal with |- (_ = ?c) => simpl c end. was working in 8.4 but was failing in 8.5beta2. Note: Changes in tacintern.ml are otherwise purely cosmetic. | |||
| 2015-06-23 | Less closures makes the GC happy. | Pierre-Marie Pédrot | |
| 2015-06-23 | Wrapped the declare_object function to pretty-print anomalies at loading time. | Thomas Sibut-Pinote | |
| 2015-06-23 | Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly. | Thomas Sibut-Pinote | |
| This allows fatal_error to be used for printing anomalies at loading time. | |||
| 2015-06-23 | Add a Set Dump Bytecode command for debugging purposes. | Maxime Dénès | |
| Prints the VM bytecode produced by compilation of a constant or a call to vm_compute. | |||
| 2015-06-23 | Fix `Pp` function used by the `Info` command. | Arnaud Spiwack | |
| I used a low-level function, now changed to `msg_notice`. | |||
| 2015-06-23 | With the field record punning syntax. | Theo Zimmermann | |
| 2015-06-23 | Put all arguments of strategy in record. | Theo Zimmermann | |
| 2015-06-23 | Strategy is now a record type with a function field. | Theo Zimmermann | |
| 2015-06-23 | Add comments. | Theo Zimmermann | |
| 2015-06-23 | Warning are enabled by default in interactive mode. | Pierre-Marie Pédrot | |
| 2015-06-23 | Document the positivity checker. | Arnaud Spiwack | |
| This is my attempt at understanding each case and subfunction of the positivity check and document each of them to the best of my capacity. | |||
| 2015-06-22 | Merge branch 'v8.5' into trunk | Pierre Letouzey | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |