aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-02-27Tacinterp: refactoring using Monad.Arnaud Spiwack
2014-02-27Code refactoring thanks to the new Monad module.Arnaud Spiwack
2014-02-27Remove unsafe code (Obj.magic) in Tacinterp.Arnaud Spiwack
2014-02-27Proofview.Notations: Now that (>>=) is free, use it for tclBIND.Arnaud Spiwack
2014-02-27Get rid of the enterl/glist API for Proofview.Goal.Arnaud Spiwack
2014-02-27Tacinterp: yet another superfluous enterl.Arnaud Spiwack
2014-02-27Tacinterp: spurious enterl.Arnaud Spiwack
2014-02-27Dead code: eval_ltac_constr.Arnaud Spiwack
2014-02-26STM: better debug messagesEnrico Tassi
2014-02-26STM: do not print goals on UndoEnrico Tassi
2014-02-26CoqIDE: print message of "Fail" commandEnrico Tassi
2014-02-26refman: document vi2voEnrico Tassi
2014-02-26STM: better messages when checking/finishing tasksEnrico Tassi
2014-02-26Library: when compiling multiple files, reset the opaque tablesEnrico Tassi
2014-02-26STM: when batch compiling a vo, assert we behave conservativelyEnrico Tassi
2014-02-26coq_makefile: new target vi2voEnrico Tassi
2014-02-26vi2vo: new flag -schedule-vi2voEnrico Tassi
2014-02-26Lazyconstr -> OpaqueproofEnrico Tassi
2014-02-26STM: backup/restore remote countersEnrico Tassi
2014-02-26remoteCounter: backup/restoreEnrico Tassi
2014-02-26univ: removing dead codeEnrico Tassi
2014-02-26checker and votour ported to new vo format (after -vi2vo)Enrico Tassi
2014-02-26New compilation mode -vi2voEnrico Tassi
2014-02-26votour: better error messagesEnrico Tassi
2014-02-26checker: less useless error messagesEnrico Tassi
2014-02-26fix checker w.r.t. mutual_inductive_body and constant_bodyEnrico Tassi
2014-02-26fix checker w.r.t. Dyn.t validationEnrico Tassi
2014-02-26Future: make ~greedy:true the default + new sink commodity APIEnrico Tassi
2014-02-26Future: each computation has a uuidEnrico Tassi
2014-02-25Tacinterp: remove the is_value check in Ltac's let-in.Arnaud Spiwack
2014-02-25Tacinterp: fewer enterl still.Arnaud Spiwack
2014-02-25Tacinterp: fewer Proofview.Goal.enterl.Arnaud Spiwack
2014-02-25Tacinterp: clean up.Arnaud Spiwack
2014-02-25Tacinterp: remove unnecessary return/bind pairs.Arnaud Spiwack
2014-02-25Fixing printing of only_parsing notations.Pierre-Marie Pédrot
2014-02-24TacticMatching: avoid some closure allocation in (<*>).Arnaud Spiwack
2014-02-24Removed some trailing whitespaces.Arnaud Spiwack
2014-02-24IStream: more efficient implementation of concat_map.Arnaud Spiwack
2014-02-24IStream: a concat_map primitive.Arnaud Spiwack
2014-02-24IStream: change type of thunk, spare allocations.Arnaud Spiwack
2014-02-24IStream: remove a useless Obj.magic.Arnaud Spiwack
2014-02-24A view type for IStream.Arnaud Spiwack
2014-02-24Ensuring that the module Stack is opaque inside Reductionops.Pierre-Marie Pédrot
2014-02-24make coqide-binaries does not build coqtop anymorePierre Boutillier
2014-02-24fixup complement FinPierre Boutillier
2014-02-24cbn understands ArgumentsPierre Boutillier
2014-02-24Simpl_behaviour becomes Reductionops.ReductionBehaviourPierre Boutillier
2014-02-24Dead Code eliminationPierre Boutillier
2014-02-24Create Debug Unification optionPierre Boutillier
2014-02-24Fix coqide build under MacOSPierre Boutillier
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 05:00:45 +0000