aboutsummaryrefslogtreecommitdiff
path: root/pretyping/term_dnet.ml
AgeCommit message (Expand)Author
2014-05-08Moving Dnet-related code to tactics/.Pierre-Marie Pédrot
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-28Adding a field ci_cstr_nargs to case_info and mind_consnrealargs toHugo Herbelin
2014-02-28Removing Pervasives.compare in Termdn.Pierre-Marie Pédrot
2014-02-28Removing a Pervasives.compare in Term_dnet.Pierre-Marie Pédrot
2013-09-18At least made the evar type opaque! There are still 5 remaining unsafeppedrot
2013-09-18Removing the last global evar generation in Term_dnet. The veryppedrot
2013-09-18Removing unused code from Term_dnet.ppedrot
2013-05-14Removing useless uses of Gmap.ppedrot
2012-11-22Monomorphization (pretyping)ppedrot
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-09-14As r15801: putting everything from Util.array_* to CArray.*.ppedrot
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-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-03-02Noise for nothingpboutill
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-03-11fix [Search] when the result has no hypothesis & constant comparisonpuech
2009-10-29Fix bug in dnet.ml, which missed some results when filtering one term against...puech
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-04-17- Fix handling of clauses in setoid_rewrite to rewrite under bindersmsozeau
2009-01-17DISCLAIMERpuech
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 01:25:59 +0000