1 files changed, 41 insertions, 12 deletions

diff --git a/engine/termops.ml b/engine/termops.ml
index 697b9a5f15..2f4c5e2049 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 CompactedDecl = Context.Compacted.Declaration
 
 (* Sorts and sort family *)
 
@@ -100,6 +101,7 @@ let term_printer = ref (fun _ -> pr_constr)
 let print_constr_env t = !term_printer t
 let print_constr t = !term_printer (Global.env()) t
 let set_print_constr f = term_printer := f
+let () = Hook.set Evd.print_constr_hook (fun env c -> !term_printer env c)
 
 let pr_var_decl env decl =
   let open NamedDecl in
@@ -607,7 +609,10 @@ let vars_of_global_reference env gr =
    [m] is appropriately lifted through abstractions of [t] *)
 
 let dependent_main noevar univs m t =
-  let eqc x y = if univs then fst (Universes.eq_constr_universes x y) else eq_constr_nounivs x y in
+  let eqc x y =
+    if univs then not (Option.is_empty (Universes.eq_constr_universes x y))
+    else eq_constr_nounivs x y
+  in
   let rec deprec m t =
     if eqc m t then
       raise Occur
@@ -673,6 +678,21 @@ let rec subst_meta bl c =
     | Meta i -> (try Int.List.assoc i bl with Not_found -> c)
     | _ -> map_constr (subst_meta bl) c
 
+let rec strip_outer_cast c = match kind_of_term c with
+  | Cast (c,_,_) -> strip_outer_cast c
+  | _ -> c
+
+(* flattens application lists throwing casts in-between *)
+let collapse_appl c = match kind_of_term c with
+  | App (f,cl) ->
+      let rec collapse_rec f cl2 =
+        match kind_of_term (strip_outer_cast f) with
+        | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
+        | _ -> mkApp (f,cl2)
+      in
+      collapse_rec f cl
+  | _ -> c
+
 (* First utilities for avoiding telescope computation for subst_term *)
 
 let prefix_application eq_fun (k,c) (t : constr) =
@@ -982,18 +1002,27 @@ let fold_named_context_both_sides f l ~init = List.fold_right_and_left f l init
 let mem_named_context_val id ctxt =
   try ignore(Environ.lookup_named_val id ctxt); true with Not_found -> false
 
-let compact_named_context_reverse sign =
+let compact_named_context sign =
   let compact l decl =
-    let (i1,c1,t1) = NamedDecl.to_tuple decl 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
-
-let compact_named_context sign = List.rev (compact_named_context_reverse sign)
+    match decl, l with
+    | NamedDecl.LocalAssum (i,t), [] ->
+       [CompactedDecl.LocalAssum ([i],t)]
+    | NamedDecl.LocalDef (i,c,t), [] ->
+       [CompactedDecl.LocalDef ([i],c,t)]
+    | NamedDecl.LocalAssum (i1,t1), CompactedDecl.LocalAssum (li,t2) :: q ->
+       if Constr.equal t1 t2
+       then CompactedDecl.LocalAssum (i1::li, t2) :: q
+       else CompactedDecl.LocalAssum ([i1],t1) :: CompactedDecl.LocalAssum (li,t2) :: q
+    | NamedDecl.LocalDef (i1,c1,t1), CompactedDecl.LocalDef (li,c2,t2) :: q ->
+       if Constr.equal c1 c2 && Constr.equal t1 t2
+       then CompactedDecl.LocalDef (i1::li, c2, t2) :: q
+       else CompactedDecl.LocalDef ([i1],c1,t1) :: CompactedDecl.LocalDef (li,c2,t2) :: q
+    | NamedDecl.LocalAssum (i,t), q ->
+       CompactedDecl.LocalAssum ([i],t) :: q
+    | NamedDecl.LocalDef (i,c,t), q ->
+       CompactedDecl.LocalDef ([i],c,t) :: q
+  in
+  sign |> Context.Named.fold_inside compact ~init:[] |> List.rev
 
 let clear_named_body id env =
   let open NamedDecl in