diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/pfedit.ml | 4 | ||||
| -rw-r--r-- | proofs/pfedit.mli | 10 | ||||
| -rw-r--r-- | proofs/proof.mli | 6 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 5 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 4 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 4 |
6 files changed, 18 insertions, 15 deletions
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 |