diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-26 16:18:47 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:30:44 +0100 |
| commit | b4b90c5d2e8c413e1981c456c933f35679386f09 (patch) | |
| tree | fc84ec244390beb2f495b024620af2e130ad5852 /proofs/tacmach.mli | |
| parent | 78a8d59b39dfcb07b94721fdcfd9241d404905d2 (diff) | |
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.
Diffstat (limited to 'proofs/tacmach.mli')
| -rw-r--r-- | proofs/tacmach.mli | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index efc3dbf55..3b23a6ab4 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -34,18 +34,18 @@ val apply_sig_tac : val pf_concl : goal sigma -> types val pf_env : goal sigma -> env -val pf_hyps : goal sigma -> Context.Named.t +val pf_hyps : goal sigma -> named_context (*i val pf_untyped_hyps : goal sigma -> (Id.t * constr) list i*) val pf_hyps_types : goal sigma -> (Id.t * types) list val pf_nth_hyp_id : goal sigma -> int -> Id.t -val pf_last_hyp : goal sigma -> Context.Named.Declaration.t +val pf_last_hyp : goal sigma -> named_declaration val pf_ids_of_hyps : goal sigma -> Id.t list val pf_global : goal sigma -> Id.t -> constr val pf_unsafe_type_of : goal sigma -> constr -> types val pf_type_of : goal sigma -> constr -> evar_map * types val pf_hnf_type_of : goal sigma -> constr -> types -val pf_get_hyp : goal sigma -> Id.t -> Context.Named.Declaration.t +val pf_get_hyp : goal sigma -> Id.t -> named_declaration val pf_get_hyp_typ : goal sigma -> Id.t -> types val pf_get_new_id : Id.t -> goal sigma -> Id.t @@ -117,9 +117,9 @@ module New : sig val pf_ids_of_hyps : ('a, 'r) Proofview.Goal.t -> identifier list val pf_hyps_types : ('a, 'r) Proofview.Goal.t -> (identifier * types) list - val pf_get_hyp : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> Context.Named.Declaration.t + val pf_get_hyp : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> named_declaration val pf_get_hyp_typ : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> types - val pf_last_hyp : ([ `NF ], 'r) Proofview.Goal.t -> Context.Named.Declaration.t + val pf_last_hyp : ([ `NF ], 'r) Proofview.Goal.t -> named_declaration val pf_nf_concl : ([ `LZ ], 'r) Proofview.Goal.t -> types val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> types -> pinductive * types |