diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-04-27 18:45:01 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-04-27 18:45:01 +0200 |
| commit | 9a91a385b2562a0656edf8766f229dc8120b2675 (patch) | |
| tree | a4fd54fedd13150bd30cedd1778634bb2344af9b /pretyping/patternops.ml | |
| parent | 746066172b8ed508886feb20cee239920ca7a4c7 (diff) | |
| parent | e574b4bdd974daa7d2ceecf799762be92fadff44 (diff) | |
Merge PR#587: Fix description of command-line arguments for Add (Rec) LoadPath
Diffstat (limited to 'pretyping/patternops.ml')
0 files changed, 0 insertions, 0 deletions