aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Misc small fixes : warning, dep cycles, ocamlbuild...Gravatar letouzey2010-04-26
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
* Fixed bugs from commit 12954 on unification complexityGravatar herbelin2010-04-20
* Reduced the complexity of evar instantiations from O(n^3) to less than O(n^2).Gravatar herbelin2010-04-19
* Recovering 8.2 behavior of "simple (e)apply" (and hence of "(e)auto").Gravatar herbelin2010-04-11
* Added a function in typing.ml to solve evars of a constr w/o going back down ...Gravatar herbelin2010-04-05
* Granting wish #2251 (forbidding rewriting a term reduced to an evar)Gravatar herbelin2010-04-05
* Partial fix to bug #2244 (ensure that pattern unification does notGravatar herbelin2010-04-05
* Extended on-the-fly eta-expansion in coercion mechanism to sort-polymorphicGravatar herbelin2010-03-28
* Fixing bug #2279 (printing nested let-in was in exponential time)Gravatar herbelin2010-03-27
* Stop dropping evar constraints when building a new goal evar defs.Gravatar msozeau2010-03-15
* Fix splitting evars tactics and stop dropping evar constraints whenGravatar msozeau2010-03-15
* fixed confusion between number of cstr arguments and number of pattern variab...Gravatar barras2010-03-12
* fix [Search] when the result has no hypothesis & constant comparisonGravatar puech2010-03-11
* Reorder resolution of type class and unification constraints.Gravatar msozeau2010-03-07
* Fix treatment of remaining unification constraints: raise a moreGravatar msozeau2010-03-07
* Improve unification when evars and metas are mixed.Gravatar msozeau2010-02-22
* Compute the correct generalization information when discharging a classGravatar msozeau2010-02-16
* Fix [Existing Class] impl and add documentation. Fix computation of theGravatar msozeau2010-02-10
* Quick fix for references to section variables unbound in the currentGravatar msozeau2010-01-26
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 07:21:04 +0000