diff options
author | 2019-02-05 11:24:23 -0500 | |
---|---|---|
committer | 2019-02-05 11:24:23 -0500 | |
commit | 6e23288ca437e8a2761a93da1c09ec52460606aa (patch) | |
tree | 81d822db80f9724b48f036e725379674412a928f /vernac/comInductive.ml | |
parent | 956960a408a4fe67c7508bf3101d469b6465686d (diff) |
Disable ssrmatching and ssreflect
The nonfree file in ssrmatching I removed in
cf916fd97fbac51af6fa68ec2704da2a28ef9ede turns out to be important to
the build process, and I can’t figure out how to replicate its effects
without including the file itself. Disable ssrmatching and ssreflect
again until the license situation gets resolved.
Diffstat (limited to 'vernac/comInductive.ml')
0 files changed, 0 insertions, 0 deletions