diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-03-05 20:32:10 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-03-05 20:54:45 +0100 |
| commit | 4177c2380fcd92bca07c97993c21ffd230408eca (patch) | |
| tree | 0ba9a8dbba9c6b2a658ad9dcda53bda68ec20838 /grammar | |
| parent | e967151588b48911caf5bc687d87b586e95e0513 (diff) | |
Adding a canary library. This canary is imperfect. It allows serialization
(hopefully), and forbids generic equality. Still, it allows generic hash.
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/grammar.mllib | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib index c2f39deed..338d44fbf 100644 --- a/grammar/grammar.mllib +++ b/grammar/grammar.mllib @@ -1,6 +1,7 @@ Coq_config Hook +Canary Hashset Hashcons CSet |