From b8b41bc50b18372598136338439266e2c8e95da5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Fri, 19 Aug 2016 14:15:32 +0200
Subject: [PATCH] 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.
---
theories/base.v | 4 +++-
theories/pretty.v | 6 ++----
theories/tactics.v | 7 +++++++
3 files changed, 12 insertions(+), 5 deletions(-)
diff --git a/theories/base.v b/theories/base.v
index 370621e..1d35448 100644
--- a/theories/base.v
+++ b/theories/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
diff --git a/theories/pretty.v b/theories/pretty.v
index 05636db..58fd383 100644
--- a/theories/pretty.v
+++ b/theories/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.
diff --git a/theories/tactics.v b/theories/tactics.v
index ce5a3b9..b1b9224 100644
--- a/theories/tactics.v
+++ b/theories/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]
--
2.24.1