Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1340 85f007b7-540e-0410-9357-904b9bb8a0f7

22 files changed, 84 insertions, 85 deletions

diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index a653b1c04..815841673 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -726,8 +726,7 @@ let print sp fn =
         let hyps = string_list_of_named_context_list hyps in
          sp,Inductive,
           print_mutual_inductive packs [] hyps env inner_types
-    | T.ConstructRef _
-    | T.EvarRef _ ->
+    | T.ConstructRef _ ->
        Util.anomaly ("print: this should not happen")
   in
    Xml.pp pp_cmds fn ;
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 287cff598..0c51f085e 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -219,8 +219,6 @@ let sp_of_global env = function
       let mip = mind_nth_type_packet mib tyi in
       assert (i <= Array.length mip.mind_consnames && i > 0);
       make_path (dirpath sp) mip.mind_consnames.(i-1) CCI
-  | EvarRef n -> 
-      make_path [] (id_of_string ("?"^(string_of_int n))) CCI
 
 let id_of_global env ref = basename (sp_of_global env ref)
 
diff --git a/kernel/term.ml b/kernel/term.ml
index ee98a7054..7503aa03a 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -44,7 +44,6 @@ type global_reference =
   | ConstRef of constant_path
   | IndRef of inductive_path
   | ConstructRef of constructor_path
-  | EvarRef of int
 
 (********************************************************************)
 (*       Constructions as implemented                               *)
diff --git a/kernel/term.mli b/kernel/term.mli
index e3f6b4463..08b1e5e86 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -39,7 +39,6 @@ type global_reference =
   | ConstRef of constant_path
   | IndRef of inductive_path
   | ConstructRef of constructor_path
-  | EvarRef of int
 
 (********************************************************************)
 (* The type of constructions *)
@@ -79,7 +78,7 @@ type arity = rel_declaration list * sorts
 
 (* [constr array] is an instance matching definitional [named_context] in
    the same order (i.e. last argument first) *)
-type existential = int * constr array
+type existential = existential_key * constr array
 type constant = constant_path * constr array
 type constructor = constructor_path * constr array
 type inductive = inductive_path * constr array
@@ -314,8 +313,8 @@ val path_of_const : constr -> constant_path
 val args_of_const : constr -> constr array
 
 (* Destructs an existential variable *)
-val destEvar : constr -> int * constr array
-val num_of_evar : constr -> int
+val destEvar : constr -> existential_key * constr array
+val num_of_evar : constr -> existential_key
 
 (* Destructs a (co)inductive type *)
 val destMutInd : constr -> inductive
diff --git a/library/declare.ml b/library/declare.ml
index fc6a6d10b..82966022b 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -267,8 +267,7 @@ let mind_oper_of_id sp id mib =
 	   mip.mind_consnames)
     mib.mind_packets
 
-let context_of_global_reference sigma env = function
-  | EvarRef n -> (Evd.map sigma n).Evd.evar_hyps
+let context_of_global_reference env = function
   | VarRef sp -> [] (* Hum !, pas correct *)
   | ConstRef sp -> (Environ.lookup_constant sp env).const_hyps
   | IndRef (sp,_) -> (Environ.lookup_mind sp env).mind_hyps
@@ -341,7 +340,7 @@ let find_section_variable id =
     | _ -> error "Arghh, you blasted me with several variables of same name"
 
 let extract_instance ref args =
-  let hyps = context_of_global_reference Evd.empty (Global.env ()) ref in
+  let hyps = context_of_global_reference (Global.env ()) ref in
   let hyps0 = current_section_context () in
   let na = Array.length args in
   let rec peel n acc = function
@@ -352,13 +351,12 @@ let extract_instance ref args =
     | [] -> Array.of_list acc
   in peel (na-1) [] hyps
 
-let constr_of_reference sigma env ref =
-  let hyps = context_of_global_reference sigma env ref in
+let constr_of_reference _ env ref =
+  let hyps = context_of_global_reference env ref in
   let hyps0 = current_section_context () in
   let env0 = Environ.reset_context env in
   let args = instance_from_named_context hyps in
   let body = match ref with
-    | EvarRef n -> mkEvar (n,Array.of_list args)
     | VarRef sp -> mkVar (basename sp)
     | ConstRef sp -> mkConst (sp,Array.of_list args)
     | ConstructRef sp -> mkMutConstruct (sp,Array.of_list args)
@@ -390,7 +388,6 @@ let global_reference kind id =
   construct_reference (Global.env()) kind id
 
 let dirpath_of_global = function
-  | EvarRef n -> ["evar"]
   | VarRef sp -> dirpath sp
   | ConstRef sp -> dirpath sp
   | IndRef (sp,_) -> dirpath sp
diff --git a/library/impargs.ml b/library/impargs.ml
index 2644944ac..8dc025e59 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -254,7 +254,6 @@ let declare_implicits = function
       let mib_imps = compute_mib_implicits sp in
       let imps = (snd mib_imps.(i)).(j-1) in
       add_anonymous_leaf (in_constructor_implicits (consp, imps))
-  | EvarRef _ -> assert false
 
 let declare_manual_implicits r l = match r with
   | VarRef sp -> 
@@ -265,8 +264,6 @@ let declare_manual_implicits r l = match r with
       add_anonymous_leaf (in_inductive_implicits (indp,Impl_manual l))
   | ConstructRef consp -> 
       add_anonymous_leaf (in_constructor_implicits (consp,Impl_manual l))
-  | EvarRef _ -> 
-      assert false
 
 (*s Tests if declared implicit *)
 
@@ -285,7 +282,6 @@ let implicits_of_global = function
   | ConstRef sp -> list_of_implicits (constant_implicits sp)
   | IndRef isp -> list_of_implicits (inductive_implicits isp)
   | ConstructRef csp ->	list_of_implicits (constructor_implicits csp)
-  | EvarRef _ -> []
 
 (*s Registration as global tables and rollback. *)
 
diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 6f2385392..d96107755 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -179,15 +179,14 @@ let ast_to_global loc c =
     | ("CONST", [sp]) ->
 	let ref = ConstRef (ast_to_sp sp) in
 	RRef (loc, ref), implicits_of_global ref
-    | ("EVAR", [(Num (_,ev))]) ->
-	let ref = EvarRef ev in
-	RRef (loc, ref), implicits_of_global ref
     | ("MUTIND", [sp;Num(_,tyi)]) -> 
 	let ref = IndRef (ast_to_sp sp, tyi) in
 	RRef (loc, ref), implicits_of_global ref
     | ("MUTCONSTRUCT", [sp;Num(_,ti);Num(_,n)]) ->
 	let ref = ConstructRef ((ast_to_sp sp,ti),n) in
 	RRef (loc, ref), implicits_of_global ref
+    | ("EVAR", [(Num (_,ev))]) ->
+	REvar (loc, ev), []
     | ("SYNCONST", [sp]) ->
 	Syntax_def.search_syntactic_definition (ast_to_sp sp), []
     | _ -> anomaly_loc (loc,"ast_to_global",
diff --git a/parsing/g_natsyntax.ml b/parsing/g_natsyntax.ml
index ca5033a20..41f6f1818 100644
--- a/parsing/g_natsyntax.ml
+++ b/parsing/g_natsyntax.ml
@@ -15,9 +15,9 @@ open Termast
 
 exception Non_closed_number
 
-let ast_O = ast_of_ref ast_of_rawconstr glob_O
-let ast_S = ast_of_ref ast_of_rawconstr glob_S
-let ast_myvar = ast_of_ref ast_of_rawconstr glob_My_special_variable_nat
+let ast_O = ast_of_ref glob_O
+let ast_S = ast_of_ref glob_S
+let ast_myvar = ast_of_ref glob_My_special_variable_nat
   
 (* For example, (nat_of_string "3") is <<(S (S (S O)))>> *)
 let nat_of_int n dloc =
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index eb6b20719..2577ef9be 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -329,7 +329,6 @@ let print_name qid =
       | IndRef (sp,_) -> print_inductive sp
       | ConstructRef ((sp,_),_) -> print_inductive sp
       | VarRef sp -> print_section_variable sp
-      | EvarRef n -> [< 'sTR "?"; 'iNT n; 'fNL >]
   with Not_found -> 
   try  (* Var locale de but, pas var de section... donc pas d'implicits *)
     let dir,str = repr_qualid qid in 
diff --git a/parsing/termast.ml b/parsing/termast.ml
index 3d72f4adc..0a7a73966 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -74,35 +74,23 @@ let stringopt_of_name = function
   | Name id -> Some (string_of_id id)
   | Anonymous -> None
 
-let ast_of_constant_ref pr (sp,ids) =
-  let a = ope("CONST", [path_section dummy_loc sp]) in
-  if !print_arguments then ope("INSTANCE",a::(array_map_to_list pr ids))
-  else a
+let ast_of_constant_ref sp =
+  ope("CONST", [path_section dummy_loc sp])
 
-let ast_of_existential_ref pr  (ev,ids) =
-  let a = ope("EVAR", [num ev]) in
-  if !print_arguments or !print_evar_arguments then
-    ope("INSTANCE",a::(array_map_to_list pr ids))
-  else a
+let ast_of_existential_ref ev =
+  ope("EVAR", [num ev])
 
-let ast_of_constructor_ref pr  (((sp,tyi),n) as cstr_sp,ids) =
-  let a = ope("MUTCONSTRUCT",[path_section dummy_loc sp; num tyi; num n]) in
-  if !print_arguments then ope("INSTANCE",a::(array_map_to_list pr ids))
-  else a
+let ast_of_constructor_ref ((sp,tyi),n) =
+  ope("MUTCONSTRUCT",[path_section dummy_loc sp; num tyi; num n])
 
-let ast_of_inductive_ref pr  ((sp,tyi) as ind_sp,ids) =
-  let a = ope("MUTIND",	[path_section dummy_loc sp; num tyi]) in
-  if !print_arguments then ope("INSTANCE",a::(array_map_to_list pr ids))
-  else a
+let ast_of_inductive_ref (sp,tyi) =
+  ope("MUTIND", [path_section dummy_loc sp; num tyi])
 
-let ast_of_ref pr r =
-  (* TODO gérer le ctxt *)
-  let ctxt = [||] in match r with
-  | ConstRef sp -> ast_of_constant_ref pr (sp,ctxt)
-  | IndRef sp -> ast_of_inductive_ref pr (sp,ctxt)
-  | ConstructRef sp -> ast_of_constructor_ref pr (sp,ctxt)
+let ast_of_ref = function
+  | ConstRef sp -> ast_of_constant_ref sp
+  | IndRef sp -> ast_of_inductive_ref sp
+  | ConstructRef sp -> ast_of_constructor_ref sp
   | VarRef sp -> ast_of_ident (basename sp)
-  | EvarRef ev -> ast_of_existential_ref pr (ev,ctxt)
 
 let ast_of_qualid p =
   let dir, s = repr_qualid p in
@@ -112,21 +100,18 @@ let ast_of_qualid p =
 (**********************************************************************)
 (* conversion of patterns                                             *)
 
-let adapt (cstr_sp,ctxt) = (cstr_sp,Array.of_list ctxt)
-
 let rec ast_of_cases_pattern = function   (* loc is thrown away for printing *)
   | PatVar (loc,Name id) -> nvar (string_of_id id)
   | PatVar (loc,Anonymous) -> nvar "_"
-  | PatCstr(loc,cstr,args,Name id) ->
+  | PatCstr(loc,(cstrsp,_),args,Name id) ->
       let args = List.map ast_of_cases_pattern args in
       ope("PATTAS",
 	  [nvar (string_of_id id);
-	   ope("PATTCONSTRUCT",
-	       (ast_of_constructor_ref ast_of_ident (adapt cstr))::args)])
-  | PatCstr(loc,cstr,args,Anonymous) ->
+	   ope("PATTCONSTRUCT", (ast_of_constructor_ref cstrsp)::args)])
+  | PatCstr(loc,(cstrsp,_),args,Anonymous) ->
       ope("PATTCONSTRUCT",
-	  (ast_of_constructor_ref ast_of_ident (adapt cstr))::
-	  List.map ast_of_cases_pattern args)
+	  (ast_of_constructor_ref cstrsp)
+	  :: List.map ast_of_cases_pattern args)
 	
 let ast_dependent na aty =
   match na with
@@ -188,8 +173,9 @@ let ast_of_app impl f args =
 *)
 
 let rec ast_of_raw = function
-  | RRef (_,ref) -> ast_of_ref ast_of_raw ref
+  | RRef (_,ref) -> ast_of_ref ref
   | RVar (_,id) -> ast_of_ident id
+  | REvar (_,n) -> ast_of_existential_ref n
   | RMeta (_,n) -> ope("META",[num n])
   | RApp (_,f,args) ->
       let (f,args) =
@@ -197,8 +183,7 @@ let rec ast_of_raw = function
       let astf = ast_of_raw f in
       let astargs = List.map ast_of_raw args in
       (match f with 
-	 | RRef (_,(EvarRef _ as ref)) ->
-	     ast_of_ref ast_of_raw ref (* we drop args *)
+	 | REvar (_,ev) -> ast_of_existential_ref ev (* we drop args *)
 	 | RRef (_,ref) -> ast_of_app (implicits_of_global ref) astf astargs
 
 	 | RVar (_,id) ->
@@ -317,19 +302,37 @@ let ast_of_constr at_top env t =
   ast_of_raw 
     (Detyping.detype avoid (names_of_rel_context env) t')
 
-let ast_of_constant env    = ast_of_constant_ref (ast_of_constr false env)
+let ast_of_constant env (sp,ids) =
+  let a = ast_of_constant_ref sp in
+  if !print_arguments then
+    ope("INSTANCE",a::(array_map_to_list (ast_of_constr false env) ids))
+  else a
 
-let ast_of_existential env = ast_of_existential_ref (ast_of_constr false env)
+let ast_of_existential env (ev,ids) =
+  let a = ast_of_existential_ref ev in
+  if !print_arguments or !print_evar_arguments then
+    ope("INSTANCE",a::(array_map_to_list (ast_of_constr false env) ids))
+  else a
 
-let ast_of_inductive env   = ast_of_inductive_ref (ast_of_constr false env)
+let ast_of_constructor env (cstr_sp,ids) =
+  let a = ast_of_constructor_ref cstr_sp in
+  if !print_arguments then
+    ope("INSTANCE",a::(array_map_to_list (ast_of_constr false env) ids))
+  else a
 
-let ast_of_constructor env = ast_of_constructor_ref (ast_of_constr false env)
+let ast_of_inductive env (ind_sp,ids) =
+  let a = ast_of_inductive_ref ind_sp in
+  if !print_arguments then
+    ope("INSTANCE",a::(array_map_to_list (ast_of_constr false env) ids))
+  else a
 
 let rec ast_of_pattern env = function
-  | PRef ref -> ast_of_ref (fun c -> ast_of_raw (Detyping.detype [] env c)) ref
+  | PRef ref -> ast_of_ref ref
 
   | PVar id -> ast_of_ident id
 
+  | PEvar n -> ast_of_existential_ref n
+
   | PRel n ->
       (try match lookup_name_of_rel n env with
 	 | Name id   -> ast_of_ident id
diff --git a/parsing/termast.mli b/parsing/termast.mli
index 4b689ead0..1d6ee2208 100644
--- a/parsing/termast.mli
+++ b/parsing/termast.mli
@@ -26,7 +26,7 @@ val ast_of_constant     : env -> constant -> Coqast.t
 val ast_of_existential  : env -> existential -> Coqast.t
 val ast_of_constructor  : env -> constructor -> Coqast.t
 val ast_of_inductive    : env -> inductive -> Coqast.t
-val ast_of_ref          : ('a -> Coqast.t) -> global_reference -> Coqast.t
+val ast_of_ref          : global_reference -> Coqast.t
 val ast_of_qualid       : qualid -> Coqast.t
 
 (* For debugging *)
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 19a3950b7..da66f63a4 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -348,7 +348,7 @@ let occur_rawconstr id =
 	(array_exists occur tyl) or
 	(not (array_exists (fun id2 -> id=id2) idl) & array_exists occur bv)
     | RCast (loc,c,t) -> (occur c) or (occur t)
-    | (RSort _ | RHole _ | RRef _ | RMeta _) -> false
+    | (RSort _ | RHole _ | RRef _ | REvar _ | RMeta _) -> false
 
   and occur_pattern (idl,p,c) = not (List.mem id idl) & (occur c)
 
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 0b190db0e..ca8553525 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -134,9 +134,7 @@ let coercion_exists coe =
   try let _ = coercion_info coe in true
   with Not_found -> false
 
-let coe_of_reference = function
-  | EvarRef _ -> raise Not_found
-  | x -> x
+let coe_of_reference x = x
 
 let hide_coercion coe =
   let _,coe_info = coercion_info coe in
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 352d1297a..2e7e804aa 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -298,7 +298,7 @@ let rec detype avoid env t =
     | IsConst (sp,cl) ->
 	detype_reference avoid env (ConstRef sp) cl
     | IsEvar (ev,cl) ->
-	let f = RRef (dummy_loc, EvarRef ev) in
+	let f = REvar (dummy_loc, ev) in
 	RApp (dummy_loc, f, List.map (detype avoid env) (Array.to_list cl))
     | IsMutInd (ind_sp,cl) ->
 	detype_reference avoid env (IndRef ind_sp) cl
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index d1566419c..513e47ea0 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -11,6 +11,7 @@ open Environ
 type constr_pattern =
   | PRef of global_reference
   | PVar of identifier
+  | PEvar of existential_key
   | PRel of int
   | PApp of constr_pattern * constr_pattern array
   | PSoApp of int * constr_pattern list
@@ -31,7 +32,7 @@ let rec occur_meta_pattern = function
       (occur_meta_pattern p) or
       (occur_meta_pattern c) or (array_exists occur_meta_pattern br)
   | PMeta _ | PSoApp _ -> true
-  | PVar _ | PRef _ | PRel _ | PSort _ | PFix _ | PCoFix _ -> false
+  | PEvar _ | PVar _ | PRef _ | PRel _ | PSort _ | PFix _ | PCoFix _ -> false
 
 type constr_label =
   | ConstNode of section_path
@@ -50,7 +51,6 @@ let label_of_ref = function
   | IndRef sp       -> IndNode sp
   | ConstructRef sp -> CstrNode sp
   | VarRef sp       -> SectionVarNode sp
-  | EvarRef n          -> raise BoundPattern
 
 let rec head_pattern_bound t =
   match t with
@@ -59,7 +59,8 @@ let rec head_pattern_bound t =
     | PCase (p,c,br)        -> head_pattern_bound c
     | PRef r                -> label_of_ref r
     | PVar id               -> VarNode id
-    | PRel _ | PMeta _ | PSoApp _  | PSort _ | PFix _ -> raise BoundPattern
+    | PEvar _ | PRel _ | PMeta _ | PSoApp _  | PSort _ | PFix _
+	-> raise BoundPattern
     (* Perhaps they were arguments, but we don't beta-reduce *)
     | PBinder(BLambda,_,_,_) -> raise BoundPattern
     | PCoFix _ -> anomaly "head_pattern_bound: not a type"
@@ -313,7 +314,8 @@ let rec pattern_of_constr t =
     | IsMutConstruct (sp,ctxt) ->
 	pattern_of_ref (ConstructRef sp) ctxt
     | IsEvar (n,ctxt) ->
-	pattern_of_ref (EvarRef n) ctxt
+	if ctxt = [||] then PEvar n
+	else PApp (PEvar n, Array.map pattern_of_constr ctxt)
     | IsMutCase (ci,p,a,br) ->
 	PCase (Some (pattern_of_constr p),pattern_of_constr a,
 	       Array.map pattern_of_constr br)
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index d69b5e724..115e86d61 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -11,6 +11,7 @@ open Environ
 type constr_pattern =
   | PRef of global_reference
   | PVar of identifier
+  | PEvar of existential_key
   | PRel of int
   | PApp of constr_pattern * constr_pattern array
   | PSoApp of int * constr_pattern list
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index fe628d2eb..6ef3ad8e5 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -215,6 +215,15 @@ let rec pretype tycon env isevars lvar lmeta = function
 	(pretype_id loc env lvar id)
 	tycon
 
+  | REvar (loc, ev) ->
+      (* Ne faudrait-il pas s'assurer que hyps est bien un
+      sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *)
+      let hyps = (Evd.map !isevars ev).evar_hyps in
+      let args = instance_from_named_context hyps in
+      let c = mkEvar (ev, Array.of_list args) in
+      let j = (Retyping.get_judgment_of env !isevars c) in
+      inh_conv_coerce_to_tycon loc env isevars j tycon
+
   | RMeta (loc,n) ->
       let j =
 	try
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 3329e62c3..99e32c76d 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -34,6 +34,7 @@ type 'ctxt reference =
 type rawconstr = 
   | RRef of loc * global_reference
   | RVar of loc * identifier
+  | REvar of loc * existential_key
   | RMeta of loc * int
   | RApp of loc * rawconstr * rawconstr list
   | RBinder of loc * binder_kind * name * rawconstr * rawconstr
@@ -64,6 +65,7 @@ let dummy_loc = (0,0)
 let loc_of_rawconstr = function
   | RRef (loc,_) -> loc
   | RVar (loc,_) -> loc
+  | REvar (loc,_) -> loc
   | RMeta (loc,_) -> loc
   | RApp (loc,_,_) -> loc
   | RBinder (loc,_,_,_,_) -> loc
@@ -78,6 +80,7 @@ let loc_of_rawconstr = function
 let set_loc_of_rawconstr loc = function
   | RRef (_,a)      -> RRef (loc,a)
   | RVar (_,a)      -> RVar (loc,a)
+  | REvar (_,a)      -> REvar (loc,a)
   | RMeta (_,a)     -> RMeta (loc,a) 
   | RApp (_,a,b)    -> RApp (loc,a,b)
   | RBinder (_,a,b,c,d) -> RBinder (loc,a,b,c,d)
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 9b8ed0a01..1bb4c13a9 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -32,6 +32,7 @@ type 'ctxt reference =
 type rawconstr = 
   | RRef of loc * global_reference
   | RVar of loc * identifier
+  | REvar of loc * existential_key
   | RMeta of loc * int
   | RApp of loc * rawconstr * rawconstr list
   | RBinder of loc * binder_kind * name * rawconstr * rawconstr
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 270742601..ee8c1f764 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -49,7 +49,7 @@ let rec type_of env cstr=
        with Not_found ->
          anomaly ("type_of: variable "^(string_of_id id)^" unbound"))
     | IsConst c -> body_of_type (type_of_constant env sigma c)
-    | IsEvar _ -> type_of_existential env sigma cstr
+    | IsEvar ev -> type_of_existential env sigma ev
     | IsMutInd ind -> body_of_type (type_of_inductive env sigma ind)
     | IsMutConstruct cstr -> body_of_type (type_of_constructor env sigma cstr)
     | IsMutCase (_,p,c,lf) ->
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 8279fb7e8..d3f7eb0ed 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -24,8 +24,8 @@ let rec execute mf env sigma cstr =
     | IsMeta n ->
 	error "execute: found a non-instanciated goal"
 
-    | IsEvar _ ->
-	let ty = type_of_existential env sigma cstr in
+    | IsEvar ev ->
+	let ty = type_of_existential env sigma ev in
 	let jty = execute mf env sigma ty in
 	let jty = assumption_of_judgment env sigma jty in
 	{ uj_val = cstr; uj_type = jty }
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 022c75cb6..e0ae40af6 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -60,7 +60,6 @@ let stre_of_coe = function
   | ConstRef sp -> constant_or_parameter_strength sp
   | VarRef sp -> variable_strength sp
   | IndRef _ | ConstructRef _ -> NeverDischarge 
-  | EvarRef _ -> anomaly "Not a persistent reference"
 
 (* verfications pour l'ajout d'une classe *)
 
@@ -197,9 +196,7 @@ let class_of_ref = function
       errorlabstrm "class_of_ref"
 	[< 'sTR "Constructors, such as "; Printer.pr_global c; 
 	   'sTR " cannot be used as class" >]
-  | EvarRef _ -> 
-      errorlabstrm "class_of_ref"
-	[< 'sTR "Existential variables cannot be used as class" >]
+
 (* 
 lp est la liste (inverse'e) des arguments de la coercion
 ids est le nom de la classe source
@@ -479,4 +476,3 @@ let process_coercion sec_sp (((coe,coeinfo),s,t) as x) =
           (((ConstructRef ((newsp,i),j)),coeinfo),s1,t1)
 	else
 	  ((coe,coeinfo),s1,t1)
-    | EvarRef _ -> anomaly "No Evar expected here as coercion"