diff options
Diffstat (limited to 'pretyping/cases.ml')
| -rw-r--r-- | pretyping/cases.ml | 18 |
1 files changed, 12 insertions, 6 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 4c87b4e7e..16244d8c0 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -295,7 +295,8 @@ let inductive_template evdref env tmloc ind = | LocalAssum (na,ty) -> let ty = EConstr.of_constr ty in let ty' = substl subst ty in - let e = e_new_evar env evdref ~src:(hole_source n) ty' in + let evd, e = Evarutil.new_evar env !evdref ~src:(hole_source n) ty' in + evdref := evd; (e::subst,e::evarl,n+1) | LocalDef (na,b,ty) -> let b = EConstr.of_constr b in @@ -396,7 +397,9 @@ let coerce_to_indtype typing_fun evdref env lvar matx tomatchl = (* Utils *) let mkExistential env ?(src=(Loc.tag Evar_kinds.InternalHole)) evdref = - let e, u = e_new_type_evar env evdref univ_flexible_alg ~src:src in e + let evd, (e, u) = new_type_evar env !evdref univ_flexible_alg ~src:src in + evdref := evd; + e let evd_comb2 f evdref x y = let (evd',y) = f !evdref x y in @@ -1681,7 +1684,8 @@ let abstract_tycon ?loc env evdref subst tycon extenv t = (fun i _ -> try list_assoc_in_triple i subst0 with Not_found -> mkRel i) 1 (rel_context env) in - let ev' = e_new_evar env evdref ~src ty in + let evd, ev' = Evarutil.new_evar env !evdref ~src ty in + evdref := evd; begin match solve_simple_eqn (evar_conv_x full_transparent_state) env !evdref (None,ev,substl inst ev') with | Success evd -> evdref := evd | UnifFailure _ -> assert false @@ -1712,7 +1716,8 @@ let abstract_tycon ?loc env evdref subst tycon extenv t = (named_context extenv) in let filter = Filter.make (rel_filter @ named_filter) in let candidates = u :: List.map mkRel vl in - let ev = e_new_evar extenv evdref ~src ~filter ~candidates ty in + let evd, ev = Evarutil.new_evar extenv !evdref ~src ~filter ~candidates ty in + evdref := evd; lift k ev in aux (0,extenv,subst0) t0 @@ -1724,8 +1729,9 @@ let build_tycon ?loc env tycon_env s subst tycon extenv evdref t = we are in an impossible branch *) let n = Context.Rel.length (rel_context env) in let n' = Context.Rel.length (rel_context tycon_env) in - let impossible_case_type, u = - e_new_type_evar (reset_context env) evdref univ_flexible_alg ~src:(Loc.tag ?loc Evar_kinds.ImpossibleCase) in + let evd, (impossible_case_type, u) = + new_type_evar (reset_context env) !evdref univ_flexible_alg ~src:(Loc.tag ?loc Evar_kinds.ImpossibleCase) in + evdref := evd; (lift (n'-n) impossible_case_type, mkSort u) | Some t -> let t = abstract_tycon ?loc tycon_env evdref subst tycon extenv t in |