From 4662a2c92ecfdfb383f504f8c230b6d2f2bb58fc Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 23 Oct 2014 20:47:29 +0200
Subject: Fixing order of hypothesis in goal hypotheses compaction for coqtop.

---
 pretyping/termops.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'pretyping/termops.mli')

diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index cbb9fb4ebf..cafb6dc10a 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -216,6 +216,7 @@ val fold_named_context_both_sides :
     named_context -> init:'a -> 'a
 val mem_named_context : Id.t -> named_context -> bool
 val compact_named_context : named_context -> named_list_context
+val compact_named_context_reverse : named_context -> named_list_context
 
 val clear_named_body : Id.t -> env -> env
 
-- 
cgit v1.2.3