- 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

8 files changed, 42 insertions, 46 deletions

diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index 2335d3a253..9ebb8774b4 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -163,7 +163,7 @@ let make_existential loc ?(opaque = true) env isevars c =
 
 let make_existential_expr loc env c =
   let key = Evarutil.new_untyped_evar () in
-  let evar = Topconstr.CEvar (loc, key) in
+  let evar = Topconstr.CEvar (loc, key, None) in
     debug 2 (str "Constructed evar " ++ int key);
     evar
 
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index e48343858a..f2b9c996bc 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -32,6 +32,7 @@ open Genarg
 
 let _ = Constrextern.print_evar_arguments := true
 let _ = set_bool_option_value (SecondaryTable ("Printing","Matching")) false
+let _ = Detyping.set_detype_anonymous (fun _ _ -> raise Not_found)
 
 (* name printers *)
 let ppid id = pp (pr_id id)
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
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 9b257014ee..d6c711f95b 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -160,6 +160,16 @@ let pr_prim_token = function
   | Numeral n -> Bigint.pr_bigint n
   | String s -> qs s
 
+let pr_evar pr n l =
+  str (Evd.string_of_existential n) ++ 
+  (match l with
+   | Some l ->
+       pr_in_comment
+         (fun l -> 
+	   str"[" ++ hov 0 (prlist_with_sep pr_coma (pr ltop) l) ++ str"]")
+         l
+   | None -> mt())
+
 let las = lapp
 let lpator = 100
 
@@ -559,7 +569,7 @@ let rec pr sep inherited a =
       lif
      
   | CHole _ -> str "_", latom
-  | CEvar (_,n) -> str (Evd.string_of_existential n), latom
+  | CEvar (_,n,l) -> pr_evar (pr mt) n l, latom
   | CPatVar (_,(_,p)) -> str "?" ++ pr_patvar p, latom
   | CSort (_,s) -> pr_rawsort s, latom
   | CCast (_,a,CastConv (k,b)) ->
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index add975cf38..5f307cd69f 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -229,37 +229,25 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     | Anonymous -> name'
     | _ -> name
 
-  (*
-    let evar_type_case isevars env ct pt lft p c =
-    let (mind,bty,rslty) = type_case_branches env (evars_of isevars) ct pt p c
-    in check_branches_message isevars env (c,ct) (bty,lft); (mind,rslty)
-  *)
-
-  let strip_meta id = (* For Grammar v7 compatibility *)
-    let s = string_of_id id in
-      if s.[0]='$' then id_of_string (String.sub s 1 (String.length s - 1))
-      else id
-
   let pretype_id loc env (lvar,unbndltacvars) id =
-    let id = strip_meta id in (* May happen in tactics defined by Grammar *)
-      try
-	let (n,typ) = lookup_rel_id id (rel_context env) in
-	  { uj_val  = mkRel n; uj_type = lift n typ }
-      with Not_found ->
-	try
-	  List.assoc id lvar
-	with Not_found ->
-	  try
-	    let (_,_,typ) = lookup_named id env in
-	      { uj_val  = mkVar id; uj_type = typ }
-	  with Not_found ->
-	    try (* To build a nicer ltac error message *)
-	      match List.assoc id unbndltacvars with
-		| None -> user_err_loc (loc,"",
-					str "variable " ++ pr_id id ++ str " should be bound to a term")
-		| Some id0 -> Pretype_errors.error_var_not_found_loc loc id0
-	    with Not_found ->
-	      error_var_not_found_loc loc id
+    try
+      let (n,typ) = lookup_rel_id id (rel_context env) in
+      { uj_val  = mkRel n; uj_type = lift n typ }
+    with Not_found ->
+    try
+      List.assoc id lvar
+    with Not_found ->
+    try
+      let (_,_,typ) = lookup_named id env in
+      { uj_val  = mkVar id; uj_type = typ }
+    with Not_found ->
+    try (* To build a nicer ltac error message *)
+      match List.assoc id unbndltacvars with
+      | None -> user_err_loc (loc,"",
+	  str "variable " ++ pr_id id ++ str " should be bound to a term")
+      | Some id0 -> Pretype_errors.error_var_not_found_loc loc id0
+    with Not_found ->
+      error_var_not_found_loc loc id
 
   (* make a dependent predicate from an undependent one *)