diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-08-01 13:02:18 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-08-01 13:02:18 +0200 |
| commit | a893cd2993acb8da5a17aa57694ded2355e8eaea (patch) | |
| tree | 00f98278bbac7b25924ef5b1a7d4220dd540f491 /tactics/class_tactics.ml | |
| parent | ec0fcba55a6849fa37438809df4783e7c5aa3a89 (diff) | |
| parent | e2a81df304c198cc2bdd5d1ffa703ed7eaca9d12 (diff) | |
Merge PR #919: Remove a few useless evar-normalizations in printing code.
Diffstat (limited to 'tactics/class_tactics.ml')
| -rw-r--r-- | tactics/class_tactics.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 5337565d3..371debede 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1460,7 +1460,6 @@ let is_mandatory p comp evd = (** In case of unsatisfiable constraints, build a nice error message *) let error_unresolvable env comp evd = - let evd = Evarutil.nf_evar_map_undefined evd in let is_part ev = match comp with | None -> true | Some s -> Evar.Set.mem ev s @@ -1474,8 +1473,7 @@ let error_unresolvable env comp evd = else (found, accu) in let (_, ev) = Evd.fold_undefined fold evd (true, None) in - Pretype_errors.unsatisfiable_constraints - (Evarutil.nf_env_evar evd env) evd ev comp + Pretype_errors.unsatisfiable_constraints env evd ev comp (** Check if an evar is concerned by the current resolution attempt, (and in particular is in the current component), and also update |