diff options
author | sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-11-26 15:50:37 +0000 |
---|---|---|
committer | sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-11-26 15:50:37 +0000 |
commit | 2d08ea6e2563bb10170f904f6e527bdec02f2432 (patch) | |
tree | 50c32e27c519def3c67a51473cdee732d4961815 /pretyping/pattern.ml | |
parent | 6bf3d8dbccdfa4b072eb6bef1d0480a678f0817e (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