diff options
| -rw-r--r-- | pretyping/classops.mli | 2 | ||||
| -rw-r--r-- | pretyping/detyping.ml | 14 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 24 |
3 files changed, 24 insertions, 16 deletions
diff --git a/pretyping/classops.mli b/pretyping/classops.mli index 053e93cd4..98d6fce9c 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 : - reference -> int (* raise [Not_found] if not a coercion *) + rawconstr 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 32d08d1cd..2dd49e4b7 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -254,12 +254,14 @@ let computable p k = in striprec (k,p) +(* let ids_of_var cl = List.map (function | RRef (_,RVar id) -> id | _-> anomaly "ids_of_var") (Array.to_list cl) +*) let lookup_name_as_renamed env t s = let rec lookup avoid env n = function @@ -313,17 +315,17 @@ 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,ids_of_var (Array.map (detype avoid env) cl))) + RRef(dummy_loc,RConst(sp,Array.map (detype avoid env) cl)) | IsEvar (ev,cl) -> - RRef(dummy_loc,REVar(ev,ids_of_var (Array.map (detype avoid env) cl))) + RRef(dummy_loc,REVar(ev,Array.map (detype avoid env) cl)) | IsAbst (sp,cl) -> anomaly "bdize: Abst should no longer occur in constr" | IsMutInd (ind_sp,cl) -> - let ids = ids_of_var (Array.map (detype avoid env) cl) in - RRef (dummy_loc,RInd (ind_sp,ids)) + let ctxt = Array.map (detype avoid env) cl in + RRef (dummy_loc,RInd (ind_sp,ctxt)) | IsMutConstruct (cstr_sp,cl) -> - let ids = ids_of_var (Array.map (detype avoid env) cl) in - RRef (dummy_loc,RConstruct (cstr_sp,ids)) + let ctxt = Array.map (detype avoid env) cl in + RRef (dummy_loc,RConstruct (cstr_sp,ctxt)) | 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 e9b74bd95..5a1a9df46 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -143,8 +143,13 @@ let transform_rec loc env sigma cl (ct,pt) = mkMutCaseA ci p c lf (***********************************************************************) + let ctxt_of_ids ids = - Array.of_list (List.map (function id -> VAR id) ids) + Array.map + (function + | RRef (_,RVar id) -> VAR id + | _ -> error "pretyping: arbitrary subst of ref not implemented") + ids let mt_evd = Evd.empty @@ -230,9 +235,10 @@ let pretype_ref loc isevars env = function let metaty = try List.assoc n !trad_metamap with Not_found -> + (* Tester si la référence est castée *) user_err_loc (loc,"pretype", - [< 'sTR "Metavariable "; 'iNT n; 'sTR "remains non instanciated" >]) + [< 'sTR "Metavariable "; 'iNT n; 'sTR" is unbound" >]) in (match kind_of_term metaty with IsCast (typ,kind) -> {uj_val=DOP0 (Meta n); uj_type=typ; uj_kind=kind} @@ -244,8 +250,8 @@ let pretype_ref loc isevars env = function | RVar id -> pretype_var loc env id -| RConst (sp,ids) -> - let cst = (sp,ctxt_of_ids ids) in +| RConst (sp,ctxt) -> + let cst = (sp,ctxt_of_ids ctxt) in make_judge (mkConst cst) (type_of_constant env !isevars cst) | RAbst sp -> failwith "Pretype: abst doit disparaître" @@ -269,17 +275,17 @@ let pretype_ref loc isevars env = function pretype vtcon isevars env (abst_value cstr) else error "Cannot typecheck an unevaluable abstraction" *) -| REVar (sp,ids) -> error " Not able to type terms with dependent subgoals" +| REVar (sp,ctxt) -> error " Not able to type terms with dependent subgoals" (* Not able to type goal existential yet let cstr = mkConst (sp,ctxt_of_ids ids) in make_judge cstr (type_of_existential env !isevars cstr) *) -| RInd (ind_sp,ids) -> - let ind = (ind_sp,ctxt_of_ids ids) in +| RInd (ind_sp,ctxt) -> + let ind = (ind_sp,ctxt_of_ids ctxt) in make_judge (mkMutInd ind) (type_of_inductive env !isevars ind) -| RConstruct (cstr_sp,ids) -> - let cstr = (cstr_sp,ctxt_of_ids ids) in +| RConstruct (cstr_sp,ctxt) -> + let cstr = (cstr_sp,ctxt_of_ids ctxt) in let (typ,kind) = destCast (type_of_constructor env !isevars cstr) in {uj_val=mkMutConstruct cstr; uj_type=typ; uj_kind=kind} |