diff options
| author | Hugo Herbelin | 2015-12-02 12:10:53 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-02 18:34:11 +0100 |
| commit | 6ab4479dfa0f9b8fd4df4342fdfdab6c25b62fb7 (patch) | |
| tree | 65ccc8e483adcd60bf1efd3bc3992d045ad90def /kernel/nativecode.ml | |
| parent | cc153dbbe45d5cf7f6ebfef6010adcc4f5bb568c (diff) | |
Improving syntax of pat/constr introduction pattern so that
pat/c1/.../cn behaves as intro H; apply c1, ... , cn in H as pat.
Open to other suggestions of syntax though.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions