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

10 files changed, 26 insertions, 12 deletions

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 }