diff options
Diffstat (limited to 'proofs/pfedit.ml')
| -rw-r--r-- | proofs/pfedit.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index d8609ed80..c07db32b7 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -176,7 +176,7 @@ let solve_by_implicit_tactic env sigma (evk,args) = match (!implicit_tactic, snd (evar_source evk sigma)) with | Some tac, (Evar_kinds.ImplicitArg _ | Evar_kinds.QuestionMark _) when - Sign.named_context_equal (Environ.named_context_of_val evi.evar_hyps) + Context.named_context_equal (Environ.named_context_of_val evi.evar_hyps) (Environ.named_context env) -> (try build_by_tactic env evi.evar_concl (tclCOMPLETE tac) with e when Logic.catchable_exception e -> raise Exit) |