aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* 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
* Forgotten hints.ml{,i} files in 38b34dfffcc.Gravatar Hugo Herbelin2014-10-08
* Adding a printer for hints.Gravatar Hugo Herbelin2014-10-07
* Splitting out of auto.ml a file hints.ml dedicated to hints so as toGravatar Hugo Herbelin2014-10-07
* Add test-suite file for the projection unfolding bug I just fixed.Gravatar Matthieu Sozeau2014-10-07
* Fix test-suite file 3352 which was containing the wrong test.Gravatar Matthieu Sozeau2014-10-07
* Fix test-suite file to test original bug, not the failure of the guardGravatar Matthieu Sozeau2014-10-07
* Build unfolded versions of the primitive projection in let (a, p) := ...Gravatar Matthieu Sozeau2014-10-07
* Fixing #3687 (inconsistent lexer state after a bullet).Gravatar Hugo Herbelin2014-10-07
* Removing debugging information committed by mistake.Gravatar Hugo Herbelin2014-10-07
* Avoid a warning with Meta's names in debugger.Gravatar Hugo Herbelin2014-10-07
* coq_makefile: explicit target install-toploop for toploop pluginsGravatar Enrico Tassi2014-10-07
* Make tclEFFECTS also update the env in the proof monadGravatar Enrico Tassi2014-10-06
* fix wrong escaping in coq_makefileGravatar Enrico Tassi2014-10-06
* decl_mode: stay in declarative modeGravatar Enrico Tassi2014-10-06
* Semantic fix of a refine in Rewrite.Gravatar Pierre-Marie Pédrot2014-10-05
* Check compatibility of types in change depending on whether it is aGravatar Hugo Herbelin2014-10-05
* A few improvements on pattern-matching compilation.Gravatar Hugo Herbelin2014-10-05
* A few Global.env removed.Gravatar Hugo Herbelin2014-10-04
* Fixing #3193 (honoring implicit arguments in local definitions).Gravatar Hugo Herbelin2014-10-03
* Classify segfaults as failures in opened bugs.Gravatar Xavier Clerc2014-10-03
* Classify segfaults as failures in opened bugsGravatar Xavier Clerc2014-10-03
* Fixing #3606 continued (doc of Scheme Boolean Equality Scheme).Gravatar Hugo Herbelin2014-10-03
* Removing deactivated command Show Tree.Gravatar Hugo Herbelin2014-10-03
* Fixing #3657 (check that both sides of a "change with" have the sameGravatar Hugo Herbelin2014-10-03
* Test for bug #3652 fixed in 0fb36157b9baGravatar Hugo Herbelin2014-10-03
* Fixing ennoying warning about evars named ?23 and so on.Gravatar Hugo Herbelin2014-10-03
* Fixing #3623 (unbound evars in types in a call to "change with").Gravatar Hugo Herbelin2014-10-03
* Add a bunch of reproduction files for bugs.Gravatar Xavier Clerc2014-10-03
* Fixing #3634 (wrong env in "cannot instantiate because not in itsGravatar Hugo Herbelin2014-10-03
* Adapting output/Arguments_renaming continued.Gravatar Hugo Herbelin2014-10-03
* Implement module subtyping for polymorphic constants (errors onGravatar Matthieu Sozeau2014-10-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 11:22:02 +0000