aboutsummaryrefslogtreecommitdiff
path: root/tactics/btermdn.ml
AgeCommit message (Expand)Author
2021-03-30Properly expand projection parameters in Btermdn.Pierre-Marie Pédrot
2020-10-21Rename the GlobRef comparison modules following the standard pattern.Pierre-Marie Pédrot
2020-09-18Remove unused API from Dn.Pierre-Marie Pédrot
2020-08-20Dnets now consider axioms as being opaque for pattern recognition.Pierre-Marie Pédrot
2020-07-27Do not rely on higher-order interfaces for patterns in dnets.Pierre-Marie Pédrot
2020-07-06Primitive persistent arraysMaxime Dénès
2020-06-23Correctly classify variables as being unfoldable in dnet patterns.Pierre-Marie Pédrot
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-07-11Merge PR #10498: [api] Deprecate GlobRef constructors.Gaëtan Gilbert
2019-07-08[api] Deprecate GlobRef constructors.Emilio Jesus Gallego Arias
2019-07-08[core] [api] Support OCaml 4.08Emilio Jesus Gallego Arias
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2018-11-19Rename TranspState into TransparentState.Pierre-Marie Pédrot
2018-11-19Proper record type and accessors for transparent states.Pierre-Marie Pédrot
2018-09-12Move maps & sets indexed by GlobRef.t into the kernelVincent Laporte
2018-05-30[api] Remove deprecated object from `Term`Emilio Jesus Gallego Arias
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-02-14Chasing a few unsafe constr coercions.Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-04-16Ensuring purity of datastructures in the API.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-12-12In discrimination nets, do not index lambdas if they're part of a betaMatthieu Sozeau
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
2014-07-30Fix discrimination net which was not recognizing primitive projections.Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-03Term dnets do no need to contain the afferent constr pattern in their nodes.Pierre-Marie Pédrot
2014-03-03Removing Termdn, and putting the relevant code in Btermdn. The current TermdnPierre-Marie Pédrot
2014-03-03Extruding code not depending of the functor argument in Termdn.Pierre-Marie Pédrot
2014-02-28Removing Pervasives.compare in Termdn.Pierre-Marie Pédrot
2012-12-14Modulification of identifierppedrot
2012-11-25Monomorphization (tactics)ppedrot
2012-11-08Monomorphized a lot of equalities over OCaml integers, thanks toppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-08-08Updating headers.herbelin
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-05-02Fix discrimination of sorts which doesn't play well with cumulativitymsozeau
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2009-10-28Backport fix for indexing of sorts which collapse every Type occurrencemsozeau
2009-10-21This big commit addresses two problems:soubiran
2009-09-22Better use of transparency information for local hypotheses: msozeau
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2008-07-28Fix bug in term dnet preventing some unifications. Allow "higher-order"msozeau
2008-06-27Enhanced discrimination nets implementation, which can now work withmsozeau
2004-12-07The type Pattern.constr_label was isomorphic to Libnames.global_reference.sacerdot
2004-07-16Nouvelle en-têteherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:34:49 +0000