aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-09-20Added eta-expansion in kernel, type inference and tactic unification,herbelin
2010-09-11Improving a few error messages in Ltac interpretationherbelin
2010-08-02Fix [clenv_missing] to compute a better approximation of missingmsozeau
2010-07-29kernel conversion and reduction do not raise assert failure on ill-typed term...barras
2010-07-29fixed bug #2105 (compilation of free de Bruijn) and missing lift of predicate...barras
2010-07-27Minor fixes:msozeau
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-07-23Some fine-tuning after removal of automatic imports of coercions in r13310herbelin
2010-07-22Extension of the recursive notations mechanismherbelin
2010-07-22Made coercions active only when modules are imported.herbelin
2010-07-18Reverted 13293 commited mistakenly. Sorry for the noise.herbelin
2010-07-18Tentative de suppression de l'import automatique des hints et coercions.herbelin
2010-06-30Fix (part of) bug #2347, de Bruijn bug in Program's pretyper.msozeau
2010-06-29Made tclABSTRACT normalize evars before saying it does not supportherbelin
2010-06-28Fixed a bug introduced in a combination in r12807 and revealed inherbelin
2010-06-26Applying François' patches about Canonical Projections (see #2302 and #2334).herbelin
2010-06-25Restored a "feature" of unification in pre-8.3 (it was used e.g. in aherbelin
2010-06-22Added Chung-Kil Hur's smart "pattern" tactic (h_resolve).herbelin
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-06-18Hack for fixing bug #2172 (see explanations in file rewrite-2172.v).herbelin
2010-06-13Addressed bug #2310 and replaced anomaly "unknown meta" raised by "refine"herbelin
2010-06-12Fixed bug #2135 (second-order unification was raising cryptic message)herbelin
2010-06-12Improved the inference of the return predicate in dependent pattern-matching.herbelin
2010-06-12Added rudimentary support for using constructors from the explicitherbelin
2010-06-12Fixed a bug in evarutil.ml (wrong env of a postponed conversion problem).herbelin
2010-06-11Mainly made that evarconv is able to solve "?n = (fun x => x) ?n" (sic).herbelin
2010-06-10Fixed two bugs in pattern-matching compilationherbelin
2010-06-06Added support for Ltac-matching terms with variables bound in the patternherbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-09 18:29:13 +0000