From 89eaab788fafcadaf5fe5fca8100bddd54675395 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 23 Oct 2014 18:34:06 +0200
Subject: Fixing order of declarations in the function which compacts variables
 of same type in a context.

---
 pretyping/termops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index a1f1f52ff3..ee60f60c0e 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -948,7 +948,7 @@ let compact_named_context sign =
        if Option.equal Constr.equal c1 c2 && Constr.equal t1 t2
        then (i1::l2,c2,t2)::q
        else ([i1],c1,t1)::l
-  in Context.fold_named_context_reverse compact ~init:[] sign
+  in List.rev (Context.fold_named_context_reverse compact ~init:[] sign)
 
 let clear_named_body id env =
   let aux _ = function
-- 
cgit v1.2.3