diff options
| author | herbelin | 1999-12-09 23:18:20 +0000 |
|---|---|---|
| committer | herbelin | 1999-12-09 23:18:20 +0000 |
| commit | 35c127288df53b8561d13082738806fa44049a1a (patch) | |
| tree | d88d603392ae0b439d1f2b9d92ae8e472142212d | |
| parent | a4436a6a355ecb3fffb52d1ca3f2d983a5bcfefd (diff) | |
Bug affichage constructeur
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@225 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/termast.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/parsing/termast.ml b/parsing/termast.ml index 0ddee900fb..082098a46f 100644 --- a/parsing/termast.ml +++ b/parsing/termast.ml @@ -473,9 +473,10 @@ let old_bdize_depcast opcast at_top env t = let oper = if n=1 then "PROD" else "PRODLIST" in ope(oper,[bdrec [] env ty;a]) | IsLambda (na,ty,c) -> - let (_,a) = factorize_binder 1 avoid env Lambda na ty c in + let (n,a) = factorize_binder 1 avoid env Lambda na ty c in (* LAMBDA et LAMBDALIST se comportent pareil *) - ope("LAMBDALIST",[bdrec [] env ty;a]) + let oper = if n=1 then "LAMBDA" else "LAMBDALIST" in + ope(oper,[bdrec [] env ty;a]) | IsAppL (f,args) -> bdize_app f (List.map (bdrec avoid env) (f::args)) | IsConst (sp,cl) -> @@ -734,7 +735,7 @@ let rec detype t = let constructs = Array.init (Array.length mip.mind_consnames) - (fun i -> ((indsp,i),[] (* on triche *))) in + (fun i -> ((indsp,i+1),[] (* on triche *))) in let eqnv = array_map3 bdize_eqn constructs lcparams bl in let eqnl = Array.to_list eqnv in let tag = @@ -848,7 +849,7 @@ let rec ast_of_raw avoid env = function let (n,a) = factorize_binder 1 avoid env bk na t c in let tag = match bk with (* LAMBDA et LAMBDALIST se comportent pareil *) - | BLambda -> "LAMBDALIST" + | 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é ? *) |