diff options
Diffstat (limited to 'plugins/firstorder')
-rw-r--r-- | plugins/firstorder/instances.ml | 7 | ||||
-rw-r--r-- | plugins/firstorder/rules.ml | 4 |
2 files changed, 7 insertions, 4 deletions
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 797f43f2a..0bc40136c 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -22,6 +22,7 @@ open Formula open Sequent open Names open Misctypes +open Sigma.Notations open Context.Rel.Declaration let compare_instance inst1 inst2= @@ -117,8 +118,10 @@ let mk_open_instance id idc gl m t= let rec aux n avoid env evmap decls = 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 = LocalAssum (Name nid,c) in + 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 = 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 diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index b0e8f7d25..c05015c53 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -212,6 +212,6 @@ let defined_connectives=lazy let normalize_evaluables= onAllHypsAndConcl (function - None->unfold_in_concl (Lazy.force defined_connectives) + None-> Proofview.V82.of_tactic (unfold_in_concl (Lazy.force defined_connectives)) | Some id -> - unfold_in_hyp (Lazy.force defined_connectives) (id,InHypTypeOnly)) + Proofview.V82.of_tactic (unfold_in_hyp (Lazy.force defined_connectives) (id,InHypTypeOnly))) |