aboutsummaryrefslogtreecommitdiff
path: root/parsing/termast.ml
diff options
context:
space:
mode:
authorherbelin2000-04-30 00:53:51 +0000
committerherbelin2000-04-30 00:53:51 +0000
commite867509591c1e8fad3fd764da652deb28d293d49 (patch)
tree020f62a4157a5b13ac8de4fcd6229f34e1971064 /parsing/termast.ml
parentde22ca2b88c8350f1f9e1e2b261c42844aea4367 (diff)
Suite intégration de constr_pattern
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@393 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/termast.ml')
-rw-r--r--parsing/termast.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/termast.ml b/parsing/termast.ml
index dda005f8bb..a044c741cb 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -766,7 +766,7 @@ let rec ast_of_pattern env = function
| PSoApp (n,args) ->
ope("SOAPP",(ope ("META",[num n]))::
- (List.map (ast_of_constr false env) args))
+ (List.map (ast_of_pattern env) args))
| PBinder (BProd,Anonymous,t,c) ->
ope("PROD",[ast_of_pattern env t; slam(None,ast_of_pattern env c)])