Backporting the legacy stream theory from Coq.

coq-community / math-classes

A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia]

https://math-classes.github.io

MIT License

162 stars 43 forks source link

Backporting the legacy stream theory from Coq. #52

Closed ppedrot closed 6 years ago

ppedrot commented 6 years ago

This PR is a backward compatible fix for PR coq/coq#7536. We simply copy the old Stream library from Coq to math-classes. Note that when the Coq PR is merged, some care will have to be taken to rewrite math-classes with a proper negative stream implementation.

spitters commented 6 years ago

Thanks! make[2]: *** No rule to make target theory/Streams.vo', needed byinterfaces/canonical_names.vo'. Stop.

Could you add that to this PR?

ppedrot commented 6 years ago

@spitters I think this is a bug in the build system. You should call configure before lauching the build system... We've fixed that on Coq side already.

spitters commented 6 years ago

Thanks. Could you be more explicit?

Should we change l15 of https://github.com/math-classes/math-classes/blob/master/.travis.yml to script: configure && make ?

ppedrot commented 6 years ago

Should be ./configure.sh && make but yes.