aboutsummaryrefslogtreecommitdiff
path: root/lib/refutpat.ml4
AgeCommit message (Collapse)Author
2010-05-19Remove refutpat.ml4, ideal.ml4 is again a normal .ml, let* coded in a naive wayletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13017 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-19static (and shared) camlp4use instead of per-file declarationletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13016 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-20Use camlp4 to accept some specific non-exhaustive patterns in groebnerletouzey
The camlp4 extension "refutpat" provides a syntax let* for pattern that are non-exhaustive on purpose (e.g. let* x::l = foo in ...). A Failure is raised if the pattern doesn't match the expression. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12245 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 20:08:34 +0000