| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-06-29 | class_tactics: remove catch-all, use Errors.noncritical | Enrico Tassi | |
| 2015-06-29 | win: compile with -debug | Enrico Tassi | |
| 2015-06-29 | Code documentation of the TACTIC/VERNAC EXTEND macros. | Pierre-Marie Pédrot | |
| 2015-06-28 | Fix incompleteness of conversion used by evarconv | Matthieu Sozeau | |
| In case we need to backtrack on universe inconsistencies when converting two (incompatible) instances of the same constant and unfold them. Bug reported by Amin Timany. | |||
| 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 | Typos in my previous edition of the reference manual. | Assia Mahboubi | |
| 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 | Adding a more efficient representation of OCaml objects in votour. | Pierre-Marie Pédrot | |
| 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-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 | 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 | 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-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-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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |