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

9 files changed, 17 insertions, 19 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 337c888a4..64aedf741 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1331,7 +1331,7 @@ let rec extern inctx scopes vars r =
 
   | RVar (loc,id) -> CRef (Ident (loc,v7_to_v8_id id))
 
-  | REvar (loc,n) -> extern_evar loc n
+  | REvar (loc,n,_) -> (* we drop args *) extern_evar loc n
 
   | RPatVar (loc,n) -> if !print_meta_as_hole then CHole loc else CPatVar (loc,n)
 
@@ -1342,7 +1342,6 @@ let rec extern inctx scopes vars r =
 	else 
 	  (f,args) in
       (match f with
-	 | REvar (loc,ev) -> extern_evar loc ev (* we drop args *)
 	 | RRef (rloc,ref) ->
 	     let subscopes = Symbols.find_arguments_scope ref in
 	     let args =
@@ -1558,7 +1557,7 @@ let extern_constr at_top env t =
 let rec raw_of_pat tenv env = function
   | PRef ref -> RRef (loc,ref)
   | PVar id -> RVar (loc,id)
-  | PEvar n -> REvar (loc,n)
+  | PEvar (n,l) -> REvar (loc,n,Some (array_map_to_list (raw_of_pat tenv env) l))
   | PRel n ->
       let id = try match lookup_name_of_rel n env with
 	| Name id   -> id
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 0f68f0314..84be73849 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -699,7 +699,7 @@ let internalise sigma env allow_soapp lvar c =
     | CPatVar (loc, _) ->
 	raise (InternalisationError (loc,NegativeMetavariable))
     | CEvar (loc, n) ->
-	REvar (loc, n)
+	REvar (loc, n, None)
     | CSort (loc, s) ->
 	RSort(loc,s)
     | CCast (loc, c1, c2) ->
diff --git a/interp/reserve.ml b/interp/reserve.ml
index dc7393c67..8b759b6aa 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -62,7 +62,7 @@ let rec unloc = function
   | RSort (_,x) -> RSort (dummy_loc,x)
   | RHole (_,x)  -> RHole (dummy_loc,x)
   | RRef (_,x) -> RRef (dummy_loc,x)
-  | REvar (_,x) -> REvar (dummy_loc,x)
+  | REvar (_,x,l) -> REvar (dummy_loc,x,l)
   | RPatVar (_,x) -> RPatVar (dummy_loc,x)
   | RDynamic (_,x) -> RDynamic (dummy_loc,x)
 
diff --git a/parsing/termast.ml b/parsing/termast.ml
index 3174898c4..0e8b84f74 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -194,7 +194,7 @@ let ast_of_app impl f args =
 let rec ast_of_raw = function
   | RRef (_,ref) -> ast_of_ref ref
   | RVar (_,id) -> ast_of_ident id
-  | REvar (_,n) -> ast_of_existential_ref n
+  | REvar (_,n,_) -> (* we drop args *) ast_of_existential_ref n
   | RPatVar (_,(_,n)) -> ope("META",[ast_of_ident n])
   | RApp (_,f,args) ->
       let (f,args) =
@@ -202,7 +202,6 @@ 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 
-	 | REvar (_,ev) -> ast_of_existential_ref ev (* we drop args *)
 	 | RRef (_,ref) -> ast_of_app (implicits_of_global ref) astf astargs
 	 | _       -> ast_of_app [] astf astargs)
 
@@ -368,7 +367,7 @@ let rec ast_of_pattern tenv env = function
 
   | PVar id -> ast_of_ident id
 
-  | PEvar n -> ast_of_existential_ref n
+  | PEvar (n,_) -> ast_of_existential_ref n
 
   | PRel n ->
       (try match lookup_name_of_rel n env with
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