removed vernaculars with side effects II

Author: ahrens

PROP_untyped/ex_ulcbeta.v

@@ -7,7 +7,7 @@ Unset Strict Implicit.
 Unset Automatic Introduction.
 Unset Transparent Obligations.
 
-Check INITIAL_INEQ_REP.
+(* Check INITIAL_INEQ_REP. *)
 
 Inductive Lambda_index := ABS | APP.
 

PROP_untyped/prop_arities_initial.v

@@ -277,7 +277,6 @@ Proof.
   rew (retakl P).
 Qed.
 
-Print Assumptions sub_struct.
 
 Definition subst_module_mor (P : REP S) := Build_RModule_Hom (sub_struct P).
 
@@ -1013,4 +1012,4 @@ Program Instance INITIAL_INEQ_REP : Initial INEQ_REP := {
 End subcat.
 End S_Mods_and_Eqs.
 
-Print Assumptions INITIAL_INEQ_REP.
+(* Print Assumptions INITIAL_INEQ_REP. *)

RPCF/RPCF_INIT.v

@@ -174,4 +174,4 @@ Program Instance PCF_initial : Initial REP := {
   InitMorUnique R := @initR_unique R
 }.
 
-Print Assumptions PCF_initial.
+(* Print Assumptions PCF_initial. *)

RPCF/RPCF_rep_cat.v

@@ -248,7 +248,5 @@ Proof.
   auto.
 Qed.
 
-Print Assumptions REP_s.
-
 Canonical Structure REP : Cat := Build_Cat REP_s.
 

RPCF/RPCF_syntax_init.v

@@ -255,11 +255,6 @@ Proof.
       auto.
 Qed.
 
-Print nat.
-Check IPO.
-Check SM_ind.
-
-
 
 Lemma init_subst V t (y : PCF V t) W (f : IDelta _ V ---> PCFE W):
       init (y >>= f) =