aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-11-25 17:09:21 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-02-20 10:03:07 +0100
commit8f93f9a2df6e17386f46f79b2a7eda4104d0a94e (patch)
tree77c1c1fdc54a7c96d197c71caa2ab75fc3041928 /test-suite/output
parent69822345c198aa6bf51354f6b84c7fd5d401bc9c (diff)
Notations: A step in cleaning constr_entry_key.
- Avoid dummy use of unit - Do not decide as early as parsing the default level for pattern - Prepare to further extensions
Diffstat (limited to 'test-suite/output')
0 files changed, 0 insertions, 0 deletions