From 87539cd9f8ce912e5e084dfbed5fa366555b6006 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Wed, 24 May 2017 18:04:10 +0200
Subject: romega: takes advantage of context variables with body

 When a context variable x is of the form "x := body : Z",
 romega is now made aware of this body. Technically, we reify an equation
 x = body, and push a corresponding (eq_refl x) as argument of the
 final do_omega.

 See also the previous commit adding this same feature to omega
 (fixing bug 142).
---
 API/API.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'API/API.mli')

diff --git a/API/API.mli b/API/API.mli
index 3ed326ff0e..4b6c755a6d 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
-- 
cgit v1.2.3