aboutsummaryrefslogtreecommitdiff
path: root/dev/include
diff options
context:
space:
mode:
authorErik Martin-Dorel2019-02-27 18:53:11 +0100
committerErik Martin-Dorel2019-04-23 12:54:43 +0200
commitf294fe1684e03f63871864def0f82190da087ebe (patch)
treefac3caa917f3ad326e113ebddf92ba90fa3d99a5 /dev/include
parentadbb10dc627faa199bc4164b45740f62af8dc3fc (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 'dev/include')
0 files changed, 0 insertions, 0 deletions