aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-04-28Fix incorrect syntax highlighting after the Goal command.Guillaume Melquiond
2014-04-28Fixing coqdoc bug #3292 (unfortunate collision betweens the relativeHugo Herbelin
2014-04-28Fixing #3293 (eta-expansion at "match" printing time was failingHugo Herbelin
2014-04-28Adding a field ci_cstr_nargs to case_info and mind_consnrealargs toHugo Herbelin
2014-04-27Rewriting [lapply] tactic in the new monad.Pierre-Marie Pédrot
2014-04-27Giving true proof-terms in inversion instead of metas.Pierre-Marie Pédrot
2014-04-25coq_makefile: -I for the new stm/ dirEnrico Tassi
2014-04-25Adding a stm/ folder, as asked during last workgroup. It was essentially movingPierre-Marie Pédrot
2014-04-25Removing Autoinstance once and for all.Pierre-Marie Pédrot
2014-04-25Removing useless try-with clauses in Goal.enter variants.Pierre-Marie Pédrot
2014-04-25Future: memory optimization when forcing a chained pure computationEnrico Tassi
2014-04-25Opaqueproofs: sink futures when interactiveEnrico Tassi
2014-04-25print futures in caml toplevel tooEnrico Tassi
2014-04-25Fix a second, trickier, typo in Termops.eta_reduce_head.Arnaud Spiwack
2014-04-25Adding a debug printer for futures.Pierre-Marie Pédrot
2014-04-25Fixing various backtrace recordings.Pierre-Marie Pédrot
2014-04-25Fix a small typo in Termops.eta_reduce_head.Arnaud Spiwack
2014-04-24Adding a [fold_map] operation on constrs.Pierre-Marie Pédrot
2014-04-24Writing tclABSTRACT in the new monad. In particular the unsafe status is nowPierre-Marie Pédrot
2014-04-23Better representation of evar filters: we represent the vacuous filters ofPierre-Marie Pédrot
2014-04-23Removing dead code, thanks to new OCaml warnings and a bit of scripting.Pierre-Marie Pédrot
2014-04-23Import proof of decidability of negated formulas from Coquelicot.Guillaume Melquiond
2014-04-22Remove some uses of excluded middle.Guillaume Melquiond
2014-04-22Replace the proof of sig_forall_dec from Kaliszyk/O'Connor by the one from Co...Guillaume Melquiond
2014-04-22Add regression tests for 3188 and 3265Jason Gross
2014-04-22Removing the compatibility layer from Leminv. Also removed an undocumentedPierre-Marie Pédrot
2014-04-22Using the new monad tactic in Inv.Pierre-Marie Pédrot
2014-04-22Removing tactic compatibility layer from Elim.Pierre-Marie Pédrot
2014-04-22Small code cleaning in Tacticals.Pierre-Marie Pédrot
2014-04-22Simplifying interface of elimination tactics. They used dummy clausenvs, andPierre-Marie Pédrot
2014-04-20Adding a test for bug #2923.Pierre-Marie Pédrot
2014-04-20Adding a test for bug #3285.Pierre-Marie Pédrot
2014-04-20Fixing bug #3285.Pierre-Marie Pédrot
2014-04-20Adding a [map] primitive to the tactic monad. Hopefully this should bePierre-Marie Pédrot
2014-04-16Fixing missing headers.Hugo Herbelin
2014-04-14Closing bug #3260Julien Forest
2014-04-10Fix guard condition for nested cofixpoints in checker.Maxime Dénès
2014-04-10Fix guard condition for nested cofixpoints.Maxime Dénès
2014-04-10better description of bug 3251Enrico Tassi
2014-04-10Have the feedback bus as a backend for dumping globs.Carst Tankink
2014-04-10Dumpglob: factor out reference dumping.Carst Tankink
2014-04-10CoqIDE: options for syntax highlightingEnrico Tassi
2014-04-10CoqIDE: removing a timer may raise an exceptionEnrico Tassi
2014-04-10coqtop -batch refuses Back 1 but accepts Undo.Pierre Boutillier
2014-04-10By resolution of the CoqWG, instantiate must not be used now that refine worksPierre Boutillier
2014-04-10No more Coersion in Init.Pierre Boutillier
2014-04-10Define [projT3] and [proj3_sig]Jason Gross
2014-04-10Test case for bug 3037Jason Gross
2014-04-10Test case for 3164Jason Gross
2014-04-10Test case for bug 3262Jason Gross
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-23 22:09:37 +0000