diff options
| author | Pierre-Marie Pédrot | 2020-09-09 11:07:52 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-09-09 11:07:52 +0200 |
| commit | 6f12c3e3ccce7028abb492f804d30ba0bef58f06 (patch) | |
| tree | db89fb070eead9bcf14880a9b3d3672b0f5bbf85 /vernac | |
| parent | 215d3013312309d47dae01b66b1781b572d30783 (diff) | |
| parent | fbe0ea439ed3cf2ad933bd6094a36b5cebc5bd19 (diff) | |
Merge PR #7825: [tactics] Refine test for unresolved evars: not reachable from initial evars
Ack-by: JasonGross
Ack-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: gares
Ack-by: jfehrle
Ack-by: maximedenes
Reviewed-by: ppedrot
Diffstat (limited to 'vernac')
| -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) |