aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-05-06md5 for MacOSPierre
2014-05-06Lemmas: export standard proof terminatorEnrico Tassi
2014-05-06Rewriting the proof monad mechanism. Now it uses pure OCaml code, withoutppedrot
2014-05-06Fix interface for template polymorphism, cleaning up code in all typing algor...Matthieu Sozeau
2014-05-06Properly reinstate old-style polymorphism in the kernel and pretyping/retyping.Matthieu Sozeau
2014-05-06Initial work on reintroducing old-style polymorphism for compatibility (the s...Matthieu Sozeau
2014-05-06Correct rebase on STM code. Thanks to E. Tassi for help on dealing withMatthieu Sozeau
2014-05-06Rework handling of universes on top of the STM, allowing for delayedMatthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-05-05Fix install target in Makefile after 6acf543800fe176ca7d47ef7165ebc14588efb6f.Maxime Dénès
2014-05-02Pos.iter arguments in a better order for cbn.Pierre Boutillier
2014-05-02Cbn is happier when ?SetPositive fixpoints have the set as recursive argumentPierre Boutillier
2014-05-02Eta contractions to please cbnPierre Boutillier
2014-05-02Update test-suite Makefile to handle coq-prog-argsJason Gross
2014-05-01Allowing the "Declare Instance" command anywhere. This was artificiallyPierre-Marie Pédrot
2014-05-01Fixing ml-doc.Pierre-Marie Pédrot
2014-04-30Fix Qcanon after changes on injection.Maxime Dénès
2014-04-30Document changes on injection.Maxime Dénès
2014-04-30Trying to improve the error messages of injection.Maxime Dénès
2014-04-29Injection: do not fail when arguments have sort Prop.Maxime Dénès
2014-04-29Native compiler: hide compiled files in a .coq-native subdirectory.Maxime Dénès
2014-04-29Completing 5eb53b5bc8d765ed75e965f43f1084e18efc8790 (I unfortunatelyHugo Herbelin
2014-04-28Reduce the amount of "Coq <" prompts generated by coq_tex. (Partial fix for b...Guillaume Melquiond
2014-04-28Prevent coq_tex from generating curly quotes. (Partial fix for bug #2964)Guillaume Melquiond
2014-04-28Recognize Parameters as a command in coqdoc. (Fix for bug #3279)Guillaume Melquiond
2014-04-28Mark lazymatch as an Ltac keyword for coqdoc. (Fix for bug #3276)Guillaume Melquiond
2014-04-28Remove unused lookup table.Guillaume Melquiond
2014-04-28Fix broken commit 2bcb2cb.Guillaume Melquiond
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-28 23:33:15 +0000