Utilisation de global_reference dans rawconstr

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

5 files changed, 17 insertions, 10 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 84041fb329..d68d8ec742 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -330,7 +330,7 @@ let check_number_of_regular_eqns eqns =
 (* Functions to deal with matrix factorization *)
 let occur_rawconstr id =
   let rec occur = function
-    | RRef (loc,RVar id) -> true
+    | RVar (loc,id') -> id = id'
     | RApp (loc,f,args) -> (occur f) or (List.exists occur args)
     | RBinder (loc,bk,na,ty,c) -> (occur ty) or ((na <> Name id) & (occur c))
     | RCases (loc,prinfo,tyopt,tml,pl) ->
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 306f2b8ce2..a452cf645e 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -137,11 +137,11 @@ let coercion_exists coe =
   with Not_found -> false
 
 let coe_of_reference = function
-  | RConst (sp,l) -> NAM_Constant sp
-  | RInd (ind_sp,l) -> NAM_Inductive ind_sp
-  | RConstruct (cstr_sp,l) -> NAM_Constructor cstr_sp
-  | RVar id  -> NAM_Var id
-  | _ -> raise Not_found
+  | ConstRef sp -> NAM_Constant sp
+  | IndRef sp -> NAM_Inductive sp
+  | ConstructRef sp -> NAM_Constructor sp
+  | VarRef sp  -> NAM_Var (basename sp)
+  | EvarRef _ -> raise Not_found
 
 let coercion_params r =
   let _,coe_info = coercion_info (coe_of_reference r) in
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index ab9410cc64..342161cb44 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -52,8 +52,10 @@ val class_info_from_index : int -> cl_typ * cl_info_typ
 val coercion_exists : coe_typ -> bool
 val coercion_info : coe_typ -> (int * coe_info_typ)
 val coercion_info_from_index : int -> coe_typ * coe_info_typ
-val coercion_params : 
-  'a array reference -> int (* raise [Not_found] if not a coercion *)
+
+(* [coercion_params] raises [Not_found] if not a coercion *)
+val coercion_params : global_reference -> int
+
 val constructor_at_head : constr -> cl_typ * int
 
 (* raises [Not_found] if not convertible to a class *)
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index f1a28f63b7..7e933a2131 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -32,7 +32,8 @@ type 'ctxt reference =
 
 (*i Pas beau ce constr dans rawconstr, mais mal compris ce ctxt des ref i*)
 type rawconstr = 
-  | RRef of loc * rawconstr array reference
+  | RRef of loc * global_reference
+  | RVar of loc * identifier
   | RMeta of loc * int
   | RApp of loc * rawconstr * rawconstr list
   | RBinder of loc * binder_kind * name * rawconstr * rawconstr
@@ -62,6 +63,7 @@ let dummy_loc = (0,0)
 
 let loc_of_rawconstr = function
   | RRef (loc,_) -> loc
+  | RVar (loc,_) -> loc
   | RMeta (loc,_) -> loc
   | RApp (loc,_,_) -> loc
   | RBinder (loc,_,_,_,_) -> loc
@@ -76,3 +78,5 @@ let loc_of_rawconstr = function
 let join_loc (deb1,_) (_,fin2) = (deb1,fin2)
 
 
+
+
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 58ebbf353d..b0f6615b96 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -30,7 +30,8 @@ type 'ctxt reference =
   | REVar of int * 'ctxt
 
 type rawconstr = 
-  | RRef of loc * rawconstr array reference
+  | RRef of loc * global_reference
+  | RVar of loc * identifier
   | RMeta of loc * int
   | RApp of loc * rawconstr * rawconstr list
   | RBinder of loc * binder_kind * name * rawconstr * rawconstr