| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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-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 | 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 | |
| 2015-06-22 | Remove uses of polymorphic equality from prev. commit | Clément Pit--Claudel | |
| Message to the github robot: This closes #63 | |||
| 2015-06-22 | Replace 'try ... with Failure "List.last"' with 'if l <> []' | Clément Pit--Claudel | |
| 2015-06-22 | Guard the List.hd call in [Show Intros] | Clément Pit--Claudel | |
| Fix for [Anomaly: Uncaught exception Failure("hd")] after running [Show Intros] at the end of a proof: Goal True. trivial. Show Intros. | |||
| 2015-06-22 | Add efficient extraction of [nat], [Z], and [string] to Haskell | Nickolai Zeldovich | |
| This mirrors the existing extraction libraries for OCaml. One wart: the extraction for [string] requires that the Haskell code imports Data.Bits and Data.Char. Coq has no way to add extra import statements to the extracted code. So we have to rely on the user to somehow import these libraries (e.g., using the -pgmF ghc option). See also https://coq.inria.fr/bugs/show_bug.cgi?id=4189 Message to github robot: this commit closes #65 | |||
| 2015-06-22 | Merge remote-tracking branch 'forge/v8.5' | Pierre Boutillier | |
| 2015-06-22 | Fixup last commit | Pierre Boutillier | |
| 2015-06-22 | update gitignore | Pierre Boutillier | |
| 2015-06-22 | All invocations to ocaml compilers go through ocamlfind | Pierre Boutillier | |
| Nothing is done for camlp4 There is an issue with computing camlbindir | |||
| 2015-06-20 | Votour displays wordsize of segments before loading them. | Pierre-Marie Pédrot | |
| 2015-06-19 | Make end-of-proof output consistent across toplevels. | Guillaume Melquiond | |
| Ideally, the code should be shared between the various toplevels, but this is a lot more work than just fixing a few strings. | |||
| 2015-06-17 | Doc: Workers do check for guardedness before sending proofs back | Enrico Tassi | |
| 2015-06-16 | Fix by Enrico on CoqIDE not locating errors anymore since 550da87456a. | Hugo Herbelin | |
| 2015-06-16 | Granting, undocumentedly, parsing of "Conjectures" as a synonym of | Hugo Herbelin | |
| "Conjecture" (see #4252). | |||
| 2015-06-15 | Native compiler: do not catch exceptions not related to dynlink. | Maxime Dénès | |
| Was making the study of bugs like #4139 painful. Now printing a better error message when a compiled file is missing. | |||
| 2015-06-12 | The "on_last_hyp" tactic now behaves as it should. | Cyprien Mangin | |
| 2015-06-11 | Add test-suite file for bug #3446. | Matthieu Sozeau | |
| 2015-06-11 | Fix bug #3446. | Matthieu Sozeau | |
| Wrong handling of algebraic universes that have upper bounds. | |||
| 2015-06-09 | STM: states coming from workers have no proof terminators (Close #4246) | Enrico Tassi | |
| Hence we reuse the ones in master. | |||
| 2015-06-09 | STM: silly mistake in jumping back to an old state (Close #4249) | Enrico Tassi | |
| 2015-06-09 | Support CRLF end of line in fake_ide. | Guillaume Melquiond | |
| 2015-06-08 | Make normalization of primitive projections in native_compute the same as ↵ | Maxime Dénès | |
| with other reduction machines. | |||
| 2015-06-08 | Fix native compilation of primitive projections. Closes #4210. | Maxime Dénès | |
| 2015-06-07 | Fixing bug #4233: The command Restart is not fontified correctly. | Pierre-Marie Pédrot | |
| 2015-06-06 | micromega : fix silly timeout | Frédéric Besson | |
| 2015-06-03 | Admitted does not drop poly-univ constraints (Fix #4244) | Enrico Tassi | |
| 2015-06-02 | Adding a test for bug #4057. | Pierre-Marie Pédrot | |
| 2015-06-01 | script to build 64 coq installer for windows | Enrico Tassi | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |