diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-03-20 09:18:14 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-03-20 09:18:14 +0000 |
| commit | 2618ee8c86e11d367a6640d89d4cde11a2ed5512 (patch) | |
| tree | 12497d4cc238c485aa4ce6fa463979a4698b1495 /parsing/termast.ml | |
| parent | 506743114ca8b0bc5d1957230a1ee1cf5a58c624 (diff) | |
Affichage des anonymes si lambda
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@328 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/termast.ml')
| -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 135d7f4f1..15e0b63bd 100644 --- a/parsing/termast.ml +++ b/parsing/termast.ml @@ -350,12 +350,13 @@ let next_name_not_occuring name l env t = | Anonymous -> id_of_string "_" (* Remark: Anonymous var may be dependent in Evar's contexts *) -let concrete_name l env n c = +let concrete_name islam l env n c = if n = Anonymous & not (dependent (Rel 1) c) then (None,l) else let fresh_id = next_name_not_occuring n l env c in - let idopt = if dependent (Rel 1) c then (Some fresh_id) else None in + let idopt = + if islam or dependent (Rel 1) c then (Some fresh_id) else None in (idopt, fresh_id::l) (* Returns the list of global variables and constants in a term *) @@ -477,7 +478,7 @@ let old_bdize at_top env t = let rec bdrec avoid env t = match collapse_appl t with (* Not well-formed constructions *) | DLAM(na,c) -> - (match concrete_name avoid env na c with + (match concrete_name true (*On ne sait pas si prod*)avoid env na c with | (Some id,avoid') -> slam(Some (string_of_id id), bdrec avoid' (add_rel (Name id,()) env) c) @@ -696,7 +697,7 @@ let old_bdize at_top env t = and factorize_binder n avoid env oper na ty c = let (env2, avoid2,na2) = - match concrete_name avoid env na c with + match concrete_name (oper=Lambda) avoid env na c with (Some id,l') -> add_rel (Name id,()) env, l', Some (string_of_id id) | (None,l') -> add_rel (Anonymous,()) env, l', None in |