diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/classops.mli | 2 | ||||
| -rw-r--r-- | pretyping/detyping.ml | 12 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 3 | ||||
| -rw-r--r-- | pretyping/rawterm.ml | 5 | ||||
| -rw-r--r-- | pretyping/rawterm.mli | 4 |
5 files changed, 13 insertions, 13 deletions
diff --git a/pretyping/classops.mli b/pretyping/classops.mli index 98d6fce9c..ab9410cc6 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -53,7 +53,7 @@ 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 : - rawconstr array reference -> int (* raise [Not_found] if not a coercion *) + 'a array reference -> int (* raise [Not_found] if not a coercion *) val constructor_at_head : constr -> cl_typ * int (* raises [Not_found] if not convertible to a class *) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 2dd49e4b7..a7c84dd3c 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -315,17 +315,13 @@ let rec detype avoid env t = | IsAppL (f,args) -> RApp (dummy_loc,detype avoid env f,List.map (detype avoid env) args) | IsConst (sp,cl) -> - RRef(dummy_loc,RConst(sp,Array.map (detype avoid env) cl)) + RRef(dummy_loc,RConst(sp,cl)) | IsEvar (ev,cl) -> - RRef(dummy_loc,REVar(ev,Array.map (detype avoid env) cl)) + RRef(dummy_loc,REVar(ev,cl)) | IsAbst (sp,cl) -> anomaly "bdize: Abst should no longer occur in constr" - | IsMutInd (ind_sp,cl) -> - let ctxt = Array.map (detype avoid env) cl in - RRef (dummy_loc,RInd (ind_sp,ctxt)) - | IsMutConstruct (cstr_sp,cl) -> - let ctxt = Array.map (detype avoid env) cl in - RRef (dummy_loc,RConstruct (cstr_sp,ctxt)) + | IsMutInd (ind_sp,cl) -> RRef (dummy_loc,RInd (ind_sp,cl)) + | IsMutConstruct (cstr_sp,cl) -> RRef (dummy_loc,RConstruct (cstr_sp,cl)) | IsMutCase (annot,p,c,bl) -> let synth_type = synthetize_type () in let tomatch = detype avoid env c in diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 5a1a9df46..609567771 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -144,12 +144,15 @@ let transform_rec loc env sigma cl (ct,pt) = (***********************************************************************) +(* let ctxt_of_ids ids = Array.map (function | RRef (_,RVar id) -> VAR id | _ -> error "pretyping: arbitrary subst of ref not implemented") ids +*) +let ctxt_of_ids cl = cl let mt_evd = Evd.empty diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index ab3075f45..4090e5815 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -32,8 +32,9 @@ type 'ctxt reference = | REVar of int * 'ctxt | RMeta of int +(*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 * Term.constr array reference | RApp of loc * rawconstr * rawconstr list | RBinder of loc * binder_kind * name * rawconstr * rawconstr | RCases of loc * Term.case_style * rawconstr option * rawconstr list * @@ -73,7 +74,7 @@ let loc_of_rawconstr = function | RCast (loc,_,_) -> loc type constr_pattern = - | PRef of constr_pattern array reference + | PRef of Term.constr array reference | PRel of int | PApp of constr_pattern * constr_pattern array | PSoApp of int * int list diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index f78520a16..5f67a8a92 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -32,7 +32,7 @@ type 'ctxt reference = | RMeta of int type rawconstr = - | RRef of loc * rawconstr array reference + | RRef of loc * Term.constr array reference | RApp of loc * rawconstr * rawconstr list | RBinder of loc * binder_kind * name * rawconstr * rawconstr | RCases of loc * Term.case_style * rawconstr option * rawconstr list * @@ -61,7 +61,7 @@ val dummy_loc : loc val loc_of_rawconstr : rawconstr -> loc type constr_pattern = - | PRef of constr_pattern array reference + | PRef of Term.constr array reference | PRel of int | PApp of constr_pattern * constr_pattern array | PSoApp of int * int list |