diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2016-02-15 19:11:42 +0100 |
|---|---|---|
| committer | Matej Kosik <m4tej.kosik@gmail.com> | 2016-02-15 19:11:42 +0100 |
| commit | 97d6583a0b9a65080639fb02deba4200f6276ce6 (patch) | |
| tree | 7e3407649be5fc1f9d47c891b0591ffd4e468468 /plugins/firstorder/instances.ml | |
| parent | 5180ab68819f10949cd41a2458bff877b3ec3204 (diff) | |
| parent | 4f041384cb27f0d24fa14b272884b4b7f69cacbe (diff) | |
merging conflicts with the original "trunk__CLEANUP__Context__2" branch
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 fcbad46d4..0bc40136c 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -23,6 +23,7 @@ open Sequent open Names open Misctypes open Sigma.Notations +open Context.Rel.Declaration let compare_instance inst1 inst2= match inst1,inst2 with @@ -120,7 +121,7 @@ let mk_open_instance id idc gl m t= let evmap = Sigma.Unsafe.of_evar_map evmap in let Sigma ((c, _), evmap, _) = Evarutil.new_type_evar env evmap Evd.univ_flexible in let evmap = Sigma.to_evar_map evmap 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 |