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 80576212f..0aafafde9 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -124,7 +124,7 @@ let mk_open_instance id idc gl m t=
match t with
GLambda(loc,name,k,_,t0)->
let t1=raux (n-1) t0 in
- GLambda(loc,name,k,GHole (Loc.ghost,Evar_kinds.BinderType name,None),t1)
+ GLambda(loc,name,k,GHole (Loc.ghost,Evar_kinds.BinderType name,Misctypes.IntroAnonymous,None),t1)
| _-> anomaly (Pp.str "can't happen") in
let ntt=try
fst (Pretyping.understand env evmap (raux m rawt))(*FIXME*)