diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-01 19:45:01 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-02-15 13:12:13 +0100 |
| commit | 968dfdb15cc11d48783017b2a91147b25c854ad6 (patch) | |
| tree | d619d1ebe51d29e5517c9c0385dc4aefe546edbe /plugins/firstorder/instances.ml | |
| parent | 97e1fccd878190a1fc51a1da45f4c06369c0e3db (diff) | |
Monotonizing the Evarutil module.
Some functions were left in the old paradigm because they are only used by the
unification algorithms, so they are not worthwhile to change for now.
Diffstat (limited to 'plugins/firstorder/instances.ml')
| -rw-r--r-- | plugins/firstorder/instances.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index a717cc91e..fcbad46d4 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 let compare_instance inst1 inst2= match inst1,inst2 with @@ -116,7 +117,9 @@ 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 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 aux (n-1) (nid::avoid) (Environ.push_rel decl env) evmap (decl::decls) in let evmap, decls = aux m [] env evmap [] in |