diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-17 15:10:57 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-17 15:10:57 +0100 |
| commit | e3e8a4065047e254f5f5c2747227db75f01b7bed (patch) | |
| tree | c7505db28eee92bc1855b6ee0cf275381b4aa106 /plugins/setoid_ring/g_newring.ml4 | |
| parent | 22c1e7c3f1d86902b1abf2d887e0e9bf93ddb60d (diff) | |
| parent | 2537e84ba9fa92db6cfd3d7f5e400b1716c31246 (diff) | |
Removing the default value mechanism for generic arguments.
There was a complicated dedicated code in grammar/ to decide whether a generic argument
parsed the empty string. We now only rely on a dynamic decision. This should not affect
efficiency, as it is only made once by declaration of ML tactics.
Diffstat (limited to 'plugins/setoid_ring/g_newring.ml4')
0 files changed, 0 insertions, 0 deletions