aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-06-24Extend test-suite for the positivity checker.Arnaud Spiwack
2015-06-24Merge branch 'v8.5'Pierre-Marie Pédrot
2015-06-24Add a space in cast since cast binds loosely.Gregory Malecha
2015-06-24improve --help documentation: the -m|--memory option was missingGabriel Scherer
2015-06-24when OCAML_GC_STATS points to a filepath, write Gc stats into itGabriel Scherer
2015-06-24On-demand Require.Pierre-Marie Pédrot
2015-06-24Splitting the library representation on disk in two.Pierre-Marie Pédrot
2015-06-23obligations: wrap Ephemeron.get to make error more informativeEnrico Tassi
2015-06-23Wrap the program_info type up in the ephemeron mechanismAlec Faithfull
2015-06-23Fixing incompatibility introduced with simpl in commit 364decf59c1 (orHugo Herbelin
2015-06-23Less closures makes the GC happy.Pierre-Marie Pédrot
2015-06-23Wrapped the declare_object function to pretty-print anomalies at loading time.Thomas Sibut-Pinote
2015-06-23Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.Thomas Sibut-Pinote
2015-06-23Add a Set Dump Bytecode command for debugging purposes.Maxime Dénès
2015-06-23Fix `Pp` function used by the `Info` command.Arnaud Spiwack
2015-06-23With the field record punning syntax.Theo Zimmermann
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-23Document the positivity checker.Arnaud Spiwack
2015-06-22Merge branch 'v8.5' into trunkPierre Letouzey
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-22Merge remote-tracking branch 'forge/v8.5'Pierre Boutillier
2015-06-22Fixup last commitPierre Boutillier
2015-06-22update gitignorePierre Boutillier
2015-06-22All invocations to ocaml compilers go through ocamlfindPierre Boutillier
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-06micromega : fix silly timeoutFrédéric Besson
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 08:30:19 +0000