diff options
| author | herbelin | 2007-08-29 13:09:36 +0000 |
|---|---|---|
| committer | herbelin | 2007-08-29 13:09:36 +0000 |
| commit | bfb2e68ff5587b71de525584deab04d4169d29d7 (patch) | |
| tree | 41d1ae2b6ccf0992f7347d670304d4fb8178709a /interp/constrextern.ml | |
| parent | e829fb40b1c9f599dd7ad2597b519b4283e9d460 (diff) | |
- Débogueur: positionnement de set_detype_anonymous pour ne pas
échouer sur les Rel liées a des Anonymous et export de l'instance
des evars vers le printeur du débogueur.
- Suppression d'un reste de code mort lié à la V7 dans pretyping.ml.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10102 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 15 |
1 files changed, 6 insertions, 9 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 37e47301ac..763261bfd5 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -105,13 +105,8 @@ let idopt_of_name = function | Name id -> Some id | Anonymous -> None -let extern_evar loc n = -(* - msgerrnl (str - "Warning: existential variable turned into meta-variable during externalization"); - CPatVar (loc,(false,make_ident "META" (Some n))) -*) - CEvar (loc,n) +let extern_evar loc n l = + if !print_evar_arguments then CEvar (loc,n,l) else CEvar (loc,n,None) let rawdebug = ref false @@ -662,9 +657,11 @@ let rec extern inctx scopes vars r = | REvar (loc,n,None) when !print_meta_as_hole -> CHole loc - | REvar (loc,n,_) -> (* we drop args *) extern_evar loc n + | REvar (loc,n,l) -> + extern_evar loc n (option_map (List.map (extern false scopes vars)) l) - | RPatVar (loc,n) -> if !print_meta_as_hole then CHole loc else CPatVar (loc,n) + | RPatVar (loc,n) -> + if !print_meta_as_hole then CHole loc else CPatVar (loc,n) | RApp (loc,f,args) -> (match f with |