aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* obligations: wrap Ephemeron.get to make error more informativeGravatar Enrico Tassi2015-06-23
* Wrap the program_info type up in the ephemeron mechanismGravatar Alec Faithfull2015-06-23
* Fixing incompatibility introduced with simpl in commit 364decf59c1 (orGravatar Hugo Herbelin2015-06-23
* Less closures makes the GC happy.Gravatar Pierre-Marie Pédrot2015-06-23
* Add a Set Dump Bytecode command for debugging purposes.Gravatar Maxime Dénès2015-06-23
* Fix `Pp` function used by the `Info` command.Gravatar Arnaud Spiwack2015-06-23
* With the field record punning syntax.Gravatar Theo Zimmermann2015-06-23
* Put all arguments of strategy in record.Gravatar Theo Zimmermann2015-06-23
* Strategy is now a record type with a function field.Gravatar Theo Zimmermann2015-06-23
* Add comments.Gravatar Theo Zimmermann2015-06-23
* Warning are enabled by default in interactive mode.Gravatar Pierre-Marie Pédrot2015-06-23
* Remove uses of polymorphic equality from prev. commitGravatar Clément Pit--Claudel2015-06-22
* Replace 'try ... with Failure "List.last"' with 'if l <> []'Gravatar Clément Pit--Claudel2015-06-22
* Guard the List.hd call in [Show Intros]Gravatar Clément Pit--Claudel2015-06-22
* Add efficient extraction of [nat], [Z], and [string] to HaskellGravatar Nickolai Zeldovich2015-06-22
* Votour displays wordsize of segments before loading them.Gravatar Pierre-Marie Pédrot2015-06-20
* Make end-of-proof output consistent across toplevels.Gravatar Guillaume Melquiond2015-06-19
* Doc: Workers do check for guardedness before sending proofs backGravatar Enrico Tassi2015-06-17
* Fix by Enrico on CoqIDE not locating errors anymore since 550da87456a.Gravatar Hugo Herbelin2015-06-16
* Granting, undocumentedly, parsing of "Conjectures" as a synonym ofGravatar Hugo Herbelin2015-06-16
* Native compiler: do not catch exceptions not related to dynlink.Gravatar Maxime Dénès2015-06-15
* The "on_last_hyp" tactic now behaves as it should.Gravatar Cyprien Mangin2015-06-12
* Add test-suite file for bug #3446.Gravatar Matthieu Sozeau2015-06-11
* Fix bug #3446.Gravatar Matthieu Sozeau2015-06-11
* STM: states coming from workers have no proof terminators (Close #4246)Gravatar Enrico Tassi2015-06-09
* STM: silly mistake in jumping back to an old state (Close #4249)Gravatar Enrico Tassi2015-06-09
* Support CRLF end of line in fake_ide.Gravatar Guillaume Melquiond2015-06-09
* Make normalization of primitive projections in native_compute the same as wit...Gravatar Maxime Dénès2015-06-08
* Fix native compilation of primitive projections. Closes #4210.Gravatar Maxime Dénès2015-06-08
* Fixing bug #4233: The command Restart is not fontified correctly.Gravatar Pierre-Marie Pédrot2015-06-07
* Admitted does not drop poly-univ constraints (Fix #4244)Gravatar Enrico Tassi2015-06-03
* Adding a test for bug #4057.Gravatar Pierre-Marie Pédrot2015-06-02
* script to build 64 coq installer for windowsGravatar Enrico Tassi2015-06-01
* Making Coq compile with ocp-memprof.Gravatar Pierre-Marie Pédrot2015-06-01
* coqtop: reset the current file name after a load-vernac-sourceGravatar Enrico Tassi2015-05-29
* Flag -test-mode intended to be used for ad-hoc prints in test-suiteGravatar Enrico Tassi2015-05-29
* make Unset Silent work in coqcGravatar Enrico Tassi2015-05-29
* STM/Univ: save initial univs (the ones in the statement) in Proof.proofGravatar Enrico Tassi2015-05-29
* coqide: don't require ocaml >= 4Gravatar Enrico Tassi2015-05-29
* Fixup for 866c41bGravatar Enrico Tassi2015-05-28
* STM: preserve branch name on edit (Close: #4245, #4246)Gravatar Enrico Tassi2015-05-28
* Test for 4159Gravatar Enrico Tassi2015-05-28
* Fix bug #4159Gravatar Matthieu Sozeau2015-05-27
* Jump to error line in CoqIDE grabs focus of the textview.Gravatar Pierre-Marie Pédrot2015-05-26
* CoqIDE columns in error and job panels can be sorted.Gravatar Pierre-Marie Pédrot2015-05-25
* Continuing 4b5af0d6e9 and 69941d4e19 about filename case check on MacOS X.Gravatar Hugo Herbelin2015-05-22
* Changing the heuristic fixing bug #4241.Gravatar Pierre Courtieu2015-05-21
* Answering report #4241 (formatting of boxes not behaving regularlyGravatar Hugo Herbelin2015-05-20
* Continuing incomplete 4b5af0d6e9ec1 (on MacOS X, ensuring that filesGravatar Hugo Herbelin2015-05-20
* Adding an extensible global state to evarmaps.Gravatar Pierre-Marie Pédrot2015-05-19