aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2013-12-29Avoid generating .ml files in native compiler.Maxime Dénès
2013-12-29Got rid of unused lazy flag in the native compiler.Maxime Dénès
2013-12-28Revert "Partial revert of r16711"Maxime Dénès
2013-12-28Removing native_name reference from constant_body.Maxime Dénès
2013-12-24STM: capture type checking error (Closes: 3195)Enrico Tassi
2013-12-24Qed: feedback when type checking is doneEnrico Tassi
2013-12-24CoqIDE: new feedback "incomplete" to signal partial QedEnrico Tassi
2013-12-24Future: optional greedy chainingEnrico Tassi
2013-12-24cleanup warningEnrico Tassi
2013-12-24Simplifying the use of hypinfos in Rewrite.Pierre-Marie Pédrot
2013-12-23Rewrite.ml: removing direction flag from hypinfo.Pierre-Marie Pédrot
2013-12-22Do not pass unification flags around in Rewrite.Pierre-Marie Pédrot
2013-12-22Slight code cleaning ensuring more static invariants in Rewrite.Pierre-Marie Pédrot
2013-12-22Adding -bt to coqc.Pierre-Marie Pédrot
2013-12-22Adding a finer-grained -bt flag to coqtop only triggering backtraces.Pierre-Marie Pédrot
2013-12-22Notation variables are now taken into account as possible ltac bound variablesPierre-Marie Pédrot
2013-12-22Notations now accept the $(...)$ tactic-in-term syntax. They are resolved atPierre-Marie Pédrot
2013-12-22Notations can now accept dummy arguments. If ever a bound variable is notPierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 15:31:14 +0000