Skip to content
Snippets Groups Projects
Select Git revision
  • gen-efeed
  • master default protected
  • basic-dune
  • mode-equiv
  • fix-finite-countable
  • eta-expand-list
  • map-lemmas
  • add-dune
  • drop-gmultiset_simple_set
  • make-countables-defined
  • notc-search
  • options
  • coq-stdpp-1.2.0
  • coq-stdpp-1.1.0
  • coq-stdpp-1.0.0
15 results

stdpp

  • Clone with SSH
  • Clone with HTTPS
    • Forked from Iris / stdpp
    Source project has a limited visibility.
    Paolo G. Giarrusso's avatar
    Generalize (e)feed pose proof to intro patterns
    Paolo G. Giarrusso authored 
    This appears a simple oversight, since `pose proof` takes an intro pattern
anyway; `feed inversion` and `feed destruct` already take intro patterns, and
I've been using the generalized `efeed pose proof` for a while.
    d1ed4016
    History
    Paolo G. Giarrusso's avatar d1ed4016
    History
    Name Last commit Last update