From 1297523bffdc3a9fe3e447acc6837be835e86d06 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Mon, 15 Aug 2016 14:14:14 +0200
Subject: CLEANUP: changing the definition of the
 "Context.NamedList.Declaration" type

---
 engine/termops.ml | 31 ++++++++++++++++++++-----------
 1 file changed, 20 insertions(+), 11 deletions(-)

(limited to 'engine')

diff --git a/engine/termops.ml b/engine/termops.ml
index 7afd7a0385..3f36059dd8 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -17,6 +17,7 @@ open Environ
 
 module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
+module NamedListDecl = Context.NamedList.Declaration
 
 (* Sorts and sort family *)
 
@@ -983,17 +984,25 @@ let rec mem_named_context id ctxt =
 
 let compact_named_context_reverse sign =
   let compact l decl =
-    let (i1,c1,t1) = match decl with
-                     | NamedDecl.LocalAssum (i,t) -> i,None,t
-                     | NamedDecl.LocalDef (i,c,t) -> i,Some c,t
-    in
-    match l with
-    | [] -> [[i1],c1,t1]
-    | (l2,c2,t2)::q ->
-       if Option.equal Constr.equal c1 c2 && Constr.equal t1 t2
-       then (i1::l2,c2,t2)::q
-       else ([i1],c1,t1)::l
-  in Context.Named.fold_inside compact ~init:[] sign
+    match decl, l with
+    | NamedDecl.LocalAssum (i,t), [] ->
+       [NamedListDecl.LocalAssum ([i],t)]
+    | NamedDecl.LocalDef (i,c,t), [] ->
+       [NamedListDecl.LocalDef ([i],c,t)]
+    | NamedDecl.LocalAssum (i1,t1), NamedListDecl.LocalAssum (li,t2) :: q ->
+       if Constr.equal t1 t2
+       then NamedListDecl.LocalAssum (i1::li, t2) :: q
+       else NamedListDecl.LocalAssum ([i1],t1) :: NamedListDecl.LocalAssum (li,t2) :: q
+    | NamedDecl.LocalDef (i1,c1,t1), NamedListDecl.LocalDef (li,c2,t2) :: q ->
+       if Constr.equal c1 c2 && Constr.equal t1 t2
+       then NamedListDecl.LocalDef (i1::li, c2, t2) :: q
+       else NamedListDecl.LocalDef ([i1],c1,t1) :: NamedListDecl.LocalDef (li,c2,t2) :: q
+    | NamedDecl.LocalAssum (i,t), q ->
+       NamedListDecl.LocalAssum ([i],t) :: q
+    | NamedDecl.LocalDef (i,c,t), q ->
+       NamedListDecl.LocalDef ([i],c,t) :: q
+  in
+  Context.Named.fold_inside compact ~init:[] sign
 
 let compact_named_context sign = List.rev (compact_named_context_reverse sign)
 
-- 
cgit v1.2.3