diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 4 | ||||
| -rw-r--r-- | pretyping/evarsolve.ml | 6 | ||||
| -rw-r--r-- | pretyping/inductiveops.ml | 6 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 16 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 2 | ||||
| -rw-r--r-- | pretyping/tacred.ml | 10 | ||||
| -rw-r--r-- | pretyping/unification.ml | 5 |
7 files changed, 26 insertions, 23 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 55c1f41c2c..afe776dced 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -73,11 +73,11 @@ let error_wrong_numarg_inductive ?loc env c n = let list_try_compile f l = let rec aux errors = function - | [] -> if errors = [] then anomaly (str "try_find_f.") else iraise (List.last errors) + | [] -> if errors = [] then anomaly (str "try_find_f.") else Exninfo.iraise (List.last errors) | h::t -> try f h with UserError _ | TypeError _ | PretypeError _ | PatternMatchingError _ as e -> - let e = CErrors.push e in + let e = Exninfo.capture e in aux (e::errors) t in aux [] l diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index aafd662f7d..c9ccd668ca 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -78,9 +78,9 @@ let get_polymorphic_positions env sigma f = match EConstr.kind sigma f with | Ind (ind, u) | Construct ((ind, _), u) -> let mib,oib = Inductive.lookup_mind_specif env ind in - (match oib.mind_arity with - | RegularArity _ -> assert false - | TemplateArity templ -> templ.template_param_levels) + (match mib.mind_template with + | None -> assert false + | Some templ -> templ.template_param_levels) | _ -> assert false let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index a4406aeba1..01994a35c7 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -681,13 +681,17 @@ let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty = match mip.mind_arity with | RegularArity s -> sigma, EConstr.of_constr (subst_instance_constr u s.mind_user_arity) | TemplateArity ar -> + let templ = match mib.mind_template with + | None -> assert false + | Some t -> t + in let _,scl = splay_arity env sigma conclty in let scl = EConstr.ESorts.kind sigma scl in let ctx = List.rev mip.mind_arity_ctxt in let evdref = ref sigma in let ctx = instantiate_universes - env evdref scl ar.template_level (ctx,ar.template_param_levels) in + env evdref scl ar.template_level (ctx,templ.template_param_levels) in !evdref, EConstr.of_constr (mkArity (List.rev ctx,scl)) let type_of_projection_constant env (p,u) = diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index ac1a4e88ef..1269488af3 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -87,9 +87,9 @@ let search_guard ?loc env possible_indexes fixdefs = let fix = ((indexes, 0),fixdefs) in (try check_fix env fix with reraise -> - let (e, info) = CErrors.push reraise in + let (e, info) = Exninfo.capture reraise in let info = Option.cata (fun loc -> Loc.add_loc info loc) info loc in - iraise (e, info)); + Exninfo.iraise (e, info)); indexes else (* we now search recursively among all combinations *) @@ -266,8 +266,8 @@ let apply_heuristics env sigma fail_evar = let flags = default_flags_of (Typeclasses.classes_transparent_state ()) in try solve_unif_constraints_with_heuristics ~flags env sigma with e when CErrors.noncritical e -> - let e = CErrors.push e in - if fail_evar then iraise e else sigma + let e = Exninfo.capture e in + if fail_evar then Exninfo.iraise e else sigma let check_typeclasses_instances_are_solved ~program_mode env current_sigma frozen = (* Naive way, call resolution again with failure flag *) @@ -753,9 +753,9 @@ struct let cofix = (i, fixdecls) in (try check_cofix !!env (i, nf_fix sigma fixdecls) with reraise -> - let (e, info) = CErrors.push reraise in + let (e, info) = Exninfo.capture reraise in let info = Option.cata (Loc.add_loc info) info loc in - iraise (e, info)); + Exninfo.iraise (e, info)); make_judge (mkCoFix cofix) ftys.(i) in discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma fixj tycon @@ -946,9 +946,9 @@ struct try judge_of_product !!env name j j' with TypeError _ as e -> - let (e, info) = CErrors.push e in + let (e, info) = Exninfo.capture e in let info = Option.cata (Loc.add_loc info) info loc in - iraise (e, info) in + Exninfo.iraise (e, info) in discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon let pretype_letin self (name, c1, t, c2) = diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 98eb33273f..b07ae8788a 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1465,7 +1465,7 @@ let report_anomaly (e, info) = UserError (None, msg) else e in - iraise (e, info) + Exninfo.iraise (e, info) let f_conv ?l2r ?reds env ?evars x y = let inj = EConstr.Unsafe.to_constr in diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 4afed07eda..fdf0db9909 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1009,11 +1009,11 @@ let change_map_constr_with_binders_left_to_right g f (env, l as acc) sigma c = let app = (mkApp (hdf, Array.sub al 0 (Array.length al - 1))) in let app' = f acc app in let a' = f acc a in - (match EConstr.kind sigma app' with - | App (hdf', al') when hdf' == hdf -> - (* Still the same projection, we ignore the change in parameters *) - mkProj (p, a') - | _ -> mkApp (app', [| a' |])) + let hdf', _ = decompose_app_vect sigma app' in + if hdf' == hdf then + (* Still the same projection, we ignore the change in parameters *) + mkProj (p, a') + else mkApp (app', [| a' |]) | _ -> map_constr_with_binders_left_to_right sigma g f acc c let e_contextually byhead (occs,c) f = begin fun env sigma t -> diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 5b87603d54..1df377b20e 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1149,10 +1149,9 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e if !debug_unification then Feedback.msg_debug (str "Leaving unification with success"); a with e -> - let e = CErrors.push e in + let e = Exninfo.capture e in if !debug_unification then Feedback.msg_debug (str "Leaving unification with failure"); - iraise e - + Exninfo.iraise e let unify_0 env sigma = unify_0_with_initial_metas (sigma,[],[]) true env |