diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 2 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 11 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 4 | ||||
| -rw-r--r-- | pretyping/unification.ml | 3 |
4 files changed, 11 insertions, 9 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 447a4c487c..fe2b0a5a1a 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1871,7 +1871,7 @@ let inh_conv_coerce_to_tycon loc env evdref j tycon = (* We put the tycon inside the arity signature, possibly discovering dependencies. *) let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c = - let nar = List.fold_left (fun n sign -> List.length sign + n) 0 arsign in + let nar = List.fold_left (fun n sign -> Context.Rel.nhyps sign + n) 0 arsign in let subst, len = List.fold_right2 (fun (tm, tmtype) sign (subst, len) -> let signlen = List.length sign in diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 1ef96e0344..f466740036 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -403,9 +403,10 @@ let ltac_interp_name_env k0 lvar env = (* tail is the part of the env enriched by pretyping *) let n = Context.Rel.length (rel_context env) - k0 in let ctxt,_ = List.chop n (rel_context env) in - let env = pop_rel_context n env in - let ctxt = List.map (Context.Rel.Declaration.map_name (ltac_interp_name lvar)) ctxt in - push_rel_context ctxt env + let open Context.Rel.Declaration in + let ctxt' = List.smartmap (map_name (ltac_interp_name lvar)) ctxt in + if List.equal (fun d1 d2 -> Name.equal (get_name d1) (get_name d2)) ctxt ctxt' then env + else push_rel_context ctxt' (pop_rel_context n env) let invert_ltac_bound_name lvar env id0 id = let id' = Id.Map.find id lvar.ltac_idents in @@ -803,8 +804,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let j = pretype_type empty_valcon env evdref lvar c2 in { j with utj_val = lift 1 j.utj_val } | Name _ -> - let var = (name,j.utj_val) in - let env' = ExtraEnv.make_env (push_rel_assum var env.ExtraEnv.env) in + let var = LocalAssum (name, j.utj_val) in + let env' = push_rel var env in pretype_type empty_valcon env' evdref lvar c2 in let name = ltac_interp_name lvar name in diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 5484e70b61..8259876c29 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -790,11 +790,11 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = (h 0 (str "<<" ++ Termops.print_constr x ++ str "|" ++ cut () ++ Cst_stack.pr cst_l ++ str "|" ++ cut () ++ Stack.pr Termops.print_constr stack ++ - str ">>") ++ fnl ()) + str ">>")) in let fold () = let () = if !debug_RAKAM then - let open Pp in Feedback.msg_notice (str "<><><><><>" ++ fnl ()) in + let open Pp in Feedback.msg_notice (str "<><><><><>") in (s,cst_l) in match kind_of_term x with diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 0c1ce0d2f8..6d80db6455 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1080,8 +1080,9 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb if !debug_unification then Feedback.msg_debug (str "Leaving unification with success"); a with e -> + let e = CErrors.push e in if !debug_unification then Feedback.msg_debug (str "Leaving unification with failure"); - raise e + iraise e let unify_0 env sigma = unify_0_with_initial_metas (sigma,[],[]) true env |