diff options
Diffstat (limited to 'engine/evarutil.ml')
| -rw-r--r-- | engine/evarutil.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 8202cc05c..374fdce72 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -11,11 +11,11 @@ open Util open Names open Term open Constr -open Termops -open Namegen open Pre_env open Environ open Evd +open Termops +open Namegen module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration @@ -54,7 +54,7 @@ let new_global evd x = (* flush_and_check_evars fails if an existential is undefined *) -exception Uninstantiated_evar of existential_key +exception Uninstantiated_evar of Evar.t let rec flush_and_check_evars sigma c = match kind c with @@ -199,9 +199,10 @@ let whd_head_evar sigma c = let meta_counter_summary_name = "meta counter" (* Generator of metavariables *) -let new_meta = - let meta_ctr = Summary.ref 0 ~name:meta_counter_summary_name in - fun () -> incr meta_ctr; !meta_ctr +let meta_ctr, meta_counter_summary_tag = + Summary.ref_tag 0 ~name:meta_counter_summary_name + +let new_meta () = incr meta_ctr; !meta_ctr let mk_new_meta () = EConstr.mkMeta(new_meta()) |