diff options
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/indfun.ml | 2 | ||||
| -rw-r--r-- | pretyping/evd.ml | 7 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
4 files changed, 7 insertions, 6 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 9d3c0b4b4..1b12cd42c 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1106,7 +1106,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let not_free_in_t id = not (is_free_in id t) in let evd = (Evd.from_env env) in let t',ctx = Pretyping.understand env evd t in - let evd = Evd.from_env ~ctx env in + let evd = Evd.from_ctx ctx in let type_t' = Typing.unsafe_type_of env evd t' in let new_env = Environ.push_rel (n,Some t',type_t') env in let new_b,id_to_exclude = diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 65dc51a84..eadeebd38 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -597,7 +597,7 @@ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacex let fixl,ntns = Command.extract_fixpoint_components false fixpoint_exprl in let ((_,_,typel),ctx,_) = Command.interp_fixpoint fixl ntns in let constr_expr_typel = - with_full_print (List.map (Constrextern.extern_constr false (Global.env ()) (Evd.from_env ~ctx (Global.env ())))) typel in + with_full_print (List.map (Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx))) typel in let fixpoint_exprl_with_new_bl = List.map2 (fun ((lna,(rec_arg_opt,rec_order),bl,ret_typ,opt_body),notation_list) fix_typ -> diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 8243f96c1..842b87c57 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -1136,9 +1136,10 @@ let make_evar_universe_context e l = match l with | None -> uctx | Some us -> - List.fold_left (fun uctx (loc,id) -> - fst (uctx_new_univ_variable univ_rigid (Some (Id.to_string id)) uctx)) - uctx us + List.fold_left + (fun uctx (loc,id) -> + fst (uctx_new_univ_variable univ_rigid (Some (Id.to_string id)) true uctx)) + uctx us (****************************************) (* Operations on constants *) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 2946766cb..e51dfbaae 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1187,7 +1187,7 @@ let vernac_reserve bl = let env = Global.env() in let sigma = Evd.from_env env in let t,ctx = Constrintern.interp_type env sigma c in - let t = Detyping.detype false [] env (Evd.from_env ~ctx env) t in + let t = Detyping.detype false [] env (Evd.from_ctx ctx) t in let t = Notation_ops.notation_constr_of_glob_constr (default_env ()) t in Reserve.declare_reserved_type idl t) in List.iter sb_decl bl |