From 91d78c590b35c9edcf9f68c408ba82090f68e156 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Fri, 5 May 2017 12:59:41 +0200
Subject: Adapted to EConstr.

---
 printing/printer.ml     | 12 ++++++------
 vernac/vernacentries.ml |  9 ---------
 2 files changed, 6 insertions(+), 15 deletions(-)

diff --git a/printing/printer.ml b/printing/printer.ml
index 0e31a4a042..997d866f92 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -359,14 +359,14 @@ let rec should_compact env sigma typ =
     match kind_of_term typ with
     | Rel _ | Var _ | Sort _ | Const _ | Ind _ -> true
     | App (c,args) ->
-       let _,type_of_c = Typing.type_of env sigma c in
-       let _,type_of_typ = Typing.type_of env sigma typ in
-       not (is_Prop type_of_typ)
+       let _,type_of_c = Typing.type_of env sigma (EConstr.of_constr c) in
+       let _,type_of_typ = Typing.type_of env sigma (EConstr.of_constr typ) in
+       not (is_Prop (EConstr.to_constr sigma type_of_typ))
        && (* These two more tests detect rare cases of non-Prop-sorted
              dependent hypothesis:  *)
-       let lnamedtyp , _ = decompose_prod type_of_c in
+       let lnamedtyp , _ = EConstr.decompose_prod sigma type_of_c in
        (* c has a non dependent type *)
-       List.for_all (fun (_,typarg) -> isSort typarg) lnamedtyp
+       List.for_all (fun (_,typarg) -> EConstr.isSort sigma typarg) lnamedtyp
        && (* and real arguments are recursively elligible to compaction. *)
        Array.for_all (should_compact env sigma) args
     | _ -> false
@@ -389,7 +389,7 @@ let rec bld_sign_env env sigma ctxt pps =
 and bld_sign_env_id env sigma ctxt pps is_start =
   match ctxt with
   | [] -> pps,ctxt
-  | CompactedDecl.LocalAssum(ids,typ) as d :: ctxt' when should_compact env sigma typ ->
+ | CompactedDecl.LocalAssum(ids,typ) as d :: ctxt' when should_compact env sigma typ ->
     let pidt = pr_var_list_decl env sigma d in
     let pps' = pps ++ (if not is_start then brk (3,0) else (mt ())) ++ pidt in
     bld_sign_env_id env sigma ctxt' pps' false
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 40cd1a29c9..d4e6af9959 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1411,15 +1411,6 @@ let _ =
       optread  = (fun _ -> None);
       optwrite = (fun _ -> ()) }
 
-let _ =
-  declare_int_option
-    { optsync  = false;
-      optdepr  = false;
-      optname  = "the hypotheses limit";
-      optkey   = ["Hyps";"Limit"];
-      optread  = Flags.print_hyps_limit;
-      optwrite = Flags.set_print_hyps_limit }
-
 let _ =
   declare_bool_option
     { optsync  = true;
-- 
cgit v1.2.3