aboutsummaryrefslogtreecommitdiffhomepage
path: root/API/API.mli
diff options
context:
space:
mode:
Diffstat (limited to 'API/API.mli')
-rw-r--r--API/API.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/API/API.mli b/API/API.mli
index 3ed326ff0..4b6c755a6 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4631,6 +4631,7 @@ sig
val pf_ids_set_of_hyps : 'a Proofview.Goal.t -> Names.Id.Set.t
val pf_concl : 'a Proofview.Goal.t -> EConstr.types
val pf_get_new_id : Names.Id.t -> 'a Proofview.Goal.t -> Names.Id.t
+ val pf_get_hyp : Names.Id.t -> 'a Proofview.Goal.t -> EConstr.named_declaration
val pf_get_hyp_typ : Names.Id.t -> 'a Proofview.Goal.t -> EConstr.types
val pf_get_type_of : 'a Proofview.Goal.t -> EConstr.constr -> EConstr.types
val pf_global : Names.Id.t -> 'a Proofview.Goal.t -> Globnames.global_reference