aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* Fix syntax highlighting of Scheme.Gravatar Guillaume Melquiond2015-03-06
* Do not highlight "using" as a constr keyword.Gravatar Guillaume Melquiond2015-03-06
* Add syntax highlighting for About.Gravatar Guillaume Melquiond2015-03-06
* Fix syntax highlighting of Save.Gravatar Guillaume Melquiond2015-03-06
* Fix syntax highlighting of Hypothesis, Axiom, Variable, Parameter, and Context.Gravatar Guillaume Melquiond2015-03-06
* Add syntax highlighting for Coercion.Gravatar Guillaume Melquiond2015-03-06
* Fix syntax highlighting of "Require multiple libraries".Gravatar Guillaume Melquiond2015-03-06
* MMapPositive: another implementation of MMapsGravatar Pierre Letouzey2015-03-06
* Fix testsuite with respect to the new formatting of Fail messages.Gravatar Guillaume Melquiond2015-03-05
* Preprend Fail to all the expected failures in the documentation.Gravatar Guillaume Melquiond2015-03-05
* Do not prepend a "Error:" header when the error is expected by the user.Gravatar Guillaume Melquiond2015-03-05
* MMaps again : adding MMapList, an implementation by ordered listGravatar Pierre Letouzey2015-03-05
* Introducing MMaps, a modernized FMaps.Gravatar Pierre Letouzey2015-03-04
* Fix bug #3532, providing universe inconsistency information when aGravatar Matthieu Sozeau2015-03-04
* Fix test-suite file, this is open.Gravatar Matthieu Sozeau2015-03-03
* Fix bug #3732: firstorder was using detyping to build existentialGravatar Matthieu Sozeau2015-03-03
* Add missing test-suite files and update gitignore.Gravatar Matthieu Sozeau2015-03-03
* Add a test-suite file ensuring coinductives with primitive projectionsGravatar Matthieu Sozeau2015-03-03
* Fix test-suite file, this is currently a wontfix, but keep theGravatar Matthieu Sozeau2015-03-03
* Fix bug #3590, keeping evars that are not turned into named metas byGravatar Matthieu Sozeau2015-03-03
* Improving display of camlp4/camlp5 versions, library and binary locations.Gravatar Hugo Herbelin2015-03-03
* Reinstalling search of camlpX in camldir, when given, forGravatar Hugo Herbelin2015-03-03
* Typos in doc modules.Gravatar Hugo Herbelin2015-03-03
* Fix bug #4103: forgot to allow unfolding projections of cofixpoints likeGravatar Matthieu Sozeau2015-03-03
* Fix bug #4101, noccur_evar's expand_projection can legitimately failGravatar Matthieu Sozeau2015-03-03
* Fix bug introduced by my last commit, forgetting to adjust de BruijnGravatar Matthieu Sozeau2015-03-03
* Fix bug #4097.Gravatar Matthieu Sozeau2015-03-02
* Now accepting unit props in mutual definitionsGravatar Bruno Barras2015-03-02
* Coq_makefile clean target erases .coq-native dirs in . if they are emptyGravatar Pierre Boutillier2015-02-28
* Fixing the rule for ml4 depencies in coq_makefileGravatar mlasson2015-02-28
* Explicit in CHANGES incompatibilities introduced in patterns by b2953849 (or ...Gravatar Pierre Boutillier2015-02-28
* Adding a test for bug #3612.Gravatar Pierre-Marie Pédrot2015-02-27
* Removing the unused field ltacrecvars of tactic internalization.Gravatar Pierre-Marie Pédrot2015-02-27
* Fixing OCaml 3.12 compilation.Gravatar Pierre-Marie Pédrot2015-02-27
* Test for bug #3249.Gravatar Pierre-Marie Pédrot2015-02-27
* Fixing bug #3249.Gravatar Pierre-Marie Pédrot2015-02-27
* Taking current env and not global env in b286c9f4f42f (4 commits ago,Gravatar Hugo Herbelin2015-02-27
* simpl: honor Global for "simpl: never" (Close: 3206)Gravatar Enrico Tassi2015-02-27
* STM: Considering Stack_overflow as a normal tactic error (Close #3576)Gravatar Enrico Tassi2015-02-27
* Fix test for #3467, I had moved it in a dumb way.Gravatar Maxime Dénès2015-02-27
* Add support so that the type of a match in an inductive type with let-inGravatar Hugo Herbelin2015-02-27
* Hack so that refine_no_check accepts an argument which is a match on anGravatar Hugo Herbelin2015-02-27
* Fixing first part of bug #3210 (inference of pattern-matching returnGravatar Hugo Herbelin2015-02-27
* Fixing typo resulting in wrong printing of return clauses forGravatar Hugo Herbelin2015-02-27
* Fix test for #3848, still open.Gravatar Maxime Dénès2015-02-27
* Moving test for #3467 to closed after PMP's fix.Gravatar Maxime Dénès2015-02-27
* Fix test-suite files for bugs #2456 and #3593, still open.Gravatar Maxime Dénès2015-02-27
* Make coq_makefile generate double-colon rules for clean and archclean. (Fix b...Gravatar Guillaume Melquiond2015-02-27
* Somehow fixing bug #3467.Gravatar Pierre-Marie Pédrot2015-02-27
* Add test-suite file for #3649.Gravatar Maxime Dénès2015-02-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-17 12:46:34 +0000