diff options
Diffstat (limited to 'vernac/command.ml')
| -rw-r--r-- | vernac/command.ml | 15 |
1 files changed, 6 insertions, 9 deletions
diff --git a/vernac/command.ml b/vernac/command.ml index 87e7e50ec2..b1425d7034 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -35,7 +35,6 @@ open Evarconv open Indschemes open Misctypes open Vernacexpr -open Sigma.Notations open Context.Rel.Declaration open Entries @@ -78,8 +77,7 @@ let red_constant_entry n ce sigma = function let env = Global.env () in let (redfun, _) = reduction_of_red_expr env red in let redfun env sigma c = - let sigma = Sigma.Unsafe.of_evar_map sigma in - let Sigma (c, _, _) = redfun.e_redfun env sigma c in + let (_, c) = redfun env sigma c in EConstr.Unsafe.to_constr c in { ce with const_entry_body = Future.chain ~pure:true proof_out @@ -582,7 +580,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = let pl = (List.hd indl).ind_univs in let ctx = Evd.make_evar_universe_context env0 pl in let evdref = ref Evd.(from_ctx ctx) in - let _, ((env_params, ctx_params), userimpls) = + let impls, ((env_params, ctx_params), userimpls) = interp_context_evars env0 evdref paramsl in let ctx_params = List.map (fun d -> map_rel_decl EConstr.Unsafe.to_constr d) ctx_params in @@ -603,7 +601,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = let indimpls = List.map (fun (_, _, impls) -> userimpls @ lift_implicits (Context.Rel.nhyps ctx_params) impls) arities in let arities = List.map pi1 arities and aritypoly = List.map pi2 arities in - let impls = compute_internalization_env env0 (Inductive params) indnames fullarities indimpls in + let impls = compute_internalization_env env0 ~impls (Inductive (params,true)) indnames fullarities indimpls in let implsforntn = compute_internalization_env env0 Variable indnames fullarities indimpls in let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in @@ -674,7 +672,7 @@ let extract_coercions indl = let extract_params indl = let paramsl = List.map (fun (_,params,_,_) -> params) indl in match paramsl with - | [] -> anomaly (Pp.str "empty list of inductive types") + | [] -> anomaly (Pp.str "empty list of inductive types.") | params::paramsl -> if not (List.for_all (eq_local_binders params) paramsl) then user_err Pp.(str "Parameters should be syntactically the same for each inductive type."); @@ -908,9 +906,8 @@ let tactics_module = subtac_dir @ ["Tactics"] let init_reference dir s () = Coqlib.coq_reference "Command" dir s let init_constant dir s evdref = - let Sigma (c, sigma, _) = Evarutil.new_global (Sigma.Unsafe.of_evar_map !evdref) - (Coqlib.coq_reference "Command" dir s) - in evdref := Sigma.to_evar_map sigma; c + let (sigma, c) = Evarutil.new_global !evdref (Coqlib.coq_reference "Command" dir s) + in evdref := sigma; c let make_ref l s = init_reference l s let fix_proto = init_constant tactics_module "fix_proto" |