Adapted to EConstr.

2 files changed, 6 insertions, 15 deletions

diff --git a/printing/printer.ml b/printing/printer.ml
index 0e31a4a04..997d866f9 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 40cd1a29c..d4e6af995 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1412,15 +1412,6 @@ let _ =
       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;
       optdepr  = false;