diff options
| author | Matthieu Sozeau | 2015-09-23 19:01:31 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-10-02 15:54:11 +0200 |
| commit | c92946243ccb0b11cd138f040a5297979229c3f5 (patch) | |
| tree | c472cbbb8ffd32a9dbdc3971477b339abbfe26ef | |
| parent | 91e01278de2420a64f1c8de03c0bc6e614577042 (diff) | |
Univs: fix after rebase (from_ctx/from_env)
| -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 9d3c0b4b46..1b12cd42ce 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 65dc51a84f..eadeebd38e 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 8243f96c16..842b87c57e 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 2946766cb1..e51dfbaaec 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 |