aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* Fix test-suite file after moving back to using C as the nameGravatar Matthieu Sozeau2014-10-15
* Modify the heuristic for unfolding lhs or rhs in evarconv, consideringGravatar Matthieu Sozeau2014-10-15
* Implement a different strategy to expand primitive projections only whenGravatar Matthieu Sozeau2014-10-15
* Add an option to not print primitive projection parameters, which canGravatar Matthieu Sozeau2014-10-15
* Fix -async-proofs-always-delegate (close 3740)Gravatar Enrico Tassi2014-10-15
* Fix ML paths (thanks Jean-Marc Notin for bisecting it)Gravatar Enrico Tassi2014-10-14
* Revert "Move eta-expansion after delta reduction in kernel reduction. This ma...Gravatar Matthieu Sozeau2014-10-14
* Oops, forgot a fix needed after the rebase.Gravatar Matthieu Sozeau2014-10-14
* Fix bug #3698: stack overflow due to eta+canonical structures inGravatar Matthieu Sozeau2014-10-14
* Fix typo, thanks Mike Shulman for spotting itGravatar Enrico Tassi2014-10-13
* Fixing "change" and "fold" after convert_hyp/convert_concl moved toGravatar Hugo Herbelin2014-10-13
* Add support for deactivating type class inference from induction/destruct.Gravatar Hugo Herbelin2014-10-13
* Adding a tactic which fails if one of the goals under focus is dependent in a...Gravatar Hugo Herbelin2014-10-13
* Adding printers for ppproofview.Gravatar Hugo Herbelin2014-10-13
* Naming main goal "Main"Gravatar Hugo Herbelin2014-10-13
* Moving function about locs in locusops.Gravatar Hugo Herbelin2014-10-13
* English typo in a function name of evarconv.Gravatar Hugo Herbelin2014-10-13
* Added support for several impossible cases in compilation of "match".Gravatar Hugo Herbelin2014-10-13
* Stm: more precise representation of nested proofsGravatar Enrico Tassi2014-10-13
* When loading libraries, feed back dependencies.Gravatar Carst Tankink2014-10-13
* Emit a warning for void Arguments statement (Close 3713)Gravatar Enrico Tassi2014-10-13
* Parsing of "?[" as two tokens (makes ssr compile).Gravatar Enrico Tassi2014-10-13
* STM: primitives to snapshot a .vi while in interactive modeGravatar Enrico Tassi2014-10-13
* selective join/export of the safe_environmentGravatar Enrico Tassi2014-10-13
* TQueue: new primitive to take a snapshot of the queueGravatar Enrico Tassi2014-10-13
* STM: simplify how the term part of a side effect is retrievedGravatar Enrico Tassi2014-10-13
* library/opaqueTables: enable their use in interactive modeGravatar Enrico Tassi2014-10-13
* Coqinit: look in toploop/ even if configured with -localGravatar Enrico Tassi2014-10-13
* Mentioning incompatibility shown in #3718 and coming from #3050Gravatar Hugo Herbelin2014-10-13
* Tentative fix for a badly used Option.get in Reductionops.Gravatar Pierre-Marie Pédrot2014-10-12
* Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameGravatar Matthieu Sozeau2014-10-11
* Do not expand primitive projections eagerly in evarconv, but onlyGravatar Matthieu Sozeau2014-10-10
* Give the same argument name for the record binder of type classGravatar Matthieu Sozeau2014-10-10
* Add debug printers for projections, fix printing of evar constraintsGravatar Matthieu Sozeau2014-10-10
* Add a "Debug Tactic Unification" option and correct the first-orderGravatar Matthieu Sozeau2014-10-10
* Make constrMatching and detyping more robust with respect toGravatar Matthieu Sozeau2014-10-10
* Fix bug due to shadowing a variable name in tacredGravatar Matthieu Sozeau2014-10-10
* Fix segfault in native compiler on int31 division.Gravatar Maxime Dénès2014-10-10
* No need anymore for referring to xml directory in MLINCLUDES.Gravatar Hugo Herbelin2014-10-09
* Restoring plugins/xml/README erased by mistake.Gravatar Hugo Herbelin2014-10-09
* Propagating name of goal to main subgoal in cut and conversion tactics.Gravatar Hugo Herbelin2014-10-09
* Added support for having one subgoal inheriting the name of its father in Ref...Gravatar Hugo Herbelin2014-10-09
* Removing Convert_concl and Convert_hyp from Logic.Gravatar Hugo Herbelin2014-10-09
* A version of convert_concl and convert_hyp in new proof engine.Gravatar Hugo Herbelin2014-10-09
* Adding printer for named_context_val and Goal.goal in debugger.Gravatar Hugo Herbelin2014-10-09
* Fixup leading ./ path cleaningGravatar Pierre Boutillier2014-10-09
* Coq_makefile: Allow empty logical namesGravatar Pierre Boutillier2014-10-09
* fix make mlidocGravatar Pierre Boutillier2014-10-08
* Fixing the anomaly in bug #3045 (a filter was not type-safe inGravatar Hugo Herbelin2014-10-08
* Applying Virgile Prevosto's patch for better error report in coqdep (#3029).Gravatar Hugo Herbelin2014-10-08
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-02 20:07:09 +0000