diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-06-21 17:40:14 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-06-21 17:40:14 +0000 |
| commit | 918bb3ed96f87a6046a8b759af9124d8a806bc51 (patch) | |
| tree | 2853d49ae374184ea45ecfd2ab447b571e6b44ba /parsing | |
| parent | 889dcd22b3110279525af9fcb07d5de651c685d4 (diff) | |
$BINDER -> BINDER
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@517 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/pcoq.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index f0b13f23e..f9cd0839f 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -138,7 +138,7 @@ let slam_ast (_,fin) id ast = let abstract_binder_ast (_,fin as loc) name a b = match a with | Coqast.Node((deb,_),s,d::l) -> - let s' = if s="$BINDER" then name else s in + let s' = if s="BINDER" then name else s in Coqast.Node((deb,fin),s', [d; List.fold_right (slam_ast loc) l b]) | _ -> invalid_arg "Bad usage of $ABSTRACT macro" |