From 2ded4c25e532c5dfca0483c211653768ebed01a7 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 13 Jun 2019 15:39:43 +0200
Subject: UIP in SProp

---
 engine/evd.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'engine/evd.mli')

diff --git a/engine/evd.mli b/engine/evd.mli
index d9b7bd76e7..679173ca72 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -732,6 +732,8 @@ module MiniEConstr : sig
     (Constr.t, Constr.types) Context.Named.Declaration.pt
   val unsafe_to_rel_decl : (t, t) Context.Rel.Declaration.pt ->
     (Constr.t, Constr.types) Context.Rel.Declaration.pt
+  val of_case_invert : (constr,Univ.Instance.t) case_invert -> (econstr,EInstance.t) case_invert
+  val unsafe_to_case_invert : (econstr,EInstance.t) case_invert -> (constr,Univ.Instance.t) case_invert
   val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt ->
     (t, t) Context.Rel.Declaration.pt
   val to_rel_decl : evar_map -> (t, t) Context.Rel.Declaration.pt ->
-- 
cgit v1.2.3