aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/pretyping.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-11-06 03:23:13 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-02-14 17:25:28 +0100
commitb365304d32db443194b7eaadda63c784814f53f1 (patch)
tree95c09bc42f35a5d49af5aeb16a281105e674a824 /pretyping/pretyping.ml
parentb113f9e1ca88514cd9d94dfe90669a27689b7434 (diff)
Evarconv API using EConstr.
Diffstat (limited to 'pretyping/pretyping.ml')
-rw-r--r--pretyping/pretyping.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index fbba682fc..570f95324 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -626,7 +626,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let fixi = match fixkind with
| GFix (vn,i) -> i
| GCoFix i -> i
- in e_conv env.ExtraEnv.env evdref ftys.(fixi) t
+ in e_conv env.ExtraEnv.env evdref (EConstr.of_constr ftys.(fixi)) (EConstr.of_constr t)
| None -> true
in
(* Note: bodies are not used by push_rec_types, so [||] is safe *)
@@ -732,7 +732,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
match candargs with
| [] -> [], j_val hj
| arg :: args ->
- if e_conv env.ExtraEnv.env evdref (j_val hj) arg then
+ if e_conv env.ExtraEnv.env evdref (EConstr.of_constr (j_val hj)) (EConstr.of_constr arg) then
args, nf_evar !evdref (j_val hj)
else [], j_val hj
in
@@ -1088,7 +1088,7 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function
match valcon with
| None -> tj
| Some v ->
- if e_cumul env.ExtraEnv.env evdref v tj.utj_val then tj
+ if e_cumul env.ExtraEnv.env evdref (EConstr.of_constr v) (EConstr.of_constr tj.utj_val) then tj
else
error_unexpected_type
~loc:(loc_of_glob_constr c) env.ExtraEnv.env !evdref tj.utj_val v