| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 2015-06-01 | Making Coq compile with ocp-memprof. | Pierre-Marie Pédrot | |
| Patch provided by Çagdas Bozman. | |||
| 2015-06-01 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-05-29 | coqtop: reset the current file name after a load-vernac-source | Enrico Tassi | |
| 2015-05-29 | Flag -test-mode intended to be used for ad-hoc prints in test-suite | Enrico Tassi | |
| Of course there is an exception to the previous commit. Fail used to print even if silenced but loading a vernac file. This behavior is useful only in tests, hence this flag. | |||
| 2015-05-29 | make Unset Silent work in coqc | Enrico Tassi | |
| Trying to untangle the flags: coqc -verbose coqtop -compile-verbose are used just to print the commands run; -quiet, -silent, Set Silent, Unset Silent control Flags.verbose flag. Flags.verbose controls many prints that are expected to be made in interactive mode. E.g. "Proof" or "tac" prints goals if such flag is true. To flip it, one can "Set/Unset Silent" in both coqtop and coqc mode. It is still messy, but the confusion between -verbose and Flags.verbose has gone (I must have identified the two things with my initial STM patch) | |||
| 2015-05-29 | STM/Univ: save initial univs (the ones in the statement) in Proof.proof | Enrico Tassi | |
| This makes the treatment of universe constraints/normalization more understandable in the Sync/Async case: - if one has to keep the constraints of the body and the type of a lemma separate, then equations coming from the body are kept (see: 866c41 ) - if they can be merge then the equations (substituted on both the body and type) can be removed (one of the sides occurs nowhere) The result is that, semantically, the constraints of a lemma do not depend on weather it was produced asynchronously (v->vio->vo, or in a CoqIDE session) or synchronously (v->vo). Still the internal representation of the constraints changes to accommodate an optimization (to reduce the size of the constraint set): - in the synchronous case (some) equations are substituted (in both the type and body), hence they can be completely dropped from the constraint set - in the asynchronous case (some) equations are substituted in the body only (the type is fixed once and for all before the equations are discovered/generated), hence these equations are necessary to relate the type and the (optimized) body and are hence kept in the constraint set | |||
| 2015-05-29 | coqide: don't require ocaml >= 4 | Enrico Tassi | |
| 2015-05-28 | Fixup for 866c41b | Enrico Tassi | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |