diff options
| author | Erik Martin-Dorel | 2019-02-27 18:53:11 +0100 |
|---|---|---|
| committer | Erik Martin-Dorel | 2019-04-23 12:54:43 +0200 |
| commit | f294fe1684e03f63871864def0f82190da087ebe (patch) | |
| tree | fac3caa917f3ad326e113ebddf92ba90fa3d99a5 /doc/plugin_tutorial/tuto3/src/construction_game.ml | |
| parent | adbb10dc627faa199bc4164b45740f62af8dc3fc (diff) | |
[ssr] under: Fix rewrite goals order when called from under
* "under"-specific behavior:
the order of goals is kept even if one issues
Global Set SsrOldRewriteGoalsOrder.
* href: https://github.com/math-comp/math-comp/blob/mathcomp-1.7.0/mathcomp/ssreflect/ssreflect.v
Diffstat (limited to 'doc/plugin_tutorial/tuto3/src/construction_game.ml')
0 files changed, 0 insertions, 0 deletions