aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Some fine-tuning after removal of automatic imports of coercions in r13310Gravatar herbelin2010-07-23
* Extension of the recursive notations mechanismGravatar herbelin2010-07-22
* Made coercions active only when modules are imported.Gravatar herbelin2010-07-22
* Reverted 13293 commited mistakenly. Sorry for the noise.Gravatar herbelin2010-07-18
* Tentative de suppression de l'import automatique des hints et coercions.Gravatar herbelin2010-07-18
* Fix (part of) bug #2347, de Bruijn bug in Program's pretyper.Gravatar msozeau2010-06-30
* Made tclABSTRACT normalize evars before saying it does not supportGravatar herbelin2010-06-29
* Fixed a bug introduced in a combination in r12807 and revealed inGravatar herbelin2010-06-28
* Applying François' patches about Canonical Projections (see #2302 and #2334).Gravatar herbelin2010-06-26
* Restored a "feature" of unification in pre-8.3 (it was used e.g. in aGravatar herbelin2010-06-25
* Added Chung-Kil Hur's smart "pattern" tactic (h_resolve).Gravatar herbelin2010-06-22
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Hack for fixing bug #2172 (see explanations in file rewrite-2172.v).Gravatar herbelin2010-06-18
* Addressed bug #2310 and replaced anomaly "unknown meta" raised by "refine"Gravatar herbelin2010-06-13
* Fixed bug #2135 (second-order unification was raising cryptic message)Gravatar herbelin2010-06-12
* Improved the inference of the return predicate in dependent pattern-matching.Gravatar herbelin2010-06-12
* Added rudimentary support for using constructors from the explicitGravatar herbelin2010-06-12
* Fixed a bug in evarutil.ml (wrong env of a postponed conversion problem).Gravatar herbelin2010-06-12
* Mainly made that evarconv is able to solve "?n = (fun x => x) ?n" (sic).Gravatar herbelin2010-06-11
* Fixed two bugs in pattern-matching compilationGravatar herbelin2010-06-10
* Added support for Ltac-matching terms with variables bound in the patternGravatar herbelin2010-06-06
* Documentation of pretype_id (minor commit).Gravatar herbelin2010-05-28
* Fixing Derive Inversion for new proof engineGravatar herbelin2010-05-26
* Fix bug 2307Gravatar pboutill2010-05-20
* Add (almost) compatibility with camlp4, without breaking support for camlp5Gravatar letouzey2010-05-19
* Remove compile-command pragmas for emacsGravatar letouzey2010-05-19
* Some ocamldoc comments + Fixing name of .coqrc.version file in refmanGravatar pboutill2010-05-18
* Applicative commutative cuts in Fixpoint guard conditionGravatar pboutill2010-05-18
* Improved the efficiency of evars traverals thanks to a split ofGravatar herbelin2010-05-13
* Added a few informations about file lineages (for the most part in kernel)Gravatar herbelin2010-05-09
* Deux commentaires retirés de ocamldoc.Gravatar aspiwack2010-05-07
* ocamldoc related fixesGravatar pboutill2010-05-03
* Various minor improvements of comments in mli for ocamldocGravatar letouzey2010-04-29
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-05 22:11:18 +0000