aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-06-23Put all arguments of strategy in record.Theo Zimmermann
2015-06-23Strategy is now a record type with a function field.Theo Zimmermann
2015-06-23Add comments.Theo Zimmermann
2015-06-23Warning are enabled by default in interactive mode.Pierre-Marie Pédrot
2015-06-22Remove uses of polymorphic equality from prev. commitClément Pit--Claudel
2015-06-22Replace 'try ... with Failure "List.last"' with 'if l <> []'Clément Pit--Claudel
2015-06-22Guard the List.hd call in [Show Intros]Clément Pit--Claudel
2015-06-22Add efficient extraction of [nat], [Z], and [string] to HaskellNickolai Zeldovich
2015-06-20Votour displays wordsize of segments before loading them.Pierre-Marie Pédrot
2015-06-19Make end-of-proof output consistent across toplevels.Guillaume Melquiond
2015-06-17Doc: Workers do check for guardedness before sending proofs backEnrico Tassi
2015-06-16Fix by Enrico on CoqIDE not locating errors anymore since 550da87456a.Hugo Herbelin
2015-06-16Granting, undocumentedly, parsing of "Conjectures" as a synonym ofHugo Herbelin
2015-06-15Native compiler: do not catch exceptions not related to dynlink.Maxime Dénès
2015-06-12The "on_last_hyp" tactic now behaves as it should.Cyprien Mangin
2015-06-11Add test-suite file for bug #3446.Matthieu Sozeau
2015-06-11Fix bug #3446.Matthieu Sozeau
2015-06-09STM: states coming from workers have no proof terminators (Close #4246)Enrico Tassi
2015-06-09STM: silly mistake in jumping back to an old state (Close #4249)Enrico Tassi
2015-06-09Support CRLF end of line in fake_ide.Guillaume Melquiond
2015-06-08Make normalization of primitive projections in native_compute the same as wit...Maxime Dénès
2015-06-08Fix native compilation of primitive projections. Closes #4210.Maxime Dénès
2015-06-07Fixing bug #4233: The command Restart is not fontified correctly.Pierre-Marie Pédrot
2015-06-03Admitted does not drop poly-univ constraints (Fix #4244)Enrico Tassi
2015-06-02Adding a test for bug #4057.Pierre-Marie Pédrot
2015-06-01script to build 64 coq installer for windowsEnrico Tassi
2015-06-01Making Coq compile with ocp-memprof.Pierre-Marie Pédrot
2015-05-29coqtop: reset the current file name after a load-vernac-sourceEnrico Tassi
2015-05-29Flag -test-mode intended to be used for ad-hoc prints in test-suiteEnrico Tassi
2015-05-29make Unset Silent work in coqcEnrico Tassi
2015-05-29STM/Univ: save initial univs (the ones in the statement) in Proof.proofEnrico Tassi
2015-05-29coqide: don't require ocaml >= 4Enrico Tassi
2015-05-28Fixup for 866c41bEnrico Tassi
2015-05-28STM: preserve branch name on edit (Close: #4245, #4246)Enrico Tassi
2015-05-28Test for 4159Enrico Tassi
2015-05-27Fix bug #4159Matthieu Sozeau
2015-05-26Jump to error line in CoqIDE grabs focus of the textview.Pierre-Marie Pédrot
2015-05-25CoqIDE columns in error and job panels can be sorted.Pierre-Marie Pédrot
2015-05-22Continuing 4b5af0d6e9 and 69941d4e19 about filename case check on MacOS X.Hugo Herbelin
2015-05-21Changing the heuristic fixing bug #4241.Pierre Courtieu
2015-05-20Answering report #4241 (formatting of boxes not behaving regularlyHugo Herbelin
2015-05-20Continuing incomplete 4b5af0d6e9ec1 (on MacOS X, ensuring that filesHugo Herbelin
2015-05-19Adding an extensible global state to evarmaps.Pierre-Marie Pédrot
2015-05-19Test for bug #4116.Pierre-Marie Pédrot
2015-05-18Uncaught exception termination exits coqtop with the anomaly errno.Pierre-Marie Pédrot
2015-05-18The Fail command does not catch uncaught exception anomalies anymore.Pierre-Marie Pédrot
2015-05-18Removing test for opened bugs that were already present in the closed test-su...Pierre-Marie Pédrot
2015-05-18Tentative fix for #3461: Anomaly: Uncaught exception Pretype_errors.PretypeEr...Pierre-Marie Pédrot
2015-05-18Fixed CHANGES to reflect -color option.Pierre Courtieu
2015-05-18Disabling colors when tERM variable is "dumb".Pierre Courtieu
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-17 04:04:22 +0000