aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2010-05-28Documentation of pretype_id (minor commit).herbelin
2010-05-26Fixing Derive Inversion for new proof engineherbelin
2010-05-20Fix bug 2307pboutill
2010-05-19Add (almost) compatibility with camlp4, without breaking support for camlp5letouzey
2010-05-19Remove compile-command pragmas for emacsletouzey
2010-05-18Some ocamldoc comments + Fixing name of .coqrc.version file in refmanpboutill
2010-05-18Applicative commutative cuts in Fixpoint guard conditionpboutill
2010-05-13Improved the efficiency of evars traverals thanks to a split ofherbelin
2010-05-09Added a few informations about file lineages (for the most part in kernel)herbelin
2010-05-07Deux commentaires retirés de ocamldoc.aspiwack
2010-05-03ocamldoc related fixespboutill
2010-04-29Various minor improvements of comments in mli for ocamldocletouzey
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2010-04-26Misc small fixes : warning, dep cycles, ocamlbuild...letouzey
2010-04-22Here comes the commit, announced long ago, of the new tactic engine.aspiwack
2010-04-20Fixed bugs from commit 12954 on unification complexityherbelin
2010-04-19Reduced the complexity of evar instantiations from O(n^3) to less than O(n^2).herbelin
2010-04-11Recovering 8.2 behavior of "simple (e)apply" (and hence of "(e)auto").herbelin
2010-04-05Added a function in typing.ml to solve evars of a constr w/o going back down ...herbelin
2010-04-05Granting wish #2251 (forbidding rewriting a term reduced to an evar)herbelin
2010-04-05Partial fix to bug #2244 (ensure that pattern unification does notherbelin
2010-03-28Extended on-the-fly eta-expansion in coercion mechanism to sort-polymorphicherbelin
2010-03-27Fixing bug #2279 (printing nested let-in was in exponential time)herbelin
2010-03-15Stop dropping evar constraints when building a new goal evar defs.msozeau
2010-03-15Fix splitting evars tactics and stop dropping evar constraints whenmsozeau
2010-03-12fixed confusion between number of cstr arguments and number of pattern variab...barras
2010-03-11fix [Search] when the result has no hypothesis & constant comparisonpuech
2010-03-07Reorder resolution of type class and unification constraints.msozeau
2010-03-07Fix treatment of remaining unification constraints: raise a moremsozeau
2010-02-22Improve unification when evars and metas are mixed.msozeau
2010-02-16Compute the correct generalization information when discharging a classmsozeau
2010-02-10Fix [Existing Class] impl and add documentation. Fix computation of themsozeau
2010-01-26Quick fix for references to section variables unbound in the currentmsozeau
2010-01-12Removing some betaiota-redexes in error messages (an experiment)herbelin
2010-01-12Typo in error messageherbelin
2010-01-12Added module sharing support for typeclasses and hints (pri_auto_tactic).soubiran
2010-01-01Fix handling of instance declarations in presence of let-ins (bugmsozeau
2009-12-30Fixing bug #2193: computation of dependencies in the "match" returnherbelin
2009-12-24In "simpl c" and "change c with d", c can be a pattern.herbelin
2009-12-24Opened the possibility to type Ltac patterns but it is not fully functional yetherbelin
2009-12-22Attached evar source to the evar_info and add location to tclWITHHOLES errorsherbelin
2009-12-21Generic support for open terms in tacticsherbelin
2009-12-21In "progress", extending the set of evars w/o solving an existing one isherbelin
2009-12-14Improved strategy for rewriting lemma possibly depending because of evars.herbelin
2009-12-03Still continuing r12485-12486, r12549, r12556 (cleaning around name generation)herbelin
2009-12-02Continuing r12485-12486 and r12549 (cleaning around name generation)herbelin
2009-12-01Continuing r12485-12486 (cleaning around name generation)herbelin
2009-11-27Added support for definition of fixpoints using tactics.herbelin
2009-11-15Fix type class discharge again.msozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 07:54:44 +0000