From b4b90c5d2e8c413e1981c456c933f35679386f09 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Nov 2016 16:18:47 +0100 Subject: Definining EConstr-based contexts. This removes quite a few unsafe casts. Unluckily, I had to reintroduce the old non-module based names for these data structures, because I could not reproduce easily the same hierarchy in EConstr. --- engine/proofview.mli | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) (limited to 'engine/proofview.mli') diff --git a/engine/proofview.mli b/engine/proofview.mli index 9f10e874a..025e3de20 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -14,6 +14,7 @@ open Util open Term +open EConstr (** Main state of tactics *) type proofview @@ -43,7 +44,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 * EConstr.types) list -> entry * proofview +val init : Evd.evar_map -> (Environ.env * 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 +53,7 @@ val init : Evd.evar_map -> (Environ.env * EConstr.types) list -> entry * proofvi [evar_map] is threaded in state passing style. *) type telescope = | TNil of Evd.evar_map - | TCons of Environ.env * Evd.evar_map * EConstr.types * (Evd.evar_map -> EConstr.constr -> telescope) + | TCons of Environ.env * Evd.evar_map * types * (Evd.evar_map -> constr -> telescope) (** Like {!init}, but goals are allowed to be dependent on one another. Dependencies between goals is represented with the type @@ -69,8 +70,8 @@ val finished : proofview -> bool (** Returns the current [evar] state. *) val return : proofview -> Evd.evar_map -val partial_proof : entry -> proofview -> EConstr.constr list -val initial_goals : entry -> (EConstr.constr * EConstr.types) list +val partial_proof : entry -> proofview -> constr list +val initial_goals : entry -> (constr * types) list @@ -484,15 +485,15 @@ module Goal : sig respectively the conclusion of [gl], the hypotheses of [gl], the environment of [gl] (i.e. the global environment and the hypotheses) and the current evar map. *) - val concl : ([ `NF ], 'r) t -> EConstr.constr - val hyps : ([ `NF ], 'r) t -> Context.Named.t + val concl : ([ `NF ], 'r) t -> constr + val hyps : ([ `NF ], 'r) t -> named_context val env : ('a, 'r) t -> Environ.env val sigma : ('a, 'r) t -> 'r Sigma.t val extra : ('a, 'r) t -> Evd.Store.t (** Returns the goal's conclusion even if the goal is not normalised. *) - val raw_concl : ('a, 'r) t -> EConstr.constr + val raw_concl : ('a, 'r) t -> constr type ('a, 'b) enter = { enter : 'r. ('a, 'r) t -> 'b } -- cgit v1.2.3