aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/pattern.ml
diff options
context:
space:
mode:
authorGravatar sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-11-26 15:50:37 +0000
committerGravatar sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-11-26 15:50:37 +0000
commit2d08ea6e2563bb10170f904f6e527bdec02f2432 (patch)
tree50c32e27c519def3c67a51473cdee732d4961815 /pretyping/pattern.ml
parent6bf3d8dbccdfa4b072eb6bef1d0480a678f0817e (diff)
backtrack of the last commit (it was my fault: the code is used by
camlp4-generated code even if it is not found using grep) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6351 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/pattern.ml')
0 files changed, 0 insertions, 0 deletions