diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-23 04:08:30 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-26 15:42:46 +0200 |
| commit | e2a81df304c198cc2bdd5d1ffa703ed7eaca9d12 (patch) | |
| tree | e38618f0a419d539bb1375334a56fc928a468591 /tactics | |
| parent | bd1a0abf49fe67e7f02dc562d4b81d27ed6f606c (diff) | |
Remove a few useless evar-normalizations in printing code.
Diffstat (limited to 'tactics')
| -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 3fc2fc31b..52475870b 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 |