aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* Promote evar_defs to evar_map (in Evd)Gravatar glondu2009-11-11
* Redoing broken commit r12498 (fixing bug #2167 + attempt to test theGravatar herbelin2009-11-11
* Fixing bug #2167 + attempt to test the compatibility of a more robustGravatar herbelin2009-11-11
* Commit 12485 continued.Gravatar herbelin2009-11-09
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
* Took local definitions into account in the test for deciding whetherGravatar herbelin2009-11-08
* - Fix discharge bug in typeclasses: some constrs were not actuallyGravatar msozeau2009-11-06
* Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.Gravatar gmelquio2009-11-04
* Reverted an incorrect code simplification in function status_changedGravatar herbelin2009-11-02
* Attempt to capture on time unification errors for "with" bindings.Gravatar herbelin2009-10-30
* Take constraints into account in the "instantiate" tacticGravatar herbelin2009-10-30
* Fix bug in dnet.ml, which missed some results when filtering one term against...Gravatar puech2009-10-29
* Integrate a few improvements on typeclasses and Program from the equations br...Gravatar msozeau2009-10-28
* Remove old compatibility stuff (Tacred.nf)Gravatar glondu2009-10-28
* Make usage of Dyn explicitGravatar glondu2009-10-28
* Fixes around typeclasses:Gravatar msozeau2009-10-27
* Improved the treatment of Local/Global options (noneffective Local onGravatar herbelin2009-10-25
* First debug... the renaming of librairies was not working and auto/dn were no...Gravatar soubiran2009-10-23
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Changed the way to support compatibility with previous versions.Gravatar herbelin2009-10-04
* - Fixed a bug in checking that implicit arguments are all correctlyGravatar herbelin2009-09-18
* Remove useless Liboject.export_function fieldGravatar glondu2009-09-17
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* - Inductive types in the "using" option of auto/eauto/firstorder areGravatar herbelin2009-09-13
* Fix the bug-ridden code used to choose leibniz or generalizedGravatar msozeau2009-09-08
* A new kind of automatically generated scheme "congr" for equality typesGravatar herbelin2009-08-23
* Death of "survive_module" and "survive_section" (the first one wasGravatar herbelin2009-08-13
* Made unification patch 12268 even more ad hoc (if evars remain in aGravatar herbelin2009-08-13
* Ensures that let-in's in arities of inductive types work well. Maybe notGravatar herbelin2009-08-11
* Relatively ad hoc fix to an ill-typed instantiation bug in typeGravatar herbelin2009-08-11
* Fixed incorrect optimization in Prettyp.pr_located_qualid introducedGravatar herbelin2009-08-07
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* Improved parameterization of Coq:Gravatar herbelin2009-08-02
* - Fixing bug #2139 (kernel-based test of well-formation of eliminationGravatar herbelin2009-07-15
* Use the proper unification flags in e_exact. This makes exact fail a bitGravatar msozeau2009-07-09
* Fixed bug #2116 ("simpl" created ill-typed term while acceptingGravatar herbelin2009-07-08
* Don't use recent ocaml tolerance for pattern "ProjectVar _" whenGravatar herbelin2009-07-08
* Reactivation of pattern unification of evars in apply unification, inGravatar herbelin2009-07-08
* Add heuristic based on non-linearity of evars to determine whether anGravatar herbelin2009-07-08
* Fixing bug 2129 (evar introduced to remember an ambiguous projectionGravatar herbelin2009-07-08
* Jolification : tentative de supprimer les "( evd)" et associés quiGravatar aspiwack2009-07-07
* change in the order of unification constraints solving (for canonical structu...Gravatar amahboub2009-07-06
* Add new variants of [rewrite] and [autorewrite] which differ in theGravatar msozeau2009-06-30
* Improve return predicate inference by making the return type dependentGravatar msozeau2009-06-28
* Fixes for r12197, the refined evars were not returned in case fail_evarGravatar msozeau2009-06-22
* documented a bug of pattern unification with metasGravatar barras2009-06-22
* Use more consistent resolution parameters in Program and regular typingGravatar msozeau2009-06-18
* Fix "unsatisfiable constraints" error messages to include all theGravatar msozeau2009-06-18
* Try typeclass resolution in coercion if no solution can be found to aGravatar msozeau2009-06-18
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-20 04:21:28 +0000