diff options
Diffstat (limited to 'contrib/subtac/subtac_pretyping_F.ml')
| -rw-r--r-- | contrib/subtac/subtac_pretyping_F.ml | 38 |
1 files changed, 19 insertions, 19 deletions
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml index 6244aef3..53eec0b6 100644 --- a/contrib/subtac/subtac_pretyping_F.ml +++ b/contrib/subtac/subtac_pretyping_F.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac_pretyping_F.ml 9563 2007-01-31 09:37:18Z msozeau $ *) +(* $Id: subtac_pretyping_F.ml 9976 2007-07-12 11:58:30Z msozeau $ *) open Pp open Util @@ -93,7 +93,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct (* coerce to tycon if any *) let inh_conv_coerce_to_tycon loc env isevars j = function - | None -> j + | None -> j_nf_isevar !isevars j | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to loc env) isevars j t let push_rels vars env = List.fold_right push_rel vars env @@ -364,21 +364,21 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct error_case_not_inductive_loc cloc env (evars_of !isevars) cj in let cstrs = get_constructors env indf in - if Array.length cstrs <> 1 then - user_err_loc (loc,"",str "Destructing let is only for inductive types with one constructor"); - let cs = cstrs.(0) in - if List.length nal <> cs.cs_nargs then - user_err_loc (loc,"", str "Destructing let on this type expects " ++ int cs.cs_nargs ++ str " variables"); - let fsign = List.map2 (fun na (_,c,t) -> (na,c,t)) - (List.rev nal) cs.cs_args in - let env_f = push_rels fsign env in - (* Make dependencies from arity signature impossible *) - let arsgn = - let arsgn,_ = get_arity env indf in - if not !allow_anonymous_refs then - List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn - else arsgn - in + if Array.length cstrs <> 1 then + user_err_loc (loc,"",str "Destructing let is only for inductive types with one constructor"); + let cs = cstrs.(0) in + if List.length nal <> cs.cs_nargs then + user_err_loc (loc,"", str "Destructing let on this type expects " ++ int cs.cs_nargs ++ str " variables"); + let fsign = List.map2 (fun na (_,c,t) -> (na,c,t)) + (List.rev nal) cs.cs_args in + let env_f = push_rels fsign env in + (* Make dependencies from arity signature impossible *) + let arsgn = + let arsgn,_ = get_arity env indf in + if not !allow_anonymous_refs then + List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn + else arsgn + in let psign = (na,None,build_dependent_inductive env indf)::arsgn in let nar = List.length arsgn in (match po with @@ -495,13 +495,13 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct ((fun vtyc env -> pretype vtyc env isevars lvar),isevars) tycon env (* loc *) (po,tml,eqns) - | RCast(loc,c,k,t) -> + | RCast(loc,c,k) -> let cj = match k with CastCoerce -> let cj = pretype empty_tycon env isevars lvar c in evd_comb1 (Coercion.inh_coerce_to_base loc env) isevars cj - | CastConv k -> + | CastConv (k,t) -> let tj = pretype_type empty_valcon env isevars lvar t in let cj = pretype (mk_tycon tj.utj_val) env isevars lvar c in (* User Casts are for helping pretyping, experimentally not to be kept*) |