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 /plugins | |
| 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 'plugins')
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 921dce4689..ff6dd8f75a 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -357,7 +357,7 @@ let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_ ppdebug(lazy Pp.(str"pirrel_rewrite: proof term: " ++ pr_econstr_env env sigma proof)); ppdebug(lazy Pp.(str"pirrel_rewrite of type: " ++ pr_econstr_env env sigma proof_ty)); try refine_with - ~first_goes_last:(not !ssroldreworder) ~with_evars:under (sigma, proof) gl + ~first_goes_last:(not !ssroldreworder || under) ~with_evars:under (sigma, proof) gl with _ -> (* we generate a msg like: "Unable to find an instance for the variable" *) let hd_ty, miss = match EConstr.kind sigma c with |