diff options
| author | Pierre-Marie Pédrot | 2019-04-11 12:11:07 +0200 |
|---|---|---|
| committer | GitHub | 2019-04-11 12:11:07 +0200 |
| commit | 5131640774d0256a390790b5becc864935585ce8 (patch) | |
| tree | f5903e140972be1dfc5052fc74e51b9c21feb813 /doc/plugin_tutorial/tuto2/src/dune | |
| parent | d47892548aebfb6640a8721ee1ec3493bfd3ce2a (diff) | |
| parent | 5463cfbaaaab2e696c4bbeeeb38f03ca79d5949e (diff) | |
Merge pull request coq/ltac2#119 from maximedenes/pretyping-rm-global
Adapt to Coq's PR #9909
Diffstat (limited to 'doc/plugin_tutorial/tuto2/src/dune')
0 files changed, 0 insertions, 0 deletions