diff options
| author | Hugo Herbelin | 2015-05-13 10:31:22 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-05-13 10:31:45 +0200 |
| commit | c5d9f483a48265941720afafd5952a917d80204b (patch) | |
| tree | b4704a036f1db09641b91f4c16bca7c00ee3ec91 /kernel/nativecode.ml | |
| parent | 574b4096517b4ac9189c2226e1cd75745e788db0 (diff) | |
Documenting Set Regular Subst Tactic (though unsure this is worth the
level of details, and this option should certainly disappear
eventually).
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions