diff options
| author | herbelin | 2000-10-05 19:21:17 +0000 |
|---|---|---|
| committer | herbelin | 2000-10-05 19:21:17 +0000 |
| commit | 89884470155c568b8abcdfd3986845f846c6f91a (patch) | |
| tree | f66fcd457cb0e07d0a31b2703565c69f6b68bded | |
| parent | cac2d5aa2c70f5c9e42c240502a0a6863b4d8026 (diff) | |
Bug affichage des implicites; bug de compatibilité LAMBDA/LAMBDALIST
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@658 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/termast.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/parsing/termast.ml b/parsing/termast.ml index 239dd9fc1a..91111ada39 100644 --- a/parsing/termast.ml +++ b/parsing/termast.ml @@ -155,7 +155,7 @@ let explicitize = else tail) (* Tail impl args are always printed even if implicit printing is off *) | [] -> List.rev lastimplargs - in exprec 0 [] + in exprec 1 [] let implicit_of_ref = function | RConstruct (cstrid,_) -> constructor_implicits_list cstrid @@ -219,8 +219,9 @@ let rec ast_of_raw = function | RBinder (_,bk,na,t,c) -> let (n,a) = factorize_binder 1 bk na (ast_of_raw t) c in let tag = match bk with - (* LAMBDA et LAMBDALIST se comportent pareil *) - | BLambda -> if n=1 then "LAMBDA" else "LAMBDALIST" + (* LAMBDA et LAMBDALIST se comportent pareil ... Non ! *) + (* Pour compatibilité des theories, il faut LAMBDALIST partout *) + | BLambda -> (* if n=1 then "LAMBDA" else *) "LAMBDALIST" (* PROD et PRODLIST doivent être distingués à cause du cas *) (* non dépendant, pour isoler l'implication; peut-être un *) (* constructeur ARROW serait-il plus justifié ? *) |