From b820ff40cb8053df01ac422f36d5f3520727b5c6 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 19 Dec 2003 18:20:53 +0000
Subject: 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
---
 pretyping/rawterm.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'pretyping/rawterm.ml')

diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index f11caa566e..78425e107a 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
-- 
cgit v1.2.3