diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-12-05 18:36:46 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-12-05 18:36:46 +0000 |
| commit | 6d34b4c933fc4144b5c6503b563ba329fbdd89d0 (patch) | |
| tree | 2dacc8cfe47dc17262d7960b946111988e07cddd /parsing/termast.ml | |
| parent | a324a5301e0b6f3e47c38fa2764c2d270843e440 (diff) | |
mise au point lexer / debugage PP
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@205 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/termast.ml')
| -rw-r--r-- | parsing/termast.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/parsing/termast.ml b/parsing/termast.ml index d26363ca3..cdaa2a268 100644 --- a/parsing/termast.ml +++ b/parsing/termast.ml @@ -852,7 +852,7 @@ let rec ast_of_raw avoid env = function (* 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é ? *) - | BProd -> if n=1 then "PROD" else "PROLIST" + | BProd -> if n=1 then "PROD" else "PRODLIST" in ope(tag,[ast_of_raw [] env t;a]) @@ -963,7 +963,7 @@ and weak_concrete_name avoid env na c = | Anonymous -> (None,avoid) | Name id -> (Some id,avoid) -let bdize_no_casts at_top env t = +let bdize at_top env t = try let avoid = if at_top then ids_of_env env else [] in ast_of_raw avoid env (detype t) @@ -984,6 +984,6 @@ let rec strong whdfun t = | VAR _ as t -> t | Rel _ as t -> t -let bdize at_top env t = bdize_no_casts at_top env (strong strip_outer_cast t) +let bdize_no_casts at_top env t = bdize at_top env (strong strip_outer_cast t) let ast_of_rawconstr = ast_of_raw [] |