aboutsummaryrefslogtreecommitdiff
path: root/kernel/inductive.ml
AgeCommit message (Expand)Author
2013-10-24inductive.ml : get rid of some obvious (Lazy.force (lazy t))letouzey
2013-10-24Rtree : cleanup of the comparing codeletouzey
2013-10-24Turn many List.assoc into List.assoc_fletouzey
2013-09-19Get rid of the uses of deprecated OCaml elements (still remaining compatible ...xclerc
2013-05-14Delayed the computation of parameters in sort polymorphism ofherbelin
2013-04-29Merging Context and Sign.ppedrot
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-03-23Minor code cleaning in CArray / CList.ppedrot
2013-02-26kernel/declarations becomes a pure mliletouzey
2013-01-28Uniformization of the "anomaly" command.ppedrot
2012-12-19Array.create is deprecatedpboutill
2012-12-14Modulification of identifierppedrot
2012-11-22Monomorphization (kernel)ppedrot
2012-11-13More monomorphizationsppedrot
2012-11-08Monomorphized a lot of equalities over OCaml integers, thanks toppedrot
2012-09-14As r15801: putting everything from Util.array_* to CArray.*.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-08-08Updating headers.herbelin
2012-03-02Noise for nothingpboutill
2011-10-05It happens that the type inference algorithm (pretyping) did not checkherbelin
2011-07-04Extraction: forbid Prop-polymorphism of inductives when extracting to Ocamlletouzey
2010-12-18Univ.constraints made fully abstract instead of being a Set of abstract stuffletouzey
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-03"Improved" the form of the inferred type of "match" byherbelin
2010-05-20fixed guard check with commutative cutsbarras
2010-05-18Applicative commutative cuts in Fixpoint guard conditionpboutill
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-03-12fixed confusion between number of cstr arguments and number of pattern variab...barras
2010-03-11introduced lazy computation of size info in the guard conditionbarras
2009-12-07revert on commit r12553barras
2009-12-01two improvements of the guard condition:barras
2009-10-21This big commit addresses two problems:soubiran
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-08-11Ensures that let-in's in arities of inductive types work well. Maybe notherbelin
2009-07-15- Fixing bug #2139 (kernel-based test of well-formation of eliminationherbelin
2008-12-02fixed kernel bug (de Bruijn) + test-suitebarras
2008-10-07fixing r11433 again:barras
2008-10-07fixed pb with r11433barras
2008-10-06bug #1951: polymorphic indtypes: universe subst was not performed in the type...barras
2008-07-25Correction d'une incohérence de typage des inductifs polymorphes: lesherbelin
2008-07-17Uniformisation du format des messages d'erreur (commencent par uneherbelin
2008-05-12Changement de stratégie vis à vis du commit 10859 sur la gestion desherbelin
2008-04-27Correction du bug des types singletons pas sous-type de Setherbelin
2008-04-23Prise en compte des coercions dans les clauses "with" même si le typeherbelin
2008-03-18improved the implementation of rtreebarras
2008-02-08Add more information to IllFormedRecBody exceptions, to show the exactmsozeau
2007-10-04Correction bug 1718 (lazy delta unfolding used to miss delta on rels and vars)herbelin
2006-12-12cosmetiquebarras
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:34:06 +0000