aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/firstorder/instances.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/firstorder/instances.ml')
-rw-r--r--plugins/firstorder/instances.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 076107450..6fd934654 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -118,7 +118,7 @@ let mk_open_instance id idc gl m t=
let nid=(fresh_id avoid var_id gl) in
(Name nid,None,dummy_constr)::(aux (n-1) (nid::avoid)) in
let nt=it_mkLambda_or_LetIn revt (aux m []) in
- let rawt=Detyping.detype false [] [] nt in
+ let rawt=Detyping.detype false [] [] evmap nt in
let rec raux n t=
if Int.equal n 0 then t else
match t with