aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/himsg.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-03-20 20:11:50 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-03-20 20:38:41 +0100
commite98d7276f52c4b67bf05a80a6b44f334966f82fd (patch)
treee85396003f974d5eaa8f84722c0ca3f050990da1 /toplevel/himsg.ml
parent08c31f46aa05098e1a97d9144599c1e5072b7fc3 (diff)
Splitting Evarutil in two distinct files.
Some parts of Evarutils were related to the management of evars under constraints. We put them in the Evardefine file.
Diffstat (limited to 'toplevel/himsg.ml')
-rw-r--r--toplevel/himsg.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 4ee1537c2..31730865f 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -779,7 +779,7 @@ let explain_unsatisfiable_constraints env sigma constr comp =
explain_typeclass_resolution env sigma info k ++ fnl () ++ cstr
let explain_pretype_error env sigma err =
- let env = Evarutil.env_nf_betaiotaevar sigma env in
+ let env = Evardefine.env_nf_betaiotaevar sigma env in
let env = make_all_name_different env in
match err with
| CantFindCaseType c -> explain_cant_find_case_type env sigma c