aboutsummaryrefslogtreecommitdiff
path: root/pretyping/coercion.ml
AgeCommit message (Expand)Author
2014-03-01Fixing pervasive comparisonsPierre-Marie Pédrot
2014-02-12TC: honor the use_typeclasses flag in pretypingEnrico Tassi
2013-09-19Get rid of the uses of deprecated OCaml elements (still remaining compatible ...xclerc
2013-09-18Removing almost all new_untyped_evar, and a bunch of Evd.add.ppedrot
2013-05-09Uniformization: isevars -> evdref/sigma/evdherbelin
2013-05-06Small cleaning of Evd interface.ppedrot
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-03-23Minor code cleaning in CArray / CList.ppedrot
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 12)letouzey
2013-02-17Added propagation of evars unification failure reasons for betterherbelin
2013-01-28Uniformization of the "anomaly" command.ppedrot
2012-12-14Modulification of identifierppedrot
2012-11-26Removed some FIXME related to equality on universes.ppedrot
2012-11-22Monomorphization (pretyping)ppedrot
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-09-14The new ocaml compiler (4.00) has a lot of very cool warnings,regisgia
2012-08-08Updating headers.herbelin
2012-07-11Fix regression introduced in r15418 that broke MathClasses. In program mode, ...msozeau
2012-06-04Forward-port fixes from 8.4 (15358, 15353, 15333).msozeau
2012-05-29Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evdletouzey
2012-04-25Avoid unneeded head-normalizations in coercion code.msozeau
2012-04-25Do not delta-head-normalize the proposition argument of sigma types during co...msozeau
2012-03-20Fix interface of resolve_typeclasses: onlyargs -> with_goals:msozeau
2012-03-19Fix bugs related to Program integration.msozeau
2012-03-14Second step of integration of Program:msozeau
2012-03-14Remove support for "abstract typing constraints" that requires unicity of sol...msozeau
2012-03-02Noise for nothingpboutill
2011-10-25Fixing use of type constraint for refining the "return" clause of "match".herbelin
2011-04-08Applying and reworking Tom Prince's patch for test-suite/failure/universes2.vherbelin
2011-03-07Reverted commit r13893 about propagation of more informativeherbelin
2011-03-07Added propagation of evars unification failure reasons for betterherbelin
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-10-31Cleaning the use of parentheses around evd and evdref (cosmetic commit).herbelin
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-05-09Added a few informations about file lineages (for the most part in kernel)herbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-03-28Extended on-the-fly eta-expansion in coercion mechanism to sort-polymorphicherbelin
2009-11-11Promote evar_defs to evar_map (in Evd)glondu
2009-10-28Integrate a few improvements on typeclasses and Program from the equations br...msozeau
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-07-07Jolification : tentative de supprimer les "( evd)" et associés quiaspiwack
2009-06-18Try typeclass resolution in coercion if no solution can be found to amsozeau
2009-04-08Some dead code removal + cleanupsletouzey
2009-02-19On remplace evar_map par evar_defs (seul evar_defs est désormais exporté aspiwack
2008-09-02Propagating commit 11343 from branch v8.2 to trunk (wish 1934 aboutherbelin
2008-06-21Various improvements in handling of evars in general and typingmsozeau
2008-05-05Mise en place d'un algorithme d'inversion des contraintes de type lorsherbelin
2008-04-26- Backtrack sur extension de syntaxe pour pose qui rentre en conflit avecherbelin
2008-04-23Prise en compte des coercions dans les clauses "with" même si le typeherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 11:42:28 +0000