aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-01-13Declared ML Module are not uncapitalized/capitalized/uncapitalized/...Pierre Boutillier
2014-01-13Fixing typo in reference manual from previous commitHugo Herbelin
2014-01-13Documenting old but useful command "Print Tables".Hugo Herbelin
2014-01-11'Pretty' printer for wf_pathsPierre
2014-01-10Fixing bug #3144.Pierre-Marie Pédrot
2014-01-10Useless Array.of_listPierre-Marie Pédrot
2014-01-10Omega: avoiding distinct proof-terms on repeated identical runsPierre Letouzey
2014-01-10Exporting the full pretyper options in Goal.constr_of_raw.Pierre-Marie Pédrot
2014-01-10Fix bug#2080: error message on Ltac name clash with primitive tacticsxclerc
2014-01-09Goodbye typerex, Hello merlinPierre
2014-01-09md5 for MacOSPierre
2014-01-08Fix base_include: Toplevel-->Coqloop, Constrintern.intern_constr without evdPierre Letouzey
2014-01-07typosEnrico Tassi
2014-01-07STM: additional fix for STM + vm_computeEnrico Tassi
2014-01-06Adding a -dumpgraph option to Coqdep that output the graph dependency of thePierre-Marie Pédrot
2014-01-06CoqIDE: do not unfocus if not needed on errors (closes: 3197)Enrico Tassi
2014-01-06fix simple test for paral-itpEnrico Tassi
2014-01-06fix typoEnrico Tassi
2014-01-06STM: handle side effects of workers correctlyEnrico Tassi
2014-01-06STM: fix worker crash when doing vm_computeEnrico Tassi
2014-01-06Algebraized "No such hypothesis" errorsPierre-Marie Pédrot
2014-01-06Add a test suite file for Ltac's "+" tactical.Arnaud Spiwack
2014-01-06Revert "Rewriting the proof monad mechanism. Now it uses pure OCaml code, wit...Arnaud Spiwack
2014-01-05refman: fist stab at Asynchronous ProofsEnrico Tassi
2014-01-05STM: modules do not prevent proofs from being ASyncEnrico Tassi
2014-01-05Proof_using: new syntax + suggestionEnrico Tassi
2014-01-05Fix coqc -time (Closes: 3201)Enrico Tassi
2014-01-05nanoPG: compete rewriting with more Emacs/PG like featuresEnrico Tassi
2014-01-05Disable GlobRef feedback (CoqIDE does nothing with them)Enrico Tassi
2014-01-05Environ: export API to transitively close a set of section variablesEnrico Tassi
2014-01-05STM: fix error messages while in batch mode (closes: 3196)Enrico Tassi
2014-01-05Paral-ITP: cleanup of command line flags and more conservative defaultEnrico Tassi
2014-01-05Fix some warnings with ocamlc 4.01Enrico Tassi
2014-01-05coqtop: -check-vi-tasks and -schedule-vi-checkingEnrico Tassi
2014-01-04Lemmas: export standard proof terminatorEnrico Tassi
2014-01-04Proof_global: Simpler API for proof_terminatorEnrico Tassi
2014-01-04STM: use sec vars in aux file if no Proof using when building .viEnrico Tassi
2014-01-04.vi files: .vo files without proofsEnrico Tassi
2014-01-04STM: simple refactoringEnrico Tassi
2014-01-04Future: allow custom action when a delegated future is forcedEnrico Tassi
2014-01-04kernel: save in aux the list of section variables usedEnrico Tassi
2014-01-04STM: set loc for aux file when interpreting vernacEnrico Tassi
2014-01-04STM: record in aux file proof build and check timeEnrico Tassi
2014-01-04Aux_file: cache information at compile time for later (re)useEnrico Tassi
2014-01-04Remove obsolete comment about Let being processed synchronouslyEnrico Tassi
2014-01-04Code cleaning in Rewrite, may also result faster.Pierre-Marie Pédrot
2014-01-01Reference the 'external' tactic.Guillaume Melquiond
2013-12-30When resetting an evarmap with the unsafe function Evd.evars_reset_evd withPierre-Marie Pédrot
2013-12-30Useless Evd.create_evar_defs.Pierre-Marie Pédrot
2013-12-30Support for evars and metas in native compiler.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 07:48:33 +0000