diff options
| author | Pierre-Marie Pédrot | 2019-08-16 01:34:22 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-08-16 01:34:22 +0200 |
| commit | d72acd6f1a5abb8066b6922e5e972fa17b215591 (patch) | |
| tree | 18506c8f48be3f52f6a2746e62a714d2a0bd1a14 /kernel/declareops.ml | |
| parent | 09002e0c20cf4da9cbb1e27146ae1fdd205b304a (diff) | |
| parent | 167d062c47f389340d5c50d022571524b2746a51 (diff) | |
Merge PR #10457: Make rewrite use the registered elimination schemes
Reviewed-by: gares
Reviewed-by: ppedrot
Diffstat (limited to 'kernel/declareops.ml')
0 files changed, 0 insertions, 0 deletions