coq/plugins/Derive, branch master The formal proof system Avoiding introducing yet another convention in naming files. 2015-01-08T18:05:14+00:00 Hugo Herbelin 2015-01-08T17:18:02+00:00 d08532d5344d96d10604760fa44109c9d56e73ce 






Uniformisation of the order of arguments env and sigma.
2014-09-12T08:39:33+00:00

Hugo Herbelin

2014-08-20T20:30:37+00:00

b006f10e7d591417844ffa1f04eeb926d6092d7b












Derive plugin: add some comments.
2014-07-23T15:52:47+00:00

Arnaud Spiwack

2014-07-23T14:33:33+00:00

5a7ab19e91bae5e694f88e0d036f74c7a7790887












Derive plugin: code reorganisation for clarity.
2014-07-23T15:52:47+00:00

Arnaud Spiwack

2014-07-23T14:26:41+00:00

9451d139c901a1e9f5fefdc0eb058cf1e66f983b












Derive plugin: small refactoring.
2014-07-23T15:52:46+00:00

Arnaud Spiwack

2014-07-23T14:11:08+00:00

1ada99f2c367c2b2bad39377c38c4dc6e4b5a04a












Derive plugin: a more general interface.
2014-07-23T15:52:46+00:00

Arnaud Spiwack

2014-07-22T15:55:00+00:00

7e577f93aca95d10584014e1d88dfbf314b74f9f

Instead of forcing the specifying property to be of the form (r spec def), allow any lemma depending on def.





Instead of forcing the specifying property to be of the form (r spec def), allow any lemma depending on def.







Proofs now take and return an evar_universe_context, simplifying interfaces
2014-06-18T15:21:21+00:00

Matthieu Sozeau

2014-06-18T15:16:59+00:00

23f4804b50307766219392229757e75da9aa41d9

and avoiding explicit substitutions and merging of contexts, e.g. in obligations.ml.
The context produced by typechecking a statement is passed in the proof, allowing the
universe name context to be correctly folded as well. Mainly an API cleanup.





and avoiding explicit substitutions and merging of contexts, e.g. in obligations.ml.
The context produced by typechecking a statement is passed in the proof, allowing the
universe name context to be correctly folded as well. Mainly an API cleanup.







poly: remove unused attribute to STM nodes and vernac classificaiton
2014-05-15T08:52:53+00:00

Enrico Tassi

2014-05-15T08:50:05+00:00

49542cf365715e27811cc15d99565046d8754c20












Fix derive plugin to properly treat universes
2014-05-06T07:59:00+00:00

Matthieu Sozeau

2014-04-09T13:31:39+00:00

99c8b69f5ef0f92b26ec23be06743312846f5af3












Initial work on reintroducing old-style polymorphism for compatibility (the stdlib does not compile entirely).
2014-05-06T07:58:54+00:00

Matthieu Sozeau

2013-10-28T13:08:46+00:00

001ff72b2c17fb7b2fcaefa2555c115f0d909a03