diff options
| -rw-r--r-- | pretyping/cases.ml | 14 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 10 |
2 files changed, 10 insertions, 14 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 2b3407c27..3ef14f7e1 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -102,9 +102,6 @@ let msg_may_need_inversion () = let make_anonymous_patvars n = list_make n (PatVar (dummy_loc,Anonymous)) -(* Environment management *) -let push_rels vars env = List.fold_right push_rel vars env - (* We have x1:t1...xn:tn,xi':ti,y1..yk |- c and re-generalize over xi:ti to get x1:t1...xn:tn,xi':ti,y1..yk |- c[xi:=xi'] *) @@ -724,7 +721,8 @@ let recover_initial_subpattern_names = List.map2 set_declaration_name let recover_alias_names get_name = List.map2 (fun x (_,c,t) ->(get_name x,c,t)) let push_rels_eqn sign eqn = - {eqn with rhs = {eqn.rhs with rhs_env = push_rels sign eqn.rhs.rhs_env} } + {eqn with + rhs = {eqn.rhs with rhs_env = push_rel_context sign eqn.rhs.rhs_env} } let push_rels_eqn_with_names sign eqn = let subpats = List.rev (list_firstn (List.length sign) eqn.patterns) in @@ -1140,7 +1138,7 @@ let build_branch current realargs deps (realnames,curname) pb arsign eqns const_ let typs' = list_map_i (fun i d -> (mkRel i,map_rel_declaration (lift i) d)) 1 typs in - let extenv = push_rels typs pb.env in + let extenv = push_rel_context typs pb.env in let typs' = List.map (fun (c,d) -> @@ -1551,7 +1549,7 @@ let build_inversion_problem loc env sigma tms t = let sign = make_arity_signature env true indf' in let sign = recover_alias_names alias_of_pat (pat :: List.rev patl) sign in let p = List.length realargs in - let env' = push_rels sign env in + let env' = push_rel_context sign env in let patl',acc_sign,acc = aux (n+p+1) env' (sign@acc_sign) tms acc in patl@pat::patl',acc_sign,acc | (t, NotInd (bo,typ)) :: tms -> @@ -1575,7 +1573,7 @@ let build_inversion_problem loc env sigma tms t = let decls = list_map_i (fun i d -> (mkRel i,map_rel_declaration (lift i) d)) 1 sign in - let pb_env = push_rels sign env in + let pb_env = push_rel_context sign env in let decls = List.map (fun (c,d) -> (c,extract_inductive_data pb_env sigma d,d)) decls in @@ -1768,7 +1766,7 @@ let prepare_predicate loc typing_fun sigma env tomatchs arsign tycon pred = (* Some type annotation *) | Some rtntyp, _ -> (* We extract the signature of the arity *) - let envar = List.fold_right push_rels arsign env in + let envar = List.fold_right push_rel_context arsign env in let sigma, newt = new_sort_variable sigma in let evdref = ref sigma in let predcclj = typing_fun (mk_tycon (mkSort newt)) envar evdref rtntyp in diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 246993f1a..b1419c47b 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -261,8 +261,6 @@ module Pretyping_F (Coercion : Coercion.S) = struct | None -> j | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to loc env) evdref j t - let push_rels vars env = List.fold_right push_rel vars env - (* used to enforce a name in Lambda when the type constraints itself is named, hence possibly dependent *) @@ -532,7 +530,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct 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 + let env_f = push_rel_context fsign env in (* Make dependencies from arity signature impossible *) let arsgn = let arsgn,_ = get_arity env indf in @@ -544,7 +542,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct let nar = List.length arsgn in (match po with | Some p -> - let env_p = push_rels psign env in + let env_p = push_rel_context psign env in let pj = pretype_type empty_valcon env_p evdref lvar p in let ccl = nf_evar !evdref pj.utj_val in let psign = make_arity_signature env true indf in (* with names *) @@ -606,7 +604,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct let psign = (na,None,build_dependent_inductive env indf)::arsgn in let pred,p = match po with | Some p -> - let env_p = push_rels psign env in + let env_p = push_rel_context psign env in let pj = pretype_type empty_valcon env_p evdref lvar p in let ccl = nf_evar !evdref pj.utj_val in let pred = it_mkLambda_or_LetIn ccl psign in @@ -635,7 +633,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct | Anonymous -> (Name (id_of_string "H"), b, t)) cs.cs_args in - let env_c = push_rels csgn env in + let env_c = push_rel_context csgn env in let bj = pretype (mk_tycon pi) env_c evdref lvar b in it_mkLambda_or_LetIn bj.uj_val cs.cs_args in let b1 = f cstrs.(0) b1 in |