Commit b8b41bc5 authored by Robbert Krebbers's avatar Robbert Krebbers

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.
parent 535bab6d
......@@ -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
......
......@@ -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.
......
......@@ -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]
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment