diff options
| -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é ? *) |