aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Injection: do not fail when arguments have sort Prop.Gravatar Maxime Dénès2014-04-29
* Native compiler: hide compiled files in a .coq-native subdirectory.Gravatar Maxime Dénès2014-04-29
* Completing 5eb53b5bc8d765ed75e965f43f1084e18efc8790 (I unfortunatelyGravatar Hugo Herbelin2014-04-29
* Reduce the amount of "Coq <" prompts generated by coq_tex. (Partial fix for b...Gravatar Guillaume Melquiond2014-04-28
* Prevent coq_tex from generating curly quotes. (Partial fix for bug #2964)Gravatar Guillaume Melquiond2014-04-28
* Recognize Parameters as a command in coqdoc. (Fix for bug #3279)Gravatar Guillaume Melquiond2014-04-28
* Mark lazymatch as an Ltac keyword for coqdoc. (Fix for bug #3276)Gravatar Guillaume Melquiond2014-04-28
* Remove unused lookup table.Gravatar Guillaume Melquiond2014-04-28
* Fix broken commit 2bcb2cb.Gravatar Guillaume Melquiond2014-04-28
* Fix incorrect syntax highlighting after the Goal command.Gravatar Guillaume Melquiond2014-04-28
* Fixing coqdoc bug #3292 (unfortunate collision betweens the relativeGravatar Hugo Herbelin2014-04-28
* Fixing #3293 (eta-expansion at "match" printing time was failingGravatar Hugo Herbelin2014-04-28
* Adding a field ci_cstr_nargs to case_info and mind_consnrealargs toGravatar Hugo Herbelin2014-04-28
* Rewriting [lapply] tactic in the new monad.Gravatar Pierre-Marie Pédrot2014-04-27
* Giving true proof-terms in inversion instead of metas.Gravatar Pierre-Marie Pédrot2014-04-27
* coq_makefile: -I for the new stm/ dirGravatar Enrico Tassi2014-04-25
* Adding a stm/ folder, as asked during last workgroup. It was essentially movingGravatar Pierre-Marie Pédrot2014-04-25
* Removing Autoinstance once and for all.Gravatar Pierre-Marie Pédrot2014-04-25
* Removing useless try-with clauses in Goal.enter variants.Gravatar Pierre-Marie Pédrot2014-04-25
* Future: memory optimization when forcing a chained pure computationGravatar Enrico Tassi2014-04-25
* Opaqueproofs: sink futures when interactiveGravatar Enrico Tassi2014-04-25
* print futures in caml toplevel tooGravatar Enrico Tassi2014-04-25
* Fix a second, trickier, typo in Termops.eta_reduce_head.Gravatar Arnaud Spiwack2014-04-25
* Adding a debug printer for futures.Gravatar Pierre-Marie Pédrot2014-04-25
* Fixing various backtrace recordings.Gravatar Pierre-Marie Pédrot2014-04-25
* Fix a small typo in Termops.eta_reduce_head.Gravatar Arnaud Spiwack2014-04-25
* Adding a [fold_map] operation on constrs.Gravatar Pierre-Marie Pédrot2014-04-24
* Writing tclABSTRACT in the new monad. In particular the unsafe status is nowGravatar Pierre-Marie Pédrot2014-04-24
* Better representation of evar filters: we represent the vacuous filters ofGravatar Pierre-Marie Pédrot2014-04-23
* Removing dead code, thanks to new OCaml warnings and a bit of scripting.Gravatar Pierre-Marie Pédrot2014-04-23
* Import proof of decidability of negated formulas from Coquelicot.Gravatar Guillaume Melquiond2014-04-23
* Remove some uses of excluded middle.Gravatar Guillaume Melquiond2014-04-22
* Replace the proof of sig_forall_dec from Kaliszyk/O'Connor by the one from Co...Gravatar Guillaume Melquiond2014-04-22
* Add regression tests for 3188 and 3265Gravatar Jason Gross2014-04-22
* Removing the compatibility layer from Leminv. Also removed an undocumentedGravatar Pierre-Marie Pédrot2014-04-22
* Using the new monad tactic in Inv.Gravatar Pierre-Marie Pédrot2014-04-22
* Removing tactic compatibility layer from Elim.Gravatar Pierre-Marie Pédrot2014-04-22
* Small code cleaning in Tacticals.Gravatar Pierre-Marie Pédrot2014-04-22
* Simplifying interface of elimination tactics. They used dummy clausenvs, andGravatar Pierre-Marie Pédrot2014-04-22
* Adding a test for bug #2923.Gravatar Pierre-Marie Pédrot2014-04-20
* Adding a test for bug #3285.Gravatar Pierre-Marie Pédrot2014-04-20
* Fixing bug #3285.Gravatar Pierre-Marie Pédrot2014-04-20
* Adding a [map] primitive to the tactic monad. Hopefully this should beGravatar Pierre-Marie Pédrot2014-04-20
* Fixing missing headers.Gravatar Hugo Herbelin2014-04-16
* Closing bug #3260Gravatar Julien Forest2014-04-14
* Fix guard condition for nested cofixpoints in checker.Gravatar Maxime Dénès2014-04-10
* Fix guard condition for nested cofixpoints.Gravatar Maxime Dénès2014-04-10
* better description of bug 3251Gravatar Enrico Tassi2014-04-10
* Have the feedback bus as a backend for dumping globs.Gravatar Carst Tankink2014-04-10
* Dumpglob: factor out reference dumping.Gravatar Carst Tankink2014-04-10