Import less Program stuff to avoid UIP/fun_ext showing up with coqchk.

There is still the reals stuff, which is caused by importint Psatz (needed
for lia) and eq_rect_eq which is caused by importint Eqdep_dec.

prelude/base.v

@@ -8,7 +8,9 @@ Global Generalizable All Variables.
 Global Set Automatic Coercions Import.
 Global Set Asymmetric Patterns.
 Global Unset Transparent Obligations.
-From Coq Require Export Morphisms RelationClasses List Bool Utf8 Program Setoid.
+From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid.
+Export ListNotations.
+From Coq.Program Require Export Basics Syntax.
 Obligation Tactic := idtac.
 
 (** Throughout this development we use [C_scope] for all general purpose

prelude/pretty.v

@@ -37,8 +37,7 @@ Proof.
   by destruct (decide (0 < x)%N); auto using pretty_N_go_help_irrel.
 Qed.
 Instance pretty_N : Pretty N := λ x, pretty_N_go x ""%string.
-Lemma pretty_N_unfold x :
-  pretty x = pretty_N_go x "".
+Lemma pretty_N_unfold x : pretty x = pretty_N_go x "".
 Proof. done. Qed.
 Instance pretty_N_inj : Inj (@eq N) (=) pretty.
 Proof.
@@ -48,8 +47,7 @@ Proof.
   cut (∀ x y s s', pretty_N_go x s = pretty_N_go y s' →
     String.length s = String.length s' → x = y ∧ s = s').
   { intros help x y Hp.
-    eapply (help x y "" ""); [by rewrite <-!pretty_N_unfold|].
-    eauto. }
+    eapply (help x y "" ""); [by rewrite <-!pretty_N_unfold|done]. }
   assert (∀ x s, ¬String.length (pretty_N_go x s) < String.length s) as help.
   { setoid_rewrite <-Nat.le_ngt.
     intros x; induction (N.lt_wf_0 x) as [x _ IH]; intros s.

prelude/tactics.v

@@ -407,6 +407,13 @@ Tactic Notation "feed" "destruct" constr(H) :=
 Tactic Notation "feed" "destruct" constr(H) "as" simple_intropattern(IP) :=
   feed (fun p => let H':=fresh in pose proof p as H'; destruct H' as IP) H.
 
+(** The block definitions are taken from [Coq.Program.Equality] and can be used
+by tactics to separate their goal from hypotheses they generalize over. *)
+Definition block {A : Type} (a : A) := a.
+
+Ltac block_goal := match goal with [ |- ?T ] => change (block T) end.
+Ltac unblock_goal := unfold block in *.
+
 
 (** The following tactic can be used to add support for patterns to tactic notation:
 It will search for the first subterm of the goal matching [pat], and then call [tac]