- 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

4 files changed, 11 insertions, 14 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
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 74ea5aef6a..77ffe3c210 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -920,8 +920,8 @@ let internalise sigma globalenv env allow_patvar lvar c =
 	RPatVar (loc, n)
     | CPatVar (loc, _) ->
 	raise (InternalisationError (loc,NegativeMetavariable))
-    | CEvar (loc, n) ->
-	REvar (loc, n, None)
+    | CEvar (loc, n, l) ->
+	REvar (loc, n, option_map (List.map (intern env)) l)
     | CSort (loc, s) ->
 	RSort(loc,s)
     | CCast (loc, c1, CastConv (k, c2)) ->
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 0c5e6dbaed..a44f0b6b43 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -565,7 +565,7 @@ type constr_expr =
       * constr_expr * constr_expr
   | CHole of loc
   | CPatVar of loc * (bool * patvar)
-  | CEvar of loc * existential_key
+  | CEvar of loc * existential_key * constr_expr list option
   | CSort of loc * rawsort
   | CCast of loc * constr_expr * constr_expr cast_type
   | CNotation of loc * notation * constr_expr list
@@ -627,7 +627,7 @@ let constr_loc = function
   | CIf (loc,_,_,_,_) -> loc
   | CHole loc -> loc
   | CPatVar (loc,_) -> loc
-  | CEvar (loc,_) -> loc
+  | CEvar (loc,_,_) -> loc
   | CSort (loc,_) -> loc
   | CCast (loc,_,_) -> loc
   | CNotation (loc,_,_) -> loc
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 75dbb7cf2b..3d928bbb4a 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -125,7 +125,7 @@ type constr_expr =
       * constr_expr * constr_expr
   | CHole of loc
   | CPatVar of loc * (bool * patvar)
-  | CEvar of loc * existential_key
+  | CEvar of loc * existential_key * constr_expr list option
   | CSort of loc * rawsort
   | CCast of loc * constr_expr * constr_expr cast_type
   | CNotation of loc * notation * constr_expr list