diff options
Diffstat (limited to 'plugins/firstorder/instances.ml')
| -rw-r--r-- | plugins/firstorder/instances.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index a717cc91e..797f43f2a 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -22,6 +22,7 @@ open Formula open Sequent open Names open Misctypes +open Context.Rel.Declaration let compare_instance inst1 inst2= match inst1,inst2 with @@ -117,7 +118,7 @@ let mk_open_instance id idc gl m t= if Int.equal n 0 then evmap, decls else let nid=(fresh_id avoid var_id gl) in let evmap, (c, _) = Evarutil.new_type_evar env evmap Evd.univ_flexible in - let decl = (Name nid,None,c) in + let decl = LocalAssum (Name nid,c) in aux (n-1) (nid::avoid) (Environ.push_rel decl env) evmap (decl::decls) in let evmap, decls = aux m [] env evmap [] in evmap, decls, revt |