diff options
| author | Maxime Dénès | 2020-09-02 12:32:29 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2020-09-07 20:47:42 +0200 |
| commit | fbe0ea439ed3cf2ad933bd6094a36b5cebc5bd19 (patch) | |
| tree | b806f117eba3cc992b0775bbe14e1562399dd40c | |
| parent | b6dabf6aa5b96cfa3c11038316399f0797d734ac (diff) | |
Circumvent revealed bug of evar resolution for fixpoint
This is to be removed once #12920 is merged.
| -rw-r--r-- | vernac/comFixpoint.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 0f34adf1c7..564d24c1ea 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -247,6 +247,7 @@ let interp_fixpoint ?(check_recursivity=true) ~cofix l : (EConstr.rel_context * Impargs.manual_implicits * int option) list) = let (env,_,pl,evd),fix,info = interp_recursive ~program_mode:false ~cofix l in if check_recursivity then check_recursive true env evd fix; + let evd = Pretyping.(solve_remaining_evars all_no_fail_flags env evd) in let uctx,fix = ground_fixpoint env evd fix in (fix,pl,uctx,info) |