aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* Removing some betaiota-redexes in error messages (an experiment)Gravatar herbelin2010-01-12
* Typo in error messageGravatar herbelin2010-01-12
* Added module sharing support for typeclasses and hints (pri_auto_tactic).Gravatar soubiran2010-01-12
* Fix handling of instance declarations in presence of let-ins (bugGravatar msozeau2010-01-01
* Fixing bug #2193: computation of dependencies in the "match" returnGravatar herbelin2009-12-30
* In "simpl c" and "change c with d", c can be a pattern.Gravatar herbelin2009-12-24
* Opened the possibility to type Ltac patterns but it is not fully functional yetGravatar herbelin2009-12-24
* Attached evar source to the evar_info and add location to tclWITHHOLES errorsGravatar herbelin2009-12-22
* Generic support for open terms in tacticsGravatar herbelin2009-12-21
* In "progress", extending the set of evars w/o solving an existing one isGravatar herbelin2009-12-21
* Improved strategy for rewriting lemma possibly depending because of evars.Gravatar herbelin2009-12-14
* Still continuing r12485-12486, r12549, r12556 (cleaning around name generation)Gravatar herbelin2009-12-03
* Continuing r12485-12486 and r12549 (cleaning around name generation)Gravatar herbelin2009-12-02
* Continuing r12485-12486 (cleaning around name generation)Gravatar herbelin2009-12-01
* Added support for definition of fixpoints using tactics.Gravatar herbelin2009-11-27
* Fix type class discharge again.Gravatar msozeau2009-11-15
* Backtrack on fixing #2167Gravatar herbelin2009-11-12
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 02:34:11 +0000