diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-23 11:18:41 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-23 11:18:41 +0000 |
| commit | 87ab5e4f9a4f93d152df721f97a0bcb6cddef973 (patch) | |
| tree | 53f9e45dc0a5d10f180af85876f45b3cf27ba266 /pretyping/pretyping.ml | |
| parent | 090b29f754f44882a49961764e63be18f0d356c4 (diff) | |
Changement de l'afficheur pour que les variables liées aient un nom indépendant des globaux quand hors but (on garde l'évitement des globaux en but, pour compatibilité)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4458 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 145dc8720..a0fbb7724 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -759,7 +759,7 @@ let rec pretype tycon env isevars lvar = function let nconstr = Array.length mip.mind_consnames in let tyi = snd ind in if isrec && mis_is_recursive_subset [tyi] recargs then - Some (Detyping.detype env + Some (Detyping.detype (false,env) (ids_of_context env) (names_of_rel_context env) (nf_evar (evars_of isevars) v)) else |