diff options
author | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-02 22:30:42 +0000 |
---|---|---|
committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-02 22:30:42 +0000 |
commit | c2dda7cf57f29e5746e5903c310a7ce88525909c (patch) | |
tree | aa60a6f57014c20f980e90230b122cc76ba21e9b /pretyping/glob_term.ml | |
parent | 401f17afa2e9cc3f2d734aef0d71a2c363838ebd (diff) |
"Let in" in pattern hell, one more iteration
This reverts commit 28bcf05dd876beea8697f6ee47ebf916a8b94cdf.
An other wrong externalize function
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15021 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/glob_term.ml')
0 files changed, 0 insertions, 0 deletions