From c8c8ccdaaffefdbd3d78c844552a08bcb7b4f915 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Nov 2016 02:12:40 +0100 Subject: Evar-normalizing functions now act on EConstrs. --- engine/evarutil.ml | 31 +++++------ engine/evarutil.mli | 4 +- engine/proofview.ml | 22 ++++---- engine/proofview.mli | 8 +-- engine/termops.mli | 4 +- ide/ide_slave.ml | 5 +- ltac/rewrite.ml | 23 ++++----- ltac/tacinterp.ml | 1 - plugins/decl_mode/decl_proof_instr.ml | 1 + plugins/derive/derive.ml | 5 +- plugins/funind/functional_principles_proofs.ml | 2 +- plugins/funind/functional_principles_types.ml | 2 +- plugins/funind/invfun.ml | 4 +- plugins/funind/recdef.ml | 6 +-- plugins/ssrmatching/ssrmatching.ml4 | 25 +++++---- pretyping/cases.ml | 8 +-- pretyping/coercion.ml | 1 - pretyping/evarconv.ml | 6 +-- pretyping/evardefine.ml | 5 +- pretyping/evarsolve.ml | 4 +- pretyping/pretype_errors.ml | 37 +++++++------- pretyping/pretype_errors.mli | 4 +- pretyping/pretyping.ml | 3 -- pretyping/reductionops.mli | 4 +- pretyping/typing.ml | 4 +- pretyping/unification.ml | 12 ++--- printing/printer.ml | 8 +-- proofs/pfedit.ml | 4 +- proofs/pfedit.mli | 10 ++-- proofs/proof.mli | 6 +-- proofs/proof_global.ml | 5 +- proofs/proof_global.mli | 4 +- proofs/tacmach.ml | 4 +- stm/lemmas.ml | 6 +-- stm/lemmas.mli | 6 +-- stm/stm.ml | 4 +- tactics/auto.ml | 2 +- tactics/class_tactics.ml | 6 +-- tactics/contradiction.ml | 3 +- tactics/eauto.ml | 3 +- tactics/equality.ml | 2 +- tactics/hints.ml | 3 +- tactics/leminv.ml | 2 - tactics/tactics.ml | 4 +- toplevel/auto_ind_decl.ml | 4 +- toplevel/classes.ml | 4 +- toplevel/command.ml | 71 +++++++++++++++----------- toplevel/himsg.ml | 56 ++++++++++---------- toplevel/obligations.ml | 4 +- toplevel/vernacentries.ml | 8 +-- 50 files changed, 233 insertions(+), 227 deletions(-) diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 8940be09d..42620c0b5 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -99,16 +99,21 @@ let rec whd_evar sigma c = if u' == u then c else mkConstructU (co, u') | _ -> c -let rec nf_evar sigma t = Constr.map (fun t -> nf_evar sigma t) (whd_evar sigma t) -let e_nf_evar sigma t = EConstr.of_constr (nf_evar sigma (EConstr.Unsafe.to_constr t)) +(** Term exploration up to instantiation. *) +let kind_of_term_upto sigma t = + Constr.kind (whd_evar sigma t) + +let rec nf_evar0 sigma t = Constr.map (fun t -> nf_evar0 sigma t) (whd_evar sigma t) +let whd_evar sigma c = EConstr.of_constr (whd_evar sigma (EConstr.Unsafe.to_constr c)) +let nf_evar sigma c = EConstr.of_constr (nf_evar0 sigma (EConstr.Unsafe.to_constr c)) let j_nf_evar sigma j = - { uj_val = e_nf_evar sigma j.uj_val; - uj_type = e_nf_evar sigma j.uj_type } + { uj_val = nf_evar sigma j.uj_val; + uj_type = nf_evar sigma j.uj_type } let jl_nf_evar sigma jl = List.map (j_nf_evar sigma) jl let jv_nf_evar sigma = Array.map (j_nf_evar sigma) let tj_nf_evar sigma {utj_val=v;utj_type=t} = - {utj_val=e_nf_evar sigma v;utj_type=t} + {utj_val=nf_evar sigma v;utj_type=t} let nf_evars_universes evm = Universes.nf_evars_and_universes_opt_subst (safe_evar_value evm) @@ -125,23 +130,23 @@ let e_nf_evars_and_universes evdref = let nf_evar_map_universes evm = let evm = Evd.nf_constraints evm in let subst = Evd.universe_subst evm in - if Univ.LMap.is_empty subst then evm, nf_evar evm + if Univ.LMap.is_empty subst then evm, nf_evar0 evm else let f = nf_evars_universes evm in Evd.raw_map (fun _ -> map_evar_info f) evm, f let nf_named_context_evar sigma ctx = - Context.Named.map (nf_evar sigma) ctx + Context.Named.map (nf_evar0 sigma) ctx let nf_rel_context_evar sigma ctx = - Context.Rel.map (nf_evar sigma) ctx + Context.Rel.map (nf_evar0 sigma) ctx let nf_env_evar sigma env = let nc' = nf_named_context_evar sigma (Environ.named_context env) in let rel' = nf_rel_context_evar sigma (Environ.rel_context env) in push_rel_context rel' (reset_with_named_context (val_of_named_context nc') env) -let nf_evar_info evc info = map_evar_info (nf_evar evc) info +let nf_evar_info evc info = map_evar_info (nf_evar0 evc) info let nf_evar_map evm = Evd.raw_map (fun _ evi -> nf_evar_info evm evi) evm @@ -527,7 +532,7 @@ let rec check_and_clear_in_constr env evdref err ids global c = | Evar (evk,l as ev) -> if Evd.is_defined !evdref evk then (* If evk is already defined we replace it by its definition *) - let nc = whd_evar !evdref c in + let nc = Evd.existential_value !evdref ev in (check_and_clear_in_constr env evdref err ids global nc) else (* We check for dependencies to elements of ids in the @@ -582,7 +587,7 @@ let rec check_and_clear_in_constr env evdref err ids global c = let evi' = { evi with evar_extra = extra' } in evdref := Evd.add !evdref evk evi' ; (* spiwack: /hacking session *) - whd_evar !evdref c + Evd.existential_value !evdref ev | _ -> map_constr (check_and_clear_in_constr env evdref err ids global) c @@ -751,10 +756,6 @@ let subterm_source evk (loc,k) = (loc,Evar_kinds.SubEvar evk) -(** Term exploration up to instantiation. *) -let kind_of_term_upto sigma t = - Constr.kind (whd_evar sigma t) - (** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and [u] up to existential variable instantiation and equalisable universes. The term [t] is interpreted in [sigma1] while [u] is diff --git a/engine/evarutil.mli b/engine/evarutil.mli index ea9599c8b..67de18abc 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -139,8 +139,8 @@ val judge_of_new_Type : 'r Sigma.t -> (unsafe_judgment, 'r) Sigma.sigma (** [flush_and_check_evars] raise [Uninstantiated_evar] if an evar remains uninstantiated; [nf_evar] leaves uninstantiated evars as is *) -val whd_evar : evar_map -> constr -> constr -val nf_evar : evar_map -> constr -> constr +val whd_evar : evar_map -> EConstr.constr -> EConstr.constr +val nf_evar : evar_map -> EConstr.constr -> EConstr.constr val j_nf_evar : evar_map -> EConstr.unsafe_judgment -> EConstr.unsafe_judgment val jl_nf_evar : evar_map -> EConstr.unsafe_judgment list -> EConstr.unsafe_judgment list diff --git a/engine/proofview.ml b/engine/proofview.ml index 9e5e9c7da..ab72cc405 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -24,7 +24,7 @@ type proofview = Proofview_monad.proofview (* The first items in pairs below are proofs (under construction). The second items in the pairs below are statements that are being proved. *) -type entry = (Term.constr * Term.types) list +type entry = (EConstr.constr * EConstr.types) list (** Returns a stylised view of a proofview for use by, for instance, ide-s. *) @@ -37,15 +37,16 @@ let proofview p = p.comb , p.solution let compact el ({ solution } as pv) = - let nf = Evarutil.nf_evar solution in + let nf c = Evarutil.nf_evar solution c in + let nf0 c = EConstr.Unsafe.to_constr (Evarutil.nf_evar solution (EConstr.of_constr c)) in let size = Evd.fold (fun _ _ i -> i+1) solution 0 in let new_el = List.map (fun (t,ty) -> nf t, nf ty) el in let pruned_solution = Evd.drop_all_defined solution in let apply_subst_einfo _ ei = Evd.({ ei with - evar_concl = nf ei.evar_concl; - evar_hyps = Environ.map_named_val nf ei.evar_hyps; - evar_candidates = Option.map (List.map nf) ei.evar_candidates }) in + evar_concl = nf0 ei.evar_concl; + evar_hyps = Environ.map_named_val nf0 ei.evar_hyps; + evar_candidates = Option.map (List.map nf0) ei.evar_candidates }) in let new_solution = Evd.raw_map_undefined apply_subst_einfo pruned_solution in let new_size = Evd.fold (fun _ _ i -> i+1) new_solution 0 in Feedback.msg_info (Pp.str (Printf.sprintf "Evars: %d -> %d\n" size new_size)); @@ -56,7 +57,7 @@ let compact el ({ solution } as pv) = type telescope = | TNil of Evd.evar_map - | TCons of Environ.env * Evd.evar_map * Term.types * (Evd.evar_map -> Term.constr -> telescope) + | TCons of Environ.env * Evd.evar_map * EConstr.types * (Evd.evar_map -> EConstr.constr -> telescope) let typeclass_resolvable = Evd.Store.field () @@ -71,11 +72,10 @@ let dependent_init = | TNil sigma -> [], { solution = sigma; comb = []; shelf = [] } | TCons (env, sigma, typ, t) -> let sigma = Sigma.Unsafe.of_evar_map sigma in - let Sigma (econstr, sigma, _) = Evarutil.new_evar env sigma ~src ~store (EConstr.of_constr typ) in - let econstr = EConstr.Unsafe.to_constr econstr in + let Sigma (econstr, sigma, _) = Evarutil.new_evar env sigma ~src ~store typ in + let (gl, _) = EConstr.destEvar (Sigma.to_evar_map sigma) econstr in let sigma = Sigma.to_evar_map sigma in let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in - let (gl, _) = Term.destEvar econstr in let entry = (econstr, typ) :: ret in entry, { solution = sol; comb = gl :: comb; shelf = [] } in @@ -1222,12 +1222,12 @@ module V82 = struct { Evd.it = comb ; sigma = solution } let top_goals initial { solution=solution; } = - let goals = CList.map (fun (t,_) -> fst (Term.destEvar t)) initial in + let goals = CList.map (fun (t,_) -> fst (Term.destEvar (EConstr.Unsafe.to_constr t))) initial in { Evd.it = goals ; sigma=solution; } let top_evars initial = let evars_of_initial (c,_) = - Evar.Set.elements (Evd.evars_of_term c) + Evar.Set.elements (Evd.evars_of_term (EConstr.Unsafe.to_constr c)) in CList.flatten (CList.map evars_of_initial initial) diff --git a/engine/proofview.mli b/engine/proofview.mli index 2350592a2..9f10e874a 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -43,7 +43,7 @@ val compact : entry -> proofview -> entry * proofview empty [evar_map] (indeed a proof can be triggered by an incomplete pretyping), [init] takes an additional argument to represent the initial [evar_map]. *) -val init : Evd.evar_map -> (Environ.env * Term.types) list -> entry * proofview +val init : Evd.evar_map -> (Environ.env * EConstr.types) list -> entry * proofview (** A [telescope] is a list of environment and conclusion like in {!init}, except that each element may depend on the previous @@ -52,7 +52,7 @@ val init : Evd.evar_map -> (Environ.env * Term.types) list -> entry * proofview [evar_map] is threaded in state passing style. *) type telescope = | TNil of Evd.evar_map - | TCons of Environ.env * Evd.evar_map * Term.types * (Evd.evar_map -> Term.constr -> telescope) + | TCons of Environ.env * Evd.evar_map * EConstr.types * (Evd.evar_map -> EConstr.constr -> telescope) (** Like {!init}, but goals are allowed to be dependent on one another. Dependencies between goals is represented with the type @@ -69,8 +69,8 @@ val finished : proofview -> bool (** Returns the current [evar] state. *) val return : proofview -> Evd.evar_map -val partial_proof : entry -> proofview -> constr list -val initial_goals : entry -> (constr * types) list +val partial_proof : entry -> proofview -> EConstr.constr list +val initial_goals : entry -> (EConstr.constr * EConstr.types) list diff --git a/engine/termops.mli b/engine/termops.mli index 3f924cfa1..196962354 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -12,8 +12,8 @@ open Pp open Names open Term -open EConstr open Environ +open EConstr (** printers *) val print_sort : sorts -> std_ppcmds @@ -283,4 +283,4 @@ val on_judgment_type : ('t -> 't) -> ('c, 't) punsafe_judgment -> ('c, 't) puns (** {6 Functions to deal with impossible cases } *) val set_impossible_default_clause : (unit -> (Constr.constr * Constr.types) Univ.in_universe_context_set) -> unit -val coq_unit_judge : unit -> EConstr.unsafe_judgment Univ.in_universe_context_set +val coq_unit_judge : unit -> unsafe_judgment Univ.in_universe_context_set diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index fcba01353..8fc5547ec 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -191,12 +191,11 @@ let process_goal sigma g = let min_env = Environ.reset_context env in let id = Goal.uid g in let ccl = - let norm_constr = Reductionops.nf_evar sigma (EConstr.Unsafe.to_constr (Goal.V82.concl sigma g)) in - let norm_constr = EConstr.of_constr norm_constr in + let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in Richpp.richpp_of_pp (pr_goal_concl_style_env env sigma norm_constr) in let process_hyp d (env,l) = - let d = CompactedDecl.map_constr (Reductionops.nf_evar sigma) d in + let d = CompactedDecl.map_constr (fun c -> EConstr.Unsafe.to_constr (Reductionops.nf_evar sigma (EConstr.of_constr c))) d in let d' = CompactedDecl.to_named_context d in (List.fold_right Environ.push_named d' env, (Richpp.richpp_of_pp (pr_compacted_decl env sigma d)) :: l) in diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index 715929c56..c942e8e92 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -57,9 +57,6 @@ let nlocal_def (na, b, t) = let inj = EConstr.Unsafe.to_constr in NamedDecl.LocalDef (na, inj b, inj t) -let nf_evar sigma c = - EConstr.of_constr (Evarutil.nf_evar sigma (EConstr.Unsafe.to_constr c)) - (** Typeclass-based generalized rewriting. *) (** Constants used by the tactic. *) @@ -663,7 +660,7 @@ let solve_remaining_by env sigma holes by = (** Evar should not be defined, but just in case *) | Some evi -> let env = Environ.reset_with_named_context evi.evar_hyps env in - let ty = evi.evar_concl in + let ty = EConstr.of_constr evi.evar_concl in let c, sigma = Pfedit.refine_by_tactic env sigma ty solve_tac in Evd.define evk c sigma in @@ -738,7 +735,7 @@ let unify_eqn (car, rel, prf, c1, c2, holes, sort) l2r flags env (sigma, cstrs) let sigma = Typeclasses.resolve_typeclasses ~filter:(no_constraints cstrs) ~fail:true env sigma in let evd = solve_remaining_by env sigma holes by in - let nf c = nf_evar evd (Reductionops.nf_meta evd c) in + let nf c = Reductionops.nf_evar evd (Reductionops.nf_meta evd c) in let c1 = nf c1 and c2 = nf c2 and rew_car = nf car and rel = nf rel and prf = nf prf in @@ -1449,7 +1446,7 @@ module Strategies = in try let sigma = Unification.w_unify env sigma CONV ~flags:(Unification.elim_flags ()) unfolded t in - let c' = nf_evar sigma c in + let c' = Reductionops.nf_evar sigma c in state, Success { rew_car = ty; rew_from = t; rew_to = c'; rew_prf = RewCast DEFAULTcast; rew_evars = (sigma, snd evars) } @@ -1522,7 +1519,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul | Success res -> let (_, cstrs) = res.rew_evars in let evars' = solve_constraints env res.rew_evars in - let newt = nf_evar evars' res.rew_to in + let newt = Reductionops.nf_evar evars' res.rew_to in let evars = (* Keep only original evars (potentially instantiated) and goal evars, the rest has been defined and substituted already. *) Evar.Set.fold @@ -1537,13 +1534,13 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul let res = match res.rew_prf with | RewCast c -> None | RewPrf (rel, p) -> - let p = nf_zeta env evars' (nf_evar evars' p) in + let p = nf_zeta env evars' (Reductionops.nf_evar evars' p) in let term = match abs with | None -> p | Some (t, ty) -> - let t = nf_evar evars' t in - let ty = nf_evar evars' ty in + let t = Reductionops.nf_evar evars' t in + let ty = Reductionops.nf_evar evars' ty in mkApp (mkLambda (Name (Id.of_string "lemma"), ty, p), [| t |]) in let proof = match is_hyp with @@ -2024,7 +2021,7 @@ let add_morphism_infer glob m n = let hook = Lemmas.mk_hook hook in Flags.silently (fun () -> - Lemmas.start_proof instance_id kind (Evd.from_ctx uctx) instance hook; + Lemmas.start_proof instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) hook; ignore (Pfedit.by (Tacinterp.interp tac))) () let add_morphism glob binders m s n = @@ -2085,7 +2082,7 @@ let unification_rewrite l2r c1 c2 sigma prf car rel but env = ~flags:rewrite_conv_unif_flags env sigma ((if l2r then c1 else c2),but) in - let nf c = nf_evar sigma c in + let nf c = Reductionops.nf_evar sigma c in let c1 = if l2r then nf c' else nf c1 and c2 = if l2r then nf c2 else nf c' and car = nf car and rel = nf rel in @@ -2104,7 +2101,7 @@ let get_hyp gl (c,l) clause l2r = let sigma, hi = decompose_applied_relation env evars (c,l) in let but = match clause with | Some id -> Tacmach.New.pf_get_hyp_typ id gl - | None -> nf_evar evars (Tacmach.New.pf_concl gl) + | None -> Reductionops.nf_evar evars (Tacmach.New.pf_concl gl) in unification_rewrite l2r hi.c1 hi.c2 sigma hi.prf hi.car hi.rel but env diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 36a0336bc..62d0cc529 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -2101,7 +2101,6 @@ let interp_redexp env sigma r = let _ = let eval ty env sigma lfun arg = - let ty = EConstr.Unsafe.to_constr ty in let ist = { lfun = lfun; extra = TacStore.empty; } in if Genarg.has_type arg (glbwit wit_tactic) then let tac = Genarg.out_gen (glbwit wit_tactic) arg in diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 6a0ec3968..da971fffb 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -1506,6 +1506,7 @@ let rec postprocess pts instr = | Pend (B_elim ET_Induction) -> begin let pfterm = List.hd (Proof.partial_proof pts) in + let pfterm = EConstr.Unsafe.to_constr pfterm in let { it = gls ; sigma = sigma } = Proof.V82.subgoals pts in let env = try Goal.V82.env sigma (List.hd gls) diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index f23f4ce7d..12d7f0660 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -28,16 +28,17 @@ let start_deriving f suchthat lemma = (* spiwack: I don't know what the rigidity flag does, picked the one that looked the most general. *) let (sigma,f_type_sort) = Evd.new_sort_variable Evd.univ_flexible_alg sigma in - let f_type_type = Term.mkSort f_type_sort in + let f_type_type = EConstr.mkSort f_type_sort in (** create the initial goals for the proof: |- Type ; |- ?1 ; f:=?2 |- suchthat *) let goals = let open Proofview in TCons ( env , sigma , f_type_type , (fun sigma f_type -> TCons ( env , sigma , f_type , (fun sigma ef -> + let f_type = EConstr.Unsafe.to_constr f_type in + let ef = EConstr.Unsafe.to_constr ef in let env' = Environ.push_named (LocalDef (f, ef, f_type)) env in let evdref = ref sigma in let suchthat = Constrintern.interp_type_evars env' evdref suchthat in - let suchthat = EConstr.Unsafe.to_constr suchthat in TCons ( env' , !evdref , suchthat , (fun sigma _ -> TNil sigma)))))) in diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index f4fa61a22..91b17b9a4 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1007,7 +1007,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num (mk_equation_id f_id) (Decl_kinds.Global, Flags.is_universe_polymorphism (), (Decl_kinds.Proof Decl_kinds.Theorem)) evd - (EConstr.Unsafe.to_constr lemma_type) + lemma_type (Lemmas.mk_hook (fun _ _ -> ())); ignore (Pfedit.by (Proofview.V82.tactic prove_replacement)); Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None))); diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index ba01b3b04..d0d44b34b 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -294,7 +294,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin new_princ_name (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem)) !evd - new_principle_type + (EConstr.of_constr new_principle_type) hook ; (* let _tim1 = System.get_time () in *) diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 5cbec7743..dcec2cb74 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -846,7 +846,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( lem_id (Decl_kinds.Global,Flags.is_universe_polymorphism (),((Decl_kinds.Proof Decl_kinds.Theorem))) !evd - (EConstr.Unsafe.to_constr typ) + typ (Lemmas.mk_hook (fun _ _ -> ())); ignore (Pfedit.by (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")") @@ -908,7 +908,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( let lem_id = mk_complete_id f_id in Lemmas.start_proof lem_id (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem)) sigma - (EConstr.Unsafe.to_constr (fst lemmas_types_infos.(i))) + (fst lemmas_types_infos.(i)) (Lemmas.mk_hook (fun _ _ -> ())); ignore (Pfedit.by (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")") diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index adbdb1eb7..56c6ab054 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1374,7 +1374,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp Lemmas.start_proof na (Decl_kinds.Global, false (* FIXME *), Decl_kinds.Proof Decl_kinds.Lemma) - sigma (EConstr.Unsafe.to_constr gls_type) + sigma gls_type (Lemmas.mk_hook hook); if Indfun_common.is_strict_tcc () then @@ -1421,7 +1421,7 @@ let com_terminate let (evmap, env) = Lemmas.get_current_context() in Lemmas.start_proof thm_name (Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env) - ctx (compute_terminate_type nb_args fonctional_ref) hook; + ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) hook; ignore (by (Proofview.V82.tactic (observe_tac (str "starting_tac") tac_start))); ignore (by (Proofview.V82.tactic (observe_tac (str "whole_start") (whole_start tac_end nb_args is_mes fonctional_ref @@ -1476,7 +1476,7 @@ let (com_eqn : int -> Id.t -> (Lemmas.start_proof eq_name (Global, false, Proof Lemma) ~sign:(Environ.named_context_val env) evmap - equation_lemma_type + (EConstr.of_constr equation_lemma_type) (Lemmas.mk_hook (fun _ _ -> ())); ignore (by (Proofview.V82.tactic (start_equation f_ref terminate_ref diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index eb5f401e3..bf3e2ac1c 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -178,6 +178,9 @@ let mk_lterm = mk_term ' ' let pf_type_of gl t = let sigma, ty = pf_type_of gl t in re_sig (sig_it gl) sigma, ty +let nf_evar sigma c = + EConstr.Unsafe.to_constr (Evarutil.nf_evar sigma (EConstr.of_constr c)) + (* }}} *) (** Profiling {{{ *************************************************************) @@ -780,13 +783,13 @@ let on_instance, instances = let rec uniquize = function | [] -> [] | (sigma,_,{ up_f = f; up_a = a; up_t = t } as x) :: xs -> - let t = Reductionops.nf_evar sigma t in - let f = Reductionops.nf_evar sigma f in - let a = Array.map (Reductionops.nf_evar sigma) a in + let t = nf_evar sigma t in + let f = nf_evar sigma f in + let a = Array.map (nf_evar sigma) a in let neq (sigma1,_,{ up_f = f1; up_a = a1; up_t = t1 }) = - let t1 = Reductionops.nf_evar sigma1 t1 in - let f1 = Reductionops.nf_evar sigma1 f1 in - let a1 = Array.map (Reductionops.nf_evar sigma1) a1 in + let t1 = nf_evar sigma1 t1 in + let f1 = nf_evar sigma1 f1 in + let a1 = Array.map (nf_evar sigma1) a1 in not (Term.eq_constr t t1 && Term.eq_constr f f1 && CArray.for_all2 Term.eq_constr a a1) in x :: uniquize (List.filter neq xs) in @@ -1138,7 +1141,7 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty = if k = h_k || List.mem k acc || Evd.mem sigma0 k then acc else (update k; k::acc) | _ -> fold_constr aux acc t in - aux [] (Evarutil.nf_evar sigma rp) in + aux [] (nf_evar sigma rp) in let sigma = List.fold_left (fun sigma e -> if Evd.is_defined sigma e then sigma else (* clear may be recursive *) @@ -1195,7 +1198,7 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty = let sigma, rp = interp_term ist gl rp in let _, h, _, rp = destLetIn rp in let sigma = cleanup_XinE h x rp sigma in - let rp = subst1 h (Evarutil.nf_evar sigma rp) in + let rp = subst1 h (nf_evar sigma rp) in sigma, mk h rp | E_In_X_In_T(e, x, rp) | E_As_X_In_T (e, x, rp) -> let mk e x p = @@ -1204,7 +1207,7 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty = let sigma, rp = interp_term ist gl rp in let _, h, _, rp = destLetIn rp in let sigma = cleanup_XinE h x rp sigma in - let rp = subst1 h (Evarutil.nf_evar sigma rp) in + let rp = subst1 h (nf_evar sigma rp) in let sigma, e = interp_term ist (re_sig (sig_it gl) sigma) e in sigma, mk e h rp ;; @@ -1220,7 +1223,7 @@ let noindex = Some(false,[]) (* calls do_subst on every sub-term identified by (pattern,occ) *) let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = - let fs sigma x = Reductionops.nf_evar sigma x in + let fs sigma x = nf_evar sigma x in let pop_evar sigma e p = let { Evd.evar_body = e_body } as e_def = Evd.find sigma e in let e_body = match e_body with Evar_defined c -> c @@ -1307,7 +1310,7 @@ let redex_of_pattern ?(resolve_typeclasses=false) env (sigma, p) = let sigma = if not resolve_typeclasses then sigma else Typeclasses.resolve_typeclasses ~fail:false env sigma in - Reductionops.nf_evar sigma e, Evd.evar_universe_context sigma + nf_evar sigma e, Evd.evar_universe_context sigma let fill_occ_pattern ?raise_NoMatch env sigma cl pat occ h = let do_make_rel, occ = diff --git a/pretyping/cases.ml b/pretyping/cases.ml index eea94f021..0e4c6619b 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -362,7 +362,7 @@ let coerce_row typing_fun evdref env pats (tomatch,(_,indopt)) = let j = typing_fun tycon env evdref tomatch in let evd, j = Coercion.inh_coerce_to_base (loc_of_glob_constr tomatch) env !evdref j in evdref := evd; - let typ = EConstr.of_constr (nf_evar !evdref (EConstr.Unsafe.to_constr j.uj_type)) in + let typ = nf_evar !evdref j.uj_type in let t = try try_find_ind env !evdref typ realnames with Not_found -> @@ -1145,7 +1145,7 @@ let postprocess_dependencies evd tocheck brs tomatch pred deps cs = let rec aux k brs tomatch pred tocheck deps = match deps, tomatch with | [], _ -> brs,tomatch,pred,[] | n::deps, Abstract (i,d) :: tomatch -> - let d = map_constr (nf_evar evd) d in + let d = map_constr (fun c -> EConstr.Unsafe.to_constr (nf_evar evd (EConstr.of_constr c))) d in let is_d = match d with LocalAssum _ -> false | LocalDef _ -> true in if is_d || List.exists (fun c -> dependent_decl evd (lift k c) d) tocheck && Array.exists (is_dependent_branch evd k) brs then @@ -2008,9 +2008,9 @@ let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred = let envar = List.fold_right push_rel_context arsign env in let sigma, newt = new_sort_variable univ_flexible_alg sigma in let evdref = ref sigma in - let predcclj = typing_fun (mk_tycon (EConstr.mkSort newt)) envar evdref rtntyp in + let predcclj = typing_fun (mk_tycon (mkSort newt)) envar evdref rtntyp in let sigma = !evdref in - let predccl = EConstr.of_constr (nf_evar sigma (EConstr.Unsafe.to_constr predcclj.uj_val)) in + let predccl = nf_evar sigma predcclj.uj_val in [sigma, predccl] in List.map diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index ead44cee2..91f53a886 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -417,7 +417,6 @@ let inh_tosort_force loc env evd j = try let t,p = lookup_path_to_sort_from env evd j.uj_type in let evd,j1 = apply_coercion env evd p j t in - let whd_evar evd c = EConstr.of_constr (whd_evar evd (EConstr.Unsafe.to_constr c)) in let j2 = on_judgment_type (whd_evar evd) j1 in (evd,type_judgment env evd j2) with Not_found | NoCoercion -> diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 87267d538..3ae2e35e6 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -526,7 +526,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | None, Success i' -> (* We do have sk1[] = sk2[]: we now unify ?ev1 and ?ev2 *) (* Note that ?ev1 and ?ev2, may have been instantiated in the meantime *) - let ev1' = EConstr.of_constr (whd_evar i' (EConstr.Unsafe.to_constr (mkEvar ev1))) in + let ev1' = whd_evar i' (mkEvar ev1) in if isEvar i' ev1' then solve_simple_eqn (evar_conv_x ts) env i' (position_problem true pbty,destEvar i' ev1', term2) @@ -536,7 +536,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | Some (r,[]), Success i' -> (* We have sk1'[] = sk2[] for some sk1' s.t. sk1[]=sk1'[r[]] *) (* we now unify r[?ev1] and ?ev2 *) - let ev2' = EConstr.of_constr (whd_evar i' (EConstr.Unsafe.to_constr (mkEvar ev2))) in + let ev2' = whd_evar i' (mkEvar ev2) in if isEvar i' ev2' then solve_simple_eqn (evar_conv_x ts) env i' (position_problem false pbty,destEvar i' ev2',Stack.zip evd (term1,r)) @@ -547,7 +547,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (* Symmetrically *) (* We have sk1[] = sk2'[] for some sk2' s.t. sk2[]=sk2'[r[]] *) (* we now unify ?ev1 and r[?ev2] *) - let ev1' = EConstr.of_constr (whd_evar i' (EConstr.Unsafe.to_constr (mkEvar ev1))) in + let ev1' = whd_evar i' (mkEvar ev1) in if isEvar i' ev1' then solve_simple_eqn (evar_conv_x ts) env i' (position_problem true pbty,destEvar i' ev1',Stack.zip evd (term2,r)) diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index 875e4a118..5831d3191 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -33,8 +33,9 @@ let new_evar_unsafe env evd ?src ?filter ?candidates ?store ?naming ?principal t (Sigma.to_evar_map evd, evk) let env_nf_evar sigma env = + let nf_evar c = EConstr.Unsafe.to_constr (nf_evar sigma (EConstr.of_constr c)) in process_rel_context - (fun d e -> push_rel (RelDecl.map_constr (nf_evar sigma) d) e) env + (fun d e -> push_rel (RelDecl.map_constr nf_evar d) e) env let env_nf_betaiotaevar sigma env = process_rel_context @@ -144,7 +145,7 @@ let define_pure_evar_as_lambda env evd evk = | _ -> error_not_product env evd typ in let avoid = ids_of_named_context (evar_context evi) in let id = - next_name_away_with_default_using_types "x" na avoid (Reductionops.whd_evar evd (EConstr.Unsafe.to_constr dom)) in + next_name_away_with_default_using_types "x" na avoid (EConstr.Unsafe.to_constr (Reductionops.whd_evar evd dom)) in let newenv = push_named (nlocal_assum (id, dom)) evenv in let filter = Filter.extend 1 (evar_filter evi) in let src = evar_source evk evd1 in diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index de2e46a78..3235c2505 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -601,13 +601,13 @@ let define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_si let evd = Sigma.Unsafe.of_evar_map evd in let Sigma (evar_in_env, evd, _) = new_evar_instance sign evd ty_t_in_sign ~filter ~src inst_in_env in let evd = Sigma.to_evar_map evd in - let t_in_env = EConstr.of_constr (whd_evar evd (EConstr.Unsafe.to_constr t_in_env)) in + let t_in_env = whd_evar evd t_in_env in let (evk, _) = destEvar evd evar_in_env in let evd = define_fun env evd None (destEvar evd evar_in_env) t_in_env in let ctxt = named_context_of_val sign in let inst_in_sign = inst_of_vars (Filter.filter_list filter ctxt) in let evar_in_sign = mkEvar (evk, inst_in_sign) in - (evd,EConstr.of_constr (whd_evar evd (EConstr.Unsafe.to_constr evar_in_sign))) + (evd,whd_evar evd evar_in_sign) (* We have x1..xq |- ?e1 : τ and had to solve something like * Σ; Γ |- ?e1[u1..uq] = (...\y1 ... \yk ... c), where c is typically some diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 673554005..24f6d1689 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -10,50 +10,51 @@ open Util open Names open Term open Environ +open EConstr open Type_errors type unification_error = - | OccurCheck of existential_key * EConstr.constr - | NotClean of EConstr.existential * env * EConstr.constr (* Constr is a variable not in scope *) + | OccurCheck of existential_key * constr + | NotClean of existential * env * constr (* Constr is a variable not in scope *) | NotSameArgSize | NotSameHead | NoCanonicalStructure - | ConversionFailed of env * EConstr.constr * EConstr.constr (* Non convertible closed terms *) + | ConversionFailed of env * constr * constr (* Non convertible closed terms *) | MetaOccurInBody of existential_key - | InstanceNotSameType of existential_key * env * EConstr.types * EConstr.types + | InstanceNotSameType of existential_key * env * types * types | UnifUnivInconsistency of Univ.univ_inconsistency | CannotSolveConstraint of Evd.evar_constraint * unification_error | ProblemBeyondCapabilities type position = (Id.t * Locus.hyp_location_flag) option -type position_reporting = (position * int) * EConstr.t +type position_reporting = (position * int) * constr -type subterm_unification_error = bool * position_reporting * position_reporting * (EConstr.constr * EConstr.constr * unification_error) option +type subterm_unification_error = bool * position_reporting * position_reporting * (constr * constr * unification_error) option -type type_error = (EConstr.constr, EConstr.types) ptype_error +type type_error = (constr, types) ptype_error type pretype_error = (* Old Case *) - | CantFindCaseType of EConstr.constr + | CantFindCaseType of constr (* Type inference unification *) - | ActualTypeNotCoercible of EConstr.unsafe_judgment * EConstr.types * unification_error + | ActualTypeNotCoercible of unsafe_judgment * types * unification_error (* Tactic unification *) - | UnifOccurCheck of existential_key * EConstr.constr + | UnifOccurCheck of existential_key * constr | UnsolvableImplicit of existential_key * Evd.unsolvability_explanation option - | CannotUnify of EConstr.constr * EConstr.constr * unification_error option - | CannotUnifyLocal of EConstr.constr * EConstr.constr * EConstr.constr + | CannotUnify of constr * constr * unification_error option + | CannotUnifyLocal of constr * constr * constr | CannotUnifyBindingType of constr * constr | CannotGeneralize of constr - | NoOccurrenceFound of EConstr.constr * Id.t option - | CannotFindWellTypedAbstraction of EConstr.constr * EConstr.constr list * (env * type_error) option - | WrongAbstractionType of Name.t * EConstr.constr * EConstr.types * EConstr.types + | NoOccurrenceFound of constr * Id.t option + | CannotFindWellTypedAbstraction of constr * constr list * (env * type_error) option + | WrongAbstractionType of Name.t * constr * types * types | AbstractionOverMeta of Name.t * Name.t - | NonLinearUnification of Name.t * EConstr.constr + | NonLinearUnification of Name.t * constr (* Pretyping *) | VarNotFound of Id.t - | UnexpectedType of EConstr.constr * EConstr.constr - | NotProduct of EConstr.constr + | UnexpectedType of constr * constr + | NotProduct of constr | TypingError of type_error | CannotUnifyOccurrences of subterm_unification_error | UnsatisfiableConstraints of diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 7cef14339..c303d5d94 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -45,8 +45,8 @@ type pretype_error = | UnsolvableImplicit of existential_key * Evd.unsolvability_explanation option | CannotUnify of constr * constr * unification_error option | CannotUnifyLocal of constr * constr * constr - | CannotUnifyBindingType of Constr.constr * Constr.constr - | CannotGeneralize of Constr.constr + | CannotUnifyBindingType of constr * constr + | CannotGeneralize of constr | NoOccurrenceFound of constr * Id.t option | CannotFindWellTypedAbstraction of constr * constr list * (env * type_error) option | WrongAbstractionType of Name.t * constr * types * types diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 6b6800ac6..4660978df 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -143,9 +143,6 @@ let nf_fix sigma (nas, cs, ts) = let inj c = EConstr.to_constr sigma c in (nas, Array.map inj cs, Array.map inj ts) -let nf_evar sigma c = - EConstr.of_constr (nf_evar sigma (EConstr.Unsafe.to_constr c)) - let search_guard loc env possible_indexes fixdefs = (* Standard situation with only one possibility for each fix. *) (* We treat it separately in order to get proper error msg. *) diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 8aaeeb2c2..dcc11cfcf 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -156,11 +156,11 @@ val nf_beta : local_reduction_function val nf_betaiota : local_reduction_function val nf_betaiotazeta : local_reduction_function val nf_all : reduction_function -val nf_evar : evar_map -> Constr.constr -> Constr.constr +val nf_evar : evar_map -> constr -> constr (** Lazy strategy, weak head reduction *) -val whd_evar : evar_map -> Constr.constr -> Constr.constr +val whd_evar : evar_map -> constr -> constr val whd_nored : local_reduction_function val whd_beta : local_reduction_function val whd_betaiota : local_reduction_function diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 7baff421f..e6f1e46b6 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -252,7 +252,7 @@ let judge_of_letin env name defj typj j = (* cstr must be in n.f. w.r.t. evars and execute returns a judgement where both the term and type are in n.f. *) let rec execute env evdref cstr = - let cstr = EConstr.of_constr (whd_evar !evdref (EConstr.Unsafe.to_constr cstr)) in + let cstr = whd_evar !evdref cstr in match EConstr.kind !evdref cstr with | Meta n -> { uj_val = cstr; uj_type = meta_type !evdref n } @@ -411,6 +411,6 @@ let e_solve_evars env evdref c = let env = enrich_env env evdref in let c = (execute env evdref c).uj_val in (* side-effect on evdref *) - EConstr.of_constr (nf_evar !evdref (EConstr.Unsafe.to_constr c)) + nf_evar !evdref c let _ = Evarconv.set_solve_evars (fun env evdref c -> e_solve_evars env evdref c) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 20f27a15a..1dc3ccdc0 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -137,7 +137,7 @@ let abstract_list_all_with_dependencies env evd typ c l = Evarconv.second_order_matching empty_transparent_state env evd ev' argoccs c in if b then - let p = nf_evar evd (EConstr.Unsafe.to_constr ev) in + let p = nf_evar evd ev in evd, p else error_cannot_find_well_typed_abstraction env evd c l None @@ -1240,7 +1240,7 @@ let try_to_coerce env evd c cty tycon = let j = make_judge c cty in let (evd',j') = inh_conv_coerce_rigid_to true Loc.ghost env evd j tycon in let evd' = Evarconv.consider_remaining_unif_problems env evd' in - let evd' = Evd.map_metas_fvalue (nf_evar evd') evd' in + let evd' = Evd.map_metas_fvalue (fun c -> EConstr.Unsafe.to_constr (nf_evar evd' (EConstr.of_constr c))) evd' in (evd',j'.uj_val) let w_coerce_to_type env evd c cty mvty = @@ -1397,7 +1397,7 @@ let w_merge env with_types flags (evd,metas,evars : subst0) = let evd''' = w_merge_rec evd'' mc ec [] in if evd' == evd''' then Evd.define sp (EConstr.Unsafe.to_constr c) evd''' - else Evd.define sp (Evarutil.nf_evar evd''' (EConstr.Unsafe.to_constr c)) evd''' in + else Evd.define sp (EConstr.Unsafe.to_constr (Evarutil.nf_evar evd''' c)) evd''' in let check_types evd = let metas = Evd.meta_list evd in @@ -1513,8 +1513,7 @@ let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env current_sig let current_sigma = Sigma.to_evar_map current_sigma in let sigma = Pretyping.solve_remaining_evars flags env current_sigma pending in let sigma, subst = nf_univ_variables sigma in - let c = EConstr.Unsafe.to_constr c in - Sigma.Unsafe.of_pair (EConstr.of_constr (CVars.subst_univs_constr subst (nf_evar sigma c)), sigma) + Sigma.Unsafe.of_pair (EConstr.of_constr (CVars.subst_univs_constr subst (EConstr.Unsafe.to_constr (nf_evar sigma c))), sigma) let default_matching_core_flags sigma = let ts = Names.full_transparent_state in { @@ -1602,7 +1601,7 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) = (fun test -> match test.testing_state with | None -> None | Some (sigma,_,l) -> - let c = applist (EConstr.of_constr (nf_evar sigma (EConstr.Unsafe.to_constr (local_strong whd_meta sigma c))), l) in + let c = applist (nf_evar sigma (local_strong whd_meta sigma c), l) in let univs, subst = nf_univ_variables sigma in Some (sigma,EConstr.of_constr (CVars.subst_univs_constr subst (EConstr.Unsafe.to_constr c)))) @@ -1926,7 +1925,6 @@ let secondOrderAbstraction env evd flags typ (p, oplist) = let secondOrderDependentAbstraction env evd flags typ (p, oplist) = let typp = Typing.meta_type evd p in let evd, pred = abstract_list_all_with_dependencies env evd typp typ oplist in - let pred = EConstr.of_constr pred in w_merge env false flags.merge_unify_flags (evd,[p,pred,(Conv,TypeProcessed)],[]) diff --git a/printing/printer.ml b/printing/printer.ml index ba4b68296..63aeec82c 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -506,8 +506,8 @@ let print_evar_constraints gl sigma = end in let pr_evconstr (pbty,env,t1,t2) = - let t1 = Evarutil.nf_evar sigma t1 - and t2 = Evarutil.nf_evar sigma t2 in + let t1 = Evarutil.nf_evar sigma (EConstr.of_constr t1) + and t2 = Evarutil.nf_evar sigma (EConstr.of_constr t2) in let env = (** We currently allow evar instances to refer to anonymous de Bruijn indices, so we protect the error printing code in this case by giving @@ -517,11 +517,11 @@ let print_evar_constraints gl sigma = naming/renaming *) Namegen.make_all_name_different env in str" " ++ - hov 2 (pr_env env ++ pr_lconstr_env env sigma t1 ++ spc () ++ + hov 2 (pr_env env ++ pr_leconstr_env env sigma t1 ++ spc () ++ str (match pbty with | Reduction.CONV -> "==" | Reduction.CUMUL -> "<=") ++ - spc () ++ pr_lconstr_env env sigma t2) + spc () ++ pr_leconstr_env env sigma t2) in let pr_candidate ev evi (candidates,acc) = if Option.has_some evi.evar_candidates then diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index af910810b..142fd9a89 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -199,6 +199,7 @@ let refine_by_tactic env sigma ty tac = | _ -> assert false in let ans = Reductionops.nf_evar sigma ans in + let ans = EConstr.Unsafe.to_constr ans in (** [neff] contains the freshly generated side-effects *) let neff = Evd.eval_side_effects sigma in (** Reset the old side-effects *) @@ -232,7 +233,8 @@ let solve_by_implicit_tactic env sigma evk = let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (CErrors.UserError (None,Pp.str"Proof is not complete."))) []) in (try let c = Evarutil.nf_evars_universes sigma evi.evar_concl in - if Evarutil.has_undefined_evars sigma (EConstr.of_constr c) then raise Exit; + let c = EConstr.of_constr c in + if Evarutil.has_undefined_evars sigma c then raise Exit; let (ans, _, ctx) = build_by_tactic env (Evd.evar_universe_context sigma) c tac in let sigma = Evd.set_universe_context sigma ctx in diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 807a554df..516125ea1 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -60,7 +60,7 @@ type lemma_possible_guards = Proof_global.lemma_possible_guards type universe_binders = Id.t Loc.located list val start_proof : - Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map -> named_context_val -> constr -> + Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map -> named_context_val -> EConstr.constr -> ?init_tac:unit Proofview.tactic -> Proof_global.proof_terminator -> unit @@ -106,7 +106,7 @@ val get_current_context : unit -> Evd.evar_map * env (** [current_proof_statement] *) val current_proof_statement : - unit -> Id.t * goal_kind * types + unit -> Id.t * goal_kind * EConstr.types (** {6 ... } *) (** [get_current_proof_name ()] return the name of the current focused @@ -166,15 +166,15 @@ val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> unit val build_constant_by_tactic : Id.t -> Evd.evar_universe_context -> named_context_val -> ?goal_kind:goal_kind -> - types -> unit Proofview.tactic -> + EConstr.types -> unit Proofview.tactic -> Safe_typing.private_constants Entries.definition_entry * bool * Evd.evar_universe_context val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?poly:polymorphic -> - types -> unit Proofview.tactic -> + EConstr.types -> unit Proofview.tactic -> constr * bool * Evd.evar_universe_context -val refine_by_tactic : env -> Evd.evar_map -> types -> unit Proofview.tactic -> +val refine_by_tactic : env -> Evd.evar_map -> EConstr.types -> unit Proofview.tactic -> constr * Evd.evar_map (** A variant of the above function that handles open terms as well. Caveat: all effects are purged in the returned term at the end, but other diff --git a/proofs/proof.mli b/proofs/proof.mli index 5053fc7fb..8dcc5b76e 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -66,9 +66,9 @@ val map_structured_proof : proof -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre (*** General proof functions ***) -val start : Evd.evar_map -> (Environ.env * Term.types) list -> proof +val start : Evd.evar_map -> (Environ.env * EConstr.types) list -> proof val dependent_start : Proofview.telescope -> proof -val initial_goals : proof -> (Term.constr * Term.types) list +val initial_goals : proof -> (EConstr.constr * EConstr.types) list val initial_euctx : proof -> Evd.evar_universe_context (* Returns [true] if the considered proof is completed, that is if no goal remain @@ -79,7 +79,7 @@ val is_done : proof -> bool val is_complete : proof -> bool (* Returns the list of partial proofs to initial goals. *) -val partial_proof : proof -> Term.constr list +val partial_proof : proof -> EConstr.constr list val compact : proof -> proof diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 2956d623f..eb1bea897 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -375,6 +375,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = in let entries = Future.map2 (fun p (_, t) -> + let t = EConstr.Unsafe.to_constr t in let univstyp, body = make_body t p in let univs, typ = Future.force univstyp in { Entries. @@ -406,7 +407,7 @@ let return_proof ?(allow_partial=false) () = (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate side-effects... This may explain why one need to uniquize side-effects thereafter... *) - let proofs = List.map (fun c -> c, eff) proofs in + let proofs = List.map (fun c -> EConstr.Unsafe.to_constr c, eff) proofs in proofs, Evd.evar_universe_context evd end else let initial_goals = Proof.initial_goals proof in @@ -430,7 +431,7 @@ let return_proof ?(allow_partial=false) () = side-effects... This may explain why one need to uniquize side-effects thereafter... *) let proofs = - List.map (fun (c, _) -> (Evarutil.nf_evars_universes evd c, eff)) initial_goals in + List.map (fun (c, _) -> (Evarutil.nf_evars_universes evd (EConstr.Unsafe.to_constr c), eff)) initial_goals in proofs, Evd.evar_universe_context evd let close_future_proof ~feedback_id proof = diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 97a21cf22..3b2cc6b23 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -86,7 +86,7 @@ val apply_terminator : proof_terminator -> proof_ending -> unit end of the proof to close the proof. *) val start_proof : Evd.evar_map -> Names.Id.t -> ?pl:universe_binders -> - Decl_kinds.goal_kind -> (Environ.env * Term.types) list -> + Decl_kinds.goal_kind -> (Environ.env * EConstr.types) list -> proof_terminator -> unit (** Like [start_proof] except that there may be dependencies between @@ -201,7 +201,7 @@ end val get_default_goal_selector : unit -> Vernacexpr.goal_selector module V82 : sig - val get_current_initial_conclusions : unit -> Names.Id.t *(Term.types list * + val get_current_initial_conclusions : unit -> Names.Id.t *(EConstr.types list * Decl_kinds.goal_kind) end diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 2fab026ea..3ed262d6e 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -223,7 +223,7 @@ module New = struct let gl = Proofview.Goal.assume gl in let concl = Proofview.Goal.concl gl in let sigma = project gl in - EConstr.of_constr (nf_evar sigma (EConstr.Unsafe.to_constr concl)) + nf_evar sigma concl let pf_whd_all gl t = pf_apply whd_all gl t @@ -241,6 +241,6 @@ module New = struct let pf_whd_all gl t = pf_apply whd_all gl t let pf_compute gl t = pf_apply compute gl t - let pf_nf_evar gl t = EConstr.of_constr (nf_evar (project gl) (EConstr.Unsafe.to_constr t)) + let pf_nf_evar gl t = nf_evar (project gl) t end diff --git a/stm/lemmas.ml b/stm/lemmas.ml index e3f1c1ac2..77fb960e1 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -449,7 +449,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook = List.iter (fun (strength,ref,imps) -> maybe_declare_manual_implicits false ref imps; call_hook (fun exn -> exn) hook strength ref) thms_data in - start_proof_univs id ?pl kind ctx t ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard + start_proof_univs id ?pl kind ctx (EConstr.of_constr t) ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard let start_proof_com ?inference_hook kind thms hook = let env0 = Global.env () in @@ -461,13 +461,12 @@ let start_proof_com ?inference_hook kind thms hook = let thms = List.map (fun (sopt,(bl,t,guard)) -> let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in let t', imps' = interp_type_evars_impls ~impls env evdref t in - let t' = EConstr.Unsafe.to_constr t' in let flags = all_and_fail_flags in let flags = { flags with use_hook = inference_hook } in evdref := solve_remaining_evars flags env !evdref (Evd.empty,!evdref); let ids = List.map RelDecl.get_name ctx in (compute_proof_name (pi1 kind) sopt, - (nf_evar !evdref (Term.it_mkProd_or_LetIn t' ctx), + (EConstr.Unsafe.to_constr (nf_evar !evdref (EConstr.it_mkProd_or_LetIn t' ctx)), (ids, imps @ lift_implicits (List.length ids) imps'), guard))) thms in @@ -519,6 +518,7 @@ let save_proof ?proof = function | None -> let pftree = Pfedit.get_pftreestate () in let id, k, typ = Pfedit.current_proof_statement () in + let typ = EConstr.Unsafe.to_constr typ in let universes = Proof.initial_euctx pftree in (* This will warn if the proof is complete *) let pproofs, _univs = diff --git a/stm/lemmas.mli b/stm/lemmas.mli index 39c089be9..681413a29 100644 --- a/stm/lemmas.mli +++ b/stm/lemmas.mli @@ -19,17 +19,17 @@ val call_hook : Future.fix_exn -> 'a declaration_hook -> Decl_kinds.locality -> Globnames.global_reference -> 'a (** A hook start_proof calls on the type of the definition being started *) -val set_start_hook : (types -> unit) -> unit +val set_start_hook : (EConstr.types -> unit) -> unit val start_proof : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map -> ?terminator:(lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) -> - ?sign:Environ.named_context_val -> types -> + ?sign:Environ.named_context_val -> EConstr.types -> ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> unit declaration_hook -> unit val start_proof_univs : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map -> ?terminator:(lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> Proof_global.proof_terminator) -> - ?sign:Environ.named_context_val -> types -> + ?sign:Environ.named_context_val -> EConstr.types -> ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> unit diff --git a/stm/stm.ml b/stm/stm.ml index d60412c0c..47e806929 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1719,8 +1719,10 @@ end = struct (* {{{ *) match Evd.(evar_body (find sigma r_goal)) with | Evd.Evar_empty -> RespNoProgress | Evd.Evar_defined t -> + let t = EConstr.of_constr t in let t = Evarutil.nf_evar sigma t in - if Evarutil.is_ground_term sigma (EConstr.of_constr t) then + if Evarutil.is_ground_term sigma t then + let t = EConstr.Unsafe.to_constr t in RespBuiltSubProof (t, Evd.evar_universe_context sigma) else CErrors.user_err ~hdr:"STM" (str"The solution is not ground") end) () diff --git a/tactics/auto.ml b/tactics/auto.ml index b548f8b92..17a488ddb 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -321,7 +321,7 @@ let rec trivial_fail_db dbg mod_delta db_list local_db = ( Proofview.Goal.enter { enter = begin fun gl -> let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in - let nf c = Evarutil.nf_evar sigma c in + let nf c = EConstr.Unsafe.to_constr (Evarutil.nf_evar sigma (EConstr.of_constr c)) in let decl = Tacmach.New.pf_last_hyp (Proofview.Goal.assume gl) in let hyp = Context.Named.Declaration.map_constr nf decl in let hintl = make_resolve_hyp env sigma hyp diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index fa2c21ac3..a4b6cb53b 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -521,8 +521,7 @@ let evars_to_goals p evm = (** Making local hints *) let make_resolve_hyp env sigma st flags only_classes pri decl = let id = NamedDecl.get_id decl in - let cty = Evarutil.nf_evar sigma (NamedDecl.get_type decl) in - let cty = EConstr.of_constr cty in + let cty = Evarutil.nf_evar sigma (EConstr.of_constr (NamedDecl.get_type decl)) in let rec iscl env ty = let ctx, ar = decompose_prod_assum sigma ty in match EConstr.kind sigma (fst (decompose_app sigma ar)) with @@ -1476,8 +1475,7 @@ let resolve_one_typeclass env ?(sigma=Evd.empty) gl unique = in let evd = sig_sig gls' in let t' = mkEvar (ev, Array.of_list subst) in - let term = Evarutil.nf_evar evd (EConstr.Unsafe.to_constr t') in - let term = EConstr.of_constr term in + let term = Evarutil.nf_evar evd t' in evd, term let _ = diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index a3a448aad..7173fb4fd 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -66,8 +66,7 @@ let contradiction_context = | [] -> Tacticals.New.tclZEROMSG (Pp.str"No such contradiction") | d :: rest -> let id = NamedDecl.get_id d in - let typ = nf_evar sigma (NamedDecl.get_type d) in - let typ = EConstr.of_constr typ in + let typ = nf_evar sigma (EConstr.of_constr (NamedDecl.get_type d)) in let typ = whd_all env sigma typ in if is_empty_type sigma typ then simplest_elim (mkVar id) diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 01f21910c..7453fff5c 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -289,8 +289,7 @@ module SearchProblem = struct in let rec_tacs = let l = - let concl = Reductionops.nf_evar (project g) (EConstr.Unsafe.to_constr (pf_concl g)) in - let concl = EConstr.of_constr concl in + let concl = Reductionops.nf_evar (project g) (pf_concl g) in filter_tactics s.tacres (e_possible_resolve (project g) s.dblist (List.hd s.localdb) secvars concl) in diff --git a/tactics/equality.ml b/tactics/equality.ml index c80cf4416..072da995d 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1212,7 +1212,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = error "Cannot solve a unification problem." in let scf = sigrec_clausal_form siglen ty in - !evdref, EConstr.of_constr (Evarutil.nf_evar !evdref (EConstr.Unsafe.to_constr scf)) + !evdref, Evarutil.nf_evar !evdref scf (* The problem is to build a destructor (a generalization of the predecessor) which, when applied to a term made of constructors diff --git a/tactics/hints.ml b/tactics/hints.ml index 851e9f01f..ef97b0b33 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1200,7 +1200,8 @@ let prepare_hint check (poly,local) env init (sigma,c) = It is actually a bit stupid to generalize over evars since the first thing make_resolves will do is to re-instantiate the products *) let sigma, subst = Evd.nf_univ_variables sigma in - let c = Evarutil.nf_evar sigma (EConstr.Unsafe.to_constr c) in + let c = Evarutil.nf_evar sigma c in + let c = EConstr.Unsafe.to_constr c in let c = CVars.subst_univs_constr subst c in let c = EConstr.of_constr c in let c = drop_extra_implicit_args sigma c in diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 3199623e7..a05b4fbf3 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -208,14 +208,12 @@ let inversion_scheme env sigma t sort dep_option inv_op = user_err ~hdr:"lemma_inversion" (str"Computed inversion goal was not closed in initial signature."); *) - let invGoal = EConstr.Unsafe.to_constr invGoal in let pf = Proof.start (Evd.from_ctx (evar_universe_context sigma)) [invEnv,invGoal] in let pf = fst (Proof.run_tactic env ( tclTHEN intro (onLastHypId inv_op)) pf) in let pfterm = List.hd (Proof.partial_proof pf) in - let pfterm = EConstr.of_constr pfterm in let global_named_context = Global.named_context_val () in let ownSign = ref begin fold_named_context diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 10582288c..0ecccd5c0 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2945,7 +2945,6 @@ let quantify lconstr = (* Modifying/Adding an hypothesis *) let specialize (c,lbind) ipat = - let nf_evar sigma c = EConstr.of_constr (nf_evar sigma (EConstr.Unsafe.to_constr c)) in Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in @@ -3825,7 +3824,7 @@ let specialize_eqs id gl = let acc' = it_mkLambda_or_LetIn acc ctx'' in let ty' = Tacred.whd_simpl env !evars ty' and acc' = Tacred.whd_simpl env !evars acc' in - let ty' = EConstr.of_constr (Evarutil.nf_evar !evars (EConstr.Unsafe.to_constr ty')) in + let ty' = Evarutil.nf_evar !evars ty' in if worked then tclTHENFIRST (Tacmach.internal_cut true id ty') (Proofview.V82.of_tactic (exact_no_check ((* refresh_universes_strict *) acc'))) gl @@ -4951,6 +4950,7 @@ let abstract_subproof id gk tac = let ctx = Evd.universe_context_set evd in evd, ctx, nf concl in + let concl = EConstr.of_constr concl in let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac) in let ectx = Evd.evar_universe_context evd in let (const, safe, ectx) = diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 5e686c41e..14071d869 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -658,6 +658,7 @@ let make_bl_scheme mode mind = let bl_goal, eff = compute_bl_goal ind lnamesparrec nparrec in let ctx = Evd.make_evar_universe_context (Global.env ()) None in let side_eff = side_effect_of_mode mode in + let bl_goal = EConstr.of_constr bl_goal in let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx bl_goal (compute_bl_tact mode (!bl_scheme_kind_aux()) (ind, Univ.Instance.empty) lnamesparrec nparrec) in @@ -783,6 +784,7 @@ let make_lb_scheme mode mind = let lb_goal, eff = compute_lb_goal ind lnamesparrec nparrec in let ctx = Evd.make_evar_universe_context (Global.env ()) None in let side_eff = side_effect_of_mode mode in + let lb_goal = EConstr.of_constr lb_goal in let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx lb_goal (compute_lb_tact mode (!lb_scheme_kind_aux()) ind lnamesparrec nparrec) in @@ -956,7 +958,7 @@ let make_eq_decidability mode mind = context_chop (nparams-nparrec) mib.mind_params_ctxt in let side_eff = side_effect_of_mode mode in let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx - (compute_dec_goal (ind,u) lnamesparrec nparrec) + (EConstr.of_constr (compute_dec_goal (ind,u) lnamesparrec nparrec)) (compute_dec_tact ind lnamesparrec nparrec) in ([|ans|], ctx), Safe_typing.empty_private_constants diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 5087aa0c8..7a5d0ed81 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -181,7 +181,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p let env' = push_rel_context ctx env in evars := Evarutil.nf_evar_map !evars; evars := resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:true env !evars; - let subst = List.map (Evarutil.nf_evar !evars) subst in + let subst = List.map (fun c -> EConstr.Unsafe.to_constr (Evarutil.nf_evar !evars (EConstr.of_constr c))) subst in if abstract then begin let subst = List.fold_left2 @@ -327,7 +327,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p the refinement manually.*) let gls = List.rev (Evd.future_goals evm) in let evm = Evd.reset_future_goals evm in - Lemmas.start_proof id kind evm termtype + Lemmas.start_proof id kind evm (EConstr.of_constr termtype) (Lemmas.mk_hook (fun _ -> instance_hook k pri global imps ?hook)); (* spiwack: I don't know what to do with the status here. *) diff --git a/toplevel/command.ml b/toplevel/command.ml index 7e3828131..44fc4eb1a 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -306,7 +306,8 @@ let do_assumptions_unbound_univs (_, poly, _ as kind) nl l = (env,empty_internalization_env) l in let evd = solve_remaining_evars all_and_fail_flags env !evdref (Evd.empty,!evdref) in - let l = List.map (on_pi2 (nf_evar evd)) l in + let nf_evar c = EConstr.Unsafe.to_constr (nf_evar evd (EConstr.of_constr c)) in + let l = List.map (on_pi2 nf_evar) l in snd (List.fold_left (fun (subst,status) ((is_coe,idl),t,(ctx,imps)) -> let t = replace_vars subst t in let (refs,status') = declare_assumptions idl is_coe kind (t,ctx) [] imps false nl in @@ -465,7 +466,7 @@ let sign_level env evd sign = | LocalDef _ -> lev, push_rel d env | LocalAssum _ -> let s = destSort (Reduction.whd_all env - (nf_evar evd (EConstr.Unsafe.to_constr (Retyping.get_type_of env evd (EConstr.of_constr (RelDecl.get_type d)))))) + (EConstr.Unsafe.to_constr (nf_evar evd (Retyping.get_type_of env evd (EConstr.of_constr (RelDecl.get_type d)))))) in let u = univ_of_sort s in (Univ.sup u lev, push_rel d env)) @@ -905,8 +906,9 @@ let fix_sub_ref = make_ref fixsub_module "Fix_sub" let measure_on_R_ref = make_ref fixsub_module "MR" let well_founded = init_constant ["Init"; "Wf"] "well_founded" let mkSubset name typ prop = - mkApp (Universes.constr_of_global (delayed_force build_sigma).typ, - [| typ; mkLambda (name, typ, prop) |]) + let open EConstr in + EConstr.Unsafe.to_constr (mkApp (EConstr.of_constr (Universes.constr_of_global (delayed_force build_sigma).typ), + [| typ; mkLambda (name, typ, prop) |])) let sigT = Lazy.from_fun build_sigma_type let make_qref s = Qualid (Loc.ghost, qualid_of_string s) @@ -943,9 +945,11 @@ let rec telescope = function ty, (LocalDef (n, b, t) :: subst), lift 1 term let nf_evar_context sigma ctx = - List.map (map_constr (Evarutil.nf_evar sigma)) ctx + List.map (map_constr (fun c -> EConstr.Unsafe.to_constr (Evarutil.nf_evar sigma (EConstr.of_constr c)))) ctx let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = + let open EConstr in + let open Vars in Coqlib.check_required_library ["Coq";"Program";"Wf"]; let env = Global.env() in let ctx = Evd.make_evar_universe_context env pl in @@ -954,11 +958,12 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let len = List.length binders_rel in let top_env = push_rel_context binders_rel env in let top_arity = interp_type_evars top_env evdref arityc in - let top_arity = EConstr.Unsafe.to_constr top_arity in - let full_arity = Term.it_mkProd_or_LetIn top_arity binders_rel in + let full_arity = it_mkProd_or_LetIn top_arity binders_rel in let argtyp, letbinders, make = telescope binders_rel in + let make = EConstr.of_constr make in let argname = Id.of_string "recarg" in let arg = LocalAssum (Name argname, argtyp) in + let argtyp = EConstr.of_constr argtyp in let binders = letbinders @ [arg] in let binders_env = push_rel_context binders_rel env in let rel, _ = interp_constr_evars_impls env evdref r in @@ -977,22 +982,21 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = | _, _ -> error () with e when CErrors.noncritical e -> error () in - let rel = EConstr.Unsafe.to_constr rel in let measure = interp_casted_constr_evars binders_env evdref measure relargty in - let measure = EConstr.Unsafe.to_constr measure in let wf_rel, wf_rel_fun, measure_fn = let measure_body, measure = it_mkLambda_or_LetIn measure letbinders, it_mkLambda_or_LetIn measure binders in - let comb = Universes.constr_of_global (delayed_force measure_on_R_ref) in + let comb = EConstr.of_constr (Universes.constr_of_global (delayed_force measure_on_R_ref)) in + let relargty = EConstr.of_constr relargty in let wf_rel = mkApp (comb, [| argtyp; relargty; rel; measure |]) in let wf_rel_fun x y = mkApp (rel, [| subst1 x measure_body; subst1 y measure_body |]) in wf_rel, wf_rel_fun, measure in - let wf_proof = mkApp (delayed_force well_founded, [| argtyp ; wf_rel |]) in + let wf_proof = mkApp (EConstr.of_constr (delayed_force well_founded), [| argtyp ; wf_rel |]) in let argid' = Id.of_string (Id.to_string argname ^ "'") in let wfarg len = LocalAssum (Name argid', mkSubset (Name argid') argtyp @@ -1000,7 +1004,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = in let intern_bl = wfarg 1 :: [arg] in let _intern_env = push_rel_context intern_bl env in - let proj = (*FIXME*)Universes.constr_of_global (delayed_force build_sigma).Coqlib.proj1 in + let proj = (*FIXME*)EConstr.of_constr (Universes.constr_of_global (delayed_force build_sigma).Coqlib.proj1) in let wfargpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel 3)) in let projection = (* in wfarg :: arg :: before *) mkApp (proj, [| argtyp ; wfargpred ; mkRel 1 |]) @@ -1009,17 +1013,21 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let intern_arity = substl [projection] top_arity_let in (* substitute the projection of wfarg for something, now intern_arity is in wfarg :: arg *) - let intern_fun_arity_prod = Term.it_mkProd_or_LetIn intern_arity [wfarg 1] in + let intern_fun_arity_prod = it_mkProd_or_LetIn intern_arity [wfarg 1] in + let intern_fun_arity_prod = EConstr.Unsafe.to_constr intern_fun_arity_prod in let intern_fun_binder = LocalAssum (Name (add_suffix recname "'"), intern_fun_arity_prod) in let curry_fun = let wfpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel (2 * len + 4))) in - let intro = (*FIXME*)Universes.constr_of_global (delayed_force build_sigma).Coqlib.intro in + let intro = (*FIXME*)EConstr.of_constr (Universes.constr_of_global (delayed_force build_sigma).Coqlib.intro) in let arg = mkApp (intro, [| argtyp; wfpred; lift 1 make; mkRel 1 |]) in let app = mkApp (mkRel (2 * len + 2 (* recproof + orig binders + current binders *)), [| arg |]) in let rcurry = mkApp (rel, [| measure; lift len measure |]) in + let rcurry = EConstr.Unsafe.to_constr rcurry in let lam = LocalAssum (Name (Id.of_string "recproof"), rcurry) in let body = it_mkLambda_or_LetIn app (lam :: binders_rel) in - let ty = Term.it_mkProd_or_LetIn (lift 1 top_arity) (lam :: binders_rel) in + let ty = it_mkProd_or_LetIn (lift 1 top_arity) (lam :: binders_rel) in + let body = EConstr.Unsafe.to_constr body in + let ty = EConstr.Unsafe.to_constr ty in LocalDef (Name recname, body, ty) in let fun_bl = intern_fun_binder :: [arg] in @@ -1028,26 +1036,24 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let ctx = LocalAssum (Name recname, get_type curry_fun) :: binders_rel in let (r, l, impls, scopes) = Constrintern.compute_internalization_data env - Constrintern.Recursive full_arity impls + Constrintern.Recursive (EConstr.Unsafe.to_constr full_arity) impls in let newimpls = Id.Map.singleton recname (r, l, impls @ [(Some (Id.of_string "recproof", Impargs.Manual, (true, false)))], scopes @ [None]) in interp_casted_constr_evars (push_rel_context ctx env) evdref - ~impls:newimpls body (lift 1 top_arity) + ~impls:newimpls body (EConstr.Unsafe.to_constr (lift 1 top_arity)) in - let intern_body = EConstr.Unsafe.to_constr intern_body in let intern_body_lam = it_mkLambda_or_LetIn intern_body (curry_fun :: lift_lets @ fun_bl) in let prop = mkLambda (Name argname, argtyp, top_arity_let) in let def = - mkApp (Universes.constr_of_global (delayed_force fix_sub_ref), + mkApp (EConstr.of_constr (Universes.constr_of_global (delayed_force fix_sub_ref)), [| argtyp ; wf_rel ; - EConstr.Unsafe.to_constr (Evarutil.e_new_evar env evdref - ~src:(Loc.ghost, Evar_kinds.QuestionMark (Evar_kinds.Define false)) (EConstr.of_constr wf_proof)); + Evarutil.e_new_evar env evdref + ~src:(Loc.ghost, Evar_kinds.QuestionMark (Evar_kinds.Define false)) wf_proof; prop |]) in - let def = Typing.e_solve_evars env evdref (EConstr.of_constr def) in - let def = EConstr.Unsafe.to_constr def in + let def = Typing.e_solve_evars env evdref def in let _ = evdref := Evarutil.nf_evar_map !evdref in let def = mkApp (def, [|intern_body_lam|]) in let binders_rel = nf_evar_context !evdref binders_rel in @@ -1057,21 +1063,22 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = if List.length binders_rel > 1 then let name = add_suffix recname "_func" in let hook l gr _ = - let body = it_mkLambda_or_LetIn (mkApp (Universes.constr_of_global gr, [|make|])) binders_rel in - let ty = Term.it_mkProd_or_LetIn top_arity binders_rel in + let body = it_mkLambda_or_LetIn (mkApp (EConstr.of_constr (Universes.constr_of_global gr), [|make|])) binders_rel in + let ty = it_mkProd_or_LetIn top_arity binders_rel in + let ty = EConstr.Unsafe.to_constr ty in let pl, univs = Evd.universe_context ?names:pl !evdref in (*FIXME poly? *) - let ce = definition_entry ~poly ~types:ty ~univs (Evarutil.nf_evar !evdref body) in + let ce = definition_entry ~poly ~types:ty ~univs (EConstr.Unsafe.to_constr (Evarutil.nf_evar !evdref body)) in (** FIXME: include locality *) let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in let gr = ConstRef c in if Impargs.is_implicit_args () || not (List.is_empty impls) then Impargs.declare_manual_implicits false gr [impls] in - let typ = Term.it_mkProd_or_LetIn top_arity binders in + let typ = it_mkProd_or_LetIn top_arity binders in hook, name, typ else - let typ = Term.it_mkProd_or_LetIn top_arity binders_rel in + let typ = it_mkProd_or_LetIn top_arity binders_rel in let hook l gr _ = if Impargs.is_implicit_args () || not (List.is_empty impls) then Impargs.declare_manual_implicits false gr [impls] @@ -1080,6 +1087,8 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let hook = Lemmas.mk_hook hook in let fullcoqc = Evarutil.nf_evar !evdref def in let fullctyp = Evarutil.nf_evar !evdref typ in + let fullcoqc = EConstr.Unsafe.to_constr fullcoqc in + let fullctyp = EConstr.Unsafe.to_constr fullctyp in Obligations.check_evars env !evdref; let evars, _, evars_def, evars_typ = Obligations.eterm_obligations env recname !evdref 0 fullcoqc fullctyp @@ -1110,7 +1119,7 @@ let interp_recursive isfix fixl notations = let fixctximpenvs, fixctximps = List.split fiximppairs in let fixccls,fixcclimps = List.split (List.map3 (interp_fix_ccl evdref) fixctximpenvs fixctxs fixl) in let fixtypes = List.map2 build_fix_type fixctxs fixccls in - let fixtypes = List.map (nf_evar !evdref) fixtypes in + let fixtypes = List.map (fun c -> EConstr.Unsafe.to_constr (nf_evar !evdref (EConstr.of_constr c))) fixtypes in let fiximps = List.map3 (fun ctximps cclimps (_,ctx) -> ctximps@(Impargs.lift_implicits (List.length ctx) cclimps)) fixctximps fixcclimps fixctxs in @@ -1285,9 +1294,9 @@ let do_program_recursive local p fixkind fixl ntns = let collect_evars id def typ imps = (* Generalize by the recursive prototypes *) let def = - nf_evar evd (EConstr.Unsafe.to_constr (Termops.it_mkNamedLambda_or_LetIn (EConstr.of_constr def) rec_sign)) + EConstr.Unsafe.to_constr (nf_evar evd (Termops.it_mkNamedLambda_or_LetIn (EConstr.of_constr def) rec_sign)) and typ = - nf_evar evd (EConstr.Unsafe.to_constr (Termops.it_mkNamedProd_or_LetIn (EConstr.of_constr typ) rec_sign)) + EConstr.Unsafe.to_constr (nf_evar evd (Termops.it_mkNamedProd_or_LetIn (EConstr.of_constr typ) rec_sign)) in let evm = collect_evars_of_term evd def typ in let evars, _, def, typ = diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 3c2fe46b3..851b87903 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -86,16 +86,18 @@ let rec contract3' env a b c = function let to_unsafe_judgment j = on_judgment EConstr.Unsafe.to_constr j let j_nf_betaiotaevar sigma j = - { uj_val = Evarutil.nf_evar sigma (EConstr.Unsafe.to_constr j.uj_val); - uj_type = EConstr.Unsafe.to_constr (Reductionops.nf_betaiota sigma j.uj_type) } + { uj_val = Evarutil.nf_evar sigma j.uj_val; + uj_type = Reductionops.nf_betaiota sigma j.uj_type } let jv_nf_betaiotaevar sigma jl = - Array.map (fun j -> on_judgment EConstr.of_constr (j_nf_betaiotaevar sigma j)) jl + Array.map (fun j -> j_nf_betaiotaevar sigma j) jl (** Printers *) let pr_lconstr c = quote (pr_lconstr c) let pr_lconstr_env e s c = quote (pr_lconstr_env e s c) +let pr_leconstr c = quote (pr_leconstr c) +let pr_leconstr_env e s c = quote (pr_leconstr_env e s c) let pr_ljudge_env e s c = let v,t = pr_ljudge_env e s c in (quote v,quote t) (** A canonisation procedure for constr such that comparing there @@ -152,7 +154,8 @@ let explicit_flags = [print_implicits; print_coercions; print_no_symbol]; (** Then more! *) [print_universes; print_implicits; print_coercions; print_no_symbol] (** and more! *) ] -let pr_explicit env sigma t1 t2 = pr_explicit_aux env sigma t1 t2 explicit_flags +let pr_explicit env sigma t1 t2 = + pr_explicit_aux env sigma (EConstr.to_constr sigma t1) (EConstr.to_constr sigma t2) explicit_flags let pr_db env i = try @@ -263,9 +266,7 @@ let explain_number_branches env sigma cj expn = str "expects " ++ int expn ++ str " branches." let explain_ill_formed_branch env sigma c ci actty expty = - let actty = EConstr.Unsafe.to_constr actty in - let expty = EConstr.Unsafe.to_constr expty in - let simp t = Reduction.nf_betaiota env (Evarutil.nf_evar sigma t) in + let simp t = Reductionops.nf_betaiota sigma (Evarutil.nf_evar sigma t) in let env = make_all_name_different env in let pc = pr_leconstr_env env sigma c in let pa, pe = pr_explicit env sigma (simp actty) (simp expty) in @@ -302,13 +303,11 @@ let explain_unification_error env sigma p1 p2 = function | NotSameArgSize | NotSameHead | NoCanonicalStructure -> (* Error speaks from itself *) [] | ConversionFailed (env,t1,t2) -> - let t1 = EConstr.to_constr sigma t1 in - let t2 = EConstr.to_constr sigma t2 in - if Term.eq_constr t1 p1 && Term.eq_constr t2 p2 then [] else + if EConstr.eq_constr sigma t1 p1 && EConstr.eq_constr sigma t2 p2 then [] else let env = make_all_name_different env in let t1 = Evarutil.nf_evar sigma t1 in let t2 = Evarutil.nf_evar sigma t2 in - if not (Term.eq_constr t1 p1) || not (Term.eq_constr t2 p2) then + if not (EConstr.eq_constr sigma t1 p1) || not (EConstr.eq_constr sigma t2 p2) then let t1, t2 = pr_explicit env sigma t1 t2 in [str "cannot unify " ++ t1 ++ strbrk " and " ++ t2] else [] @@ -317,8 +316,6 @@ let explain_unification_error env sigma p1 p2 = function strbrk " refers to a metavariable - please report your example" ++ strbrk "at " ++ str Coq_config.wwwbugtracker ++ str "."] | InstanceNotSameType (evk,env,t,u) -> - let t = EConstr.to_constr sigma t in - let u = EConstr.to_constr sigma u in let t, u = pr_explicit env sigma t u in [str "unable to find a well-typed instantiation for " ++ quote (pr_existential_key sigma evk) ++ @@ -331,11 +328,13 @@ let explain_unification_error env sigma p1 p2 = function else [str "universe inconsistency"] | CannotSolveConstraint ((pb,env,t,u),e) -> + let t = EConstr.of_constr t in + let u = EConstr.of_constr u in let t = Evarutil.nf_evar sigma t in let u = Evarutil.nf_evar sigma u in let env = make_all_name_different env in - (strbrk "cannot satisfy constraint " ++ pr_lconstr_env env sigma t ++ - str " == " ++ pr_lconstr_env env sigma u) + (strbrk "cannot satisfy constraint " ++ pr_leconstr_env env sigma t ++ + str " == " ++ pr_leconstr_env env sigma u) :: aux t u e | ProblemBeyondCapabilities -> [] @@ -349,10 +348,9 @@ let explain_actual_type env sigma j t reason = let env = make_all_name_different env in let j = j_nf_betaiotaevar sigma j in let t = Reductionops.nf_betaiota sigma t in - let t = EConstr.Unsafe.to_constr t in (** Actually print *) let pe = pr_ne_context_of (str "In environment") env sigma in - let pc = pr_lconstr_env env sigma (Environ.j_val j) in + let pc = pr_leconstr_env env sigma (Environ.j_val j) in let (pt, pct) = pr_explicit env sigma t (Environ.j_type j) in let ppreason = explain_unification_error env sigma j.uj_type t reason in pe ++ @@ -363,11 +361,9 @@ let explain_actual_type env sigma j t reason = ppreason ++ str ".") let explain_cant_apply_bad_type env sigma (n,exptyp,actualtyp) rator randl = - let exptyp = EConstr.Unsafe.to_constr exptyp in let randl = jv_nf_betaiotaevar sigma randl in let exptyp = Evarutil.nf_evar sigma exptyp in let actualtyp = Reductionops.nf_betaiota sigma actualtyp in - let actualtyp = EConstr.Unsafe.to_constr actualtyp in let rator = Evarutil.j_nf_evar sigma rator in let env = make_all_name_different env in let actualtyp, exptyp = pr_explicit env sigma actualtyp exptyp in @@ -520,11 +516,9 @@ let explain_ill_formed_rec_body env sigma err names i fixenv vdefj = let explain_ill_typed_rec_body env sigma i names vdefj vargs = let vdefj = Evarutil.jv_nf_evar sigma vdefj in - let vargs = Array.map EConstr.Unsafe.to_constr vargs in - let vdefj = Array.map to_unsafe_judgment vdefj in let vargs = Array.map (Evarutil.nf_evar sigma) vargs in let env = make_all_name_different env in - let pvd = pr_lconstr_env env sigma vdefj.(i).uj_val in + let pvd = pr_leconstr_env env sigma vdefj.(i).uj_val in let pvdt, pv = pr_explicit env sigma vdefj.(i).uj_type vargs.(i) in str "The " ++ (match vdefj with [|_|] -> mt () | _ -> pr_nth (i+1) ++ spc ()) ++ @@ -584,13 +578,13 @@ let rec explain_evar_kind env sigma evk ty = function | Evar_kinds.SubEvar evk' -> let evi = Evd.find sigma evk' in let pc = match evi.evar_body with - | Evar_defined c -> pr_lconstr_env env sigma (Evarutil.nf_evar sigma c) + | Evar_defined c -> pr_leconstr_env env sigma (Evarutil.nf_evar sigma (EConstr.of_constr c)) | Evar_empty -> assert false in - let ty' = Evarutil.nf_evar sigma evi.evar_concl in + let ty' = Evarutil.nf_evar sigma (EConstr.of_constr evi.evar_concl) in pr_existential_key sigma evk ++ str " of type " ++ ty ++ str " in the partial instance " ++ pc ++ str " found for " ++ explain_evar_kind env sigma evk' - (pr_lconstr_env env sigma ty') (snd evi.evar_source) + (pr_leconstr_env env sigma ty') (snd evi.evar_source) let explain_typeclass_resolution env sigma evi k = match Typeclasses.class_of_constr sigma (EConstr.of_constr evi.evar_concl) with @@ -655,7 +649,7 @@ let explain_cannot_unify_local env sigma m n subn = let explain_refiner_cannot_generalize env sigma ty = str "Cannot find a well-typed generalisation of the goal with type: " ++ - pr_lconstr_env env sigma ty ++ str "." + pr_leconstr_env env sigma ty ++ str "." let explain_no_occurrence_found env sigma c id = let c = EConstr.to_constr sigma c in @@ -666,8 +660,8 @@ let explain_no_occurrence_found env sigma c id = | None -> str"the current goal") ++ str "." let explain_cannot_unify_binding_type env sigma m n = - let pm = pr_lconstr_env env sigma m in - let pn = pr_lconstr_env env sigma n in + let pm = pr_leconstr_env env sigma m in + let pn = pr_leconstr_env env sigma n in str "This binding has type" ++ brk(1,1) ++ pm ++ spc () ++ str "which should be unifiable with" ++ brk(1,1) ++ pn ++ str "." @@ -760,8 +754,6 @@ let explain_cannot_unify_occurrences env sigma nested ((cl2,pos2),t2) ((cl1,pos1 let ppreason = match e with | None -> mt() | Some (c1,c2,e) -> - let c1 = EConstr.to_constr sigma c1 in - let c2 = EConstr.to_constr sigma c2 in explain_unification_error env sigma c1 c2 (Some e) in str "Found incompatible occurrences of the pattern" ++ str ":" ++ @@ -841,12 +833,16 @@ let explain_pretype_error env sigma err = let actual = EConstr.Unsafe.to_constr actual in let expect = EConstr.Unsafe.to_constr expect in let env, actual, expect = contract2 env actual expect in + let actual = EConstr.of_constr actual in + let expect = EConstr.of_constr expect in explain_unexpected_type env sigma actual expect | NotProduct c -> explain_not_product env sigma c | CannotUnify (m,n,e) -> let m = EConstr.Unsafe.to_constr m in let n = EConstr.Unsafe.to_constr n in let env, m, n = contract2 env m n in + let m = EConstr.of_constr m in + let n = EConstr.of_constr n in explain_cannot_unify env sigma m n e | CannotUnifyLocal (m,n,sn) -> explain_cannot_unify_local env sigma m n sn | CannotGeneralize ty -> explain_refiner_cannot_generalize env sigma ty diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 6da2f82ab..f4a786a73 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -818,7 +818,7 @@ let rec string_of_list sep f = function let solve_by_tac name evi t poly ctx = let id = name in - let concl = evi.evar_concl in + let concl = EConstr.of_constr evi.evar_concl in (* spiwack: the status is dropped. *) let (entry,_,ctx') = Pfedit.build_constant_by_tactic id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps concl (Tacticals.New.tclCOMPLETE t) in @@ -936,7 +936,7 @@ let rec solve_obligation prg num tac = Proof_global.make_terminator (obligation_terminator prg.prg_name num guard hook auto) in let hook ctx = Lemmas.mk_hook (obligation_hook prg obl num auto ctx) in - let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd obl.obl_type ~terminator hook in + let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator hook in let _ = Pfedit.by !default_tactic in Option.iter (fun tac -> Pfedit.set_end_tac tac) tac diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 4376f51dc..cf3da7e02 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -59,7 +59,7 @@ let show_proof () = (* spiwack: this would probably be cooler with a bit of polishing. *) let p = Proof_global.give_me_the_proof () in let pprf = Proof.partial_proof p in - Feedback.msg_notice (Pp.prlist_with_sep Pp.fnl Printer.pr_constr pprf) + Feedback.msg_notice (Pp.prlist_with_sep Pp.fnl Printer.pr_econstr pprf) let show_node () = (* spiwack: I'm have little clue what this function used to do. I deactivated it, @@ -459,7 +459,8 @@ let start_proof_and_print k l hook = let env = Evd.evar_filtered_env evi in try let concl = Evarutil.nf_evars_universes sigma evi.Evd.evar_concl in - if Evarutil.has_undefined_evars sigma (EConstr.of_constr concl) then raise Exit; + let concl = EConstr.of_constr concl in + if Evarutil.has_undefined_evars sigma concl then raise Exit; let c, _, ctx = Pfedit.build_by_tactic env (Evd.evar_universe_context sigma) concl (Tacticals.New.tclCOMPLETE tac) @@ -877,6 +878,7 @@ let vernac_set_used_variables e = let env = Global.env () in let tys = List.map snd (Proof.initial_goals (Proof_global.give_me_the_proof ())) in + let tys = List.map EConstr.Unsafe.to_constr tys in let l = Proof_using.process_expr env e tys in let vars = Environ.named_context env in List.iter (fun id -> @@ -1901,7 +1903,7 @@ let vernac_check_guard () = try let { Evd.it=gl ; sigma=sigma } = Proof.V82.top_goal pts in Inductiveops.control_only_guard (Goal.V82.env sigma gl) - pfterm; + (EConstr.Unsafe.to_constr pfterm); (str "The condition holds up to here") with UserError(_,s) -> (str ("Condition violated: ") ++s) -- cgit v1.2.3