aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* ratrapage exception, deja fait ...Gravatar bgregoir2011-01-11
* Fixing an uncaught exception bug with use of vmcastGravatar herbelin2011-01-07
* mli comments for docGravatar pboutill2011-01-07
* Rename mkR* smart constructors (mostly in funind)Gravatar glondu2010-12-25
* More {raw => glob} changes for consistencyGravatar glondu2010-12-24
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Change of nomenclature: rawconstr -> glob_constrGravatar glondu2010-12-23
* Fixing bug #2454: inversion predicate strategy for inferring the typeGravatar herbelin2010-12-19
* Univ.constraints made fully abstract instead of being a Set of abstract stuffGravatar letouzey2010-12-18
* Misc improvements about evar_mapGravatar letouzey2010-12-15
* Refresh universes in params when generating schemes (Closes: #2429)Gravatar glondu2010-11-08
* Delayed the evar normalization in error messages to the last minuteGravatar herbelin2010-11-07
* An experimental support for open constrs in hints and in "using"Gravatar herbelin2010-10-31
* Cleaning the use of parentheses around evd and evdref (cosmetic commit).Gravatar herbelin2010-10-31
* Slight cosmetic cleaning of tacred.ml.Gravatar herbelin2010-10-31
* Fixing the Not_found error in bug #2404 + dead code removal in cases.mlGravatar herbelin2010-10-06
* Improve handling of metas as evars in unification (patch by Hugo)Gravatar letouzey2010-09-30
* Speed-up refine by avoiding some calls to Evd.foldGravatar letouzey2010-09-30
* Fix bug #2321, allowing "_" named projections in classes. Not realizingGravatar msozeau2010-09-28
* Remove some occurrences of "open Termops"Gravatar glondu2010-09-28
* Remove "init" label from Termops.it_mk* specialized functionsGravatar glondu2010-09-28
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Added eta-expansion in kernel, type inference and tactic unification,Gravatar herbelin2010-09-20
* Improving a few error messages in Ltac interpretationGravatar herbelin2010-09-11
* Fix [clenv_missing] to compute a better approximation of missingGravatar msozeau2010-08-02
* kernel conversion and reduction do not raise assert failure on ill-typed term...Gravatar barras2010-07-29
* fixed bug #2105 (compilation of free de Bruijn) and missing lift of predicate...Gravatar barras2010-07-29
* Minor fixes:Gravatar msozeau2010-07-27
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 14:54:47 +0000