aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* Properly reinstate old-style polymorphism in the kernel and pretyping/retyping.Gravatar Matthieu Sozeau2014-05-06
* Initial work on reintroducing old-style polymorphism for compatibility (the s...Gravatar Matthieu Sozeau2014-05-06
* Correct rebase on STM code. Thanks to E. Tassi for help on dealing withGravatar Matthieu Sozeau2014-05-06
* Rework handling of universes on top of the STM, allowing for delayedGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Fix install target in Makefile after 6acf543800fe176ca7d47ef7165ebc14588efb6f.Gravatar Maxime Dénès2014-05-05
* Pos.iter arguments in a better order for cbn.Gravatar Pierre Boutillier2014-05-02
* Cbn is happier when ?SetPositive fixpoints have the set as recursive argumentGravatar Pierre Boutillier2014-05-02
* Eta contractions to please cbnGravatar Pierre Boutillier2014-05-02
* Update test-suite Makefile to handle coq-prog-argsGravatar Jason Gross2014-05-02
* Allowing the "Declare Instance" command anywhere. This was artificiallyGravatar Pierre-Marie Pédrot2014-05-01
* Fixing ml-doc.Gravatar Pierre-Marie Pédrot2014-05-01
* Fix Qcanon after changes on injection.Gravatar Maxime Dénès2014-04-30
* Document changes on injection.Gravatar Maxime Dénès2014-04-30
* Trying to improve the error messages of injection.Gravatar Maxime Dénès2014-04-30
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2025-02-02 22:07:45 +0000