General Subobjectclassifier

I am looking for abstract (tac1. tac2. tac3 .... tacn).
Yes, I can rewrite it using ; but this more difficult to maintain (trust
me, I have tried).
Matita has a nice feature where you can step through semicolons. This would
be another solution.

On Thu, Sep 11, 2014 at 5:08 PM, Jason Gross <notifications@github.com>
wrote:

> In theories/ObjectClassifier.v:
>
> > @@ -88,4 +96,48 @@ simpl in p. by path_induction.
> >  Qed.
> >
> >  End FamPow.
> > +
> > +Section Subobjectclassifier.
> > +(** We prove that hProp is the subobject classifier *)
> > +(** In fact, the proof works for general mere predicates on [Type],
> > +not just [IsHProp], truncations and modalities are important examples.*)
> > +Variable A:Type.
> > +Variable isP:Type -> Type.
> > +Variable ishprop_isP: forall I, IsHProp (isP I).
> > +Definition IsPfibered {I} (f:I->A):=forall i, isP (hfiber f i).
> > +Definition PFam := (sig (fun F:Fam A => IsPfibered (pr2 F))).
> > +(* Bug: abstract should accept more than one tactic.
>
> What do you mean? Are you looking for one of
>
> abstract (foo; bar).first [ abstract foo | abstract bar ].abstract first [ foo | bar ].
>
> ?
>
> —
> Reply to this email directly or view it on GitHub
> <https://github.com/HoTT/HoTT/pull/487/files#r17426425>.
>