Substitution dans REvar et PEvar plutot que encodage via noeud application pour eviter la confusion avec la (vraie) application

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

5 files changed, 11 insertions, 11 deletions

diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index f453e911e..f5c3b2c03 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -34,7 +34,7 @@ let patvar_of_int_v7 n = Names.id_of_string ("?" ^ string_of_int n)
 type constr_pattern =
   | PRef of global_reference
   | PVar of identifier
-  | PEvar of existential_key
+  | PEvar of existential_key * constr_pattern array
   | PRel of int
   | PApp of constr_pattern * constr_pattern array
   | PSoApp of patvar * constr_pattern list
@@ -176,9 +176,7 @@ let rec pattern_of_constr t =
     | Const sp         -> PRef (ConstRef sp)
     | Ind sp        -> PRef (IndRef sp)
     | Construct sp -> PRef (ConstructRef sp)
-    | Evar (n,ctxt) ->
-	if ctxt = [||] then PEvar n
-	else PApp (PEvar n, Array.map pattern_of_constr ctxt)
+    | Evar (n,ctxt) -> PEvar (n,Array.map pattern_of_constr ctxt)
     | Case (ci,p,a,br) ->
 	PCase ((Some ci.ci_ind,ci.ci_pp_info.style),
 	       Some (pattern_of_constr p),pattern_of_constr a,
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index f05a08659..7a3b9127d 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -33,7 +33,7 @@ val patvar_of_int_v7 : int -> patvar
 type constr_pattern =
   | PRef of global_reference
   | PVar of identifier
-  | PEvar of existential_key
+  | PEvar of existential_key * constr_pattern array
   | PRel of int
   | PApp of constr_pattern * constr_pattern array
   | PSoApp of patvar * constr_pattern list
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index e8965659e..f8fcc9b9e 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -223,11 +223,13 @@ let rec pretype tycon env isevars lvar = function
 	(pretype_id loc env lvar id)
 	tycon
 
-  | REvar (loc, ev) ->
+  | REvar (loc, ev, instopt) ->
       (* 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 (evars_of isevars) ev).evar_hyps in
-      let args = instance_from_named_context hyps in
+      let args = match instopt with
+        | None -> instance_from_named_context hyps
+        | Some inst -> failwith "Evar subtitutions not implemented" in
       let c = mkEvar (ev, args) in
       let j = (Retyping.get_judgment_of env (evars_of isevars) c) in
       inh_conv_coerce_to_tycon loc env isevars j tycon
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index f11caa566..78425e107 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -61,7 +61,7 @@ type hole_kind =
 type rawconstr = 
   | RRef of (loc * global_reference)
   | RVar of (loc * identifier)
-  | REvar of loc * existential_key
+  | REvar of loc * existential_key * rawconstr list option
   | RPatVar of loc * (bool * patvar) (* Used for patterns only *)
   | RApp of loc * rawconstr * rawconstr list
   | RLambda of loc * name * rawconstr * rawconstr
@@ -153,7 +153,7 @@ let map_rawconstr_with_binders_loc loc g f e = function
   | RSort (_,x) -> RSort (loc,x)
   | RHole (_,x)  -> RHole (loc,x)
   | RRef (_,x) -> RRef (loc,x)
-  | REvar (_,x) -> REvar (loc,x)
+  | REvar (_,x,l) -> REvar (loc,x,l)
   | RPatVar (_,x) -> RPatVar (loc,x)
   | RDynamic (_,x) -> RDynamic (loc,x)
 *)
@@ -300,7 +300,7 @@ let rec subst_raw subst raw =
 let loc_of_rawconstr = function
   | RRef (loc,_) -> loc
   | RVar (loc,_) -> loc
-  | REvar (loc,_) -> loc
+  | REvar (loc,_,_) -> loc
   | RPatVar (loc,_) -> loc
   | RApp (loc,_,_) -> loc
   | RLambda (loc,_,_,_) -> loc
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 993b7e84a..651530c94 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -59,7 +59,7 @@ type hole_kind =
 type rawconstr = 
   | RRef of (loc * global_reference)
   | RVar of (loc * identifier)
-  | REvar of loc * existential_key
+  | REvar of loc * existential_key * rawconstr list option
   | RPatVar of loc * (bool * patvar) (* Used for patterns only *)
   | RApp of loc * rawconstr * rawconstr list
   | RLambda of loc * name * rawconstr * rawconstr