diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-12-12 11:16:31 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-12 11:16:31 +0100 |
| commit | 3200d6a890dfea363a6f39b856023b6a1c1dae5c (patch) | |
| tree | 189089a1c29139172a47516bf0f2b85108abd973 /engine | |
| parent | 3a56a7f7ec35286360fef5a661634a86c5a13daf (diff) | |
| parent | 5676b113920fb48d4898817d6c0ce3353b06107f (diff) | |
Merge PR #6275: [summary] Allow typed projections from global state.
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/evarutil.ml | 7 | ||||
| -rw-r--r-- | engine/evarutil.mli | 2 | ||||
| -rw-r--r-- | engine/evd.ml | 5 | ||||
| -rw-r--r-- | engine/evd.mli | 2 |
4 files changed, 8 insertions, 8 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 907f1b1ac..3445b744a 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -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()) diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 5fd4634d6..9d0b973a7 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -236,7 +236,7 @@ val evd_comb2 : (evar_map -> 'b -> 'c -> evar_map * 'a) -> evar_map ref -> 'b -> val subterm_source : Evar.t -> Evar_kinds.t Loc.located -> Evar_kinds.t Loc.located -val meta_counter_summary_name : string +val meta_counter_summary_tag : int Summary.Dyn.tag (** Deprecated *) type type_constraint = types option diff --git a/engine/evd.ml b/engine/evd.ml index 45d2a8b08..e33c851f6 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -466,9 +466,8 @@ let add d e i = add_with_name d e i let evar_counter_summary_name = "evar counter" (* Generator of existential names *) -let new_untyped_evar = - let evar_ctr = Summary.ref 0 ~name:evar_counter_summary_name in - fun () -> incr evar_ctr; Evar.unsafe_of_int !evar_ctr +let evar_ctr, evar_counter_summary_tag = Summary.ref_tag 0 ~name:evar_counter_summary_name +let new_untyped_evar () = incr evar_ctr; Evar.unsafe_of_int !evar_ctr let new_evar evd ?name evi = let evk = new_untyped_evar () in diff --git a/engine/evd.mli b/engine/evd.mli index 636bd1be1..b28ce2a62 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -613,7 +613,7 @@ type unsolvability_explanation = SeveralInstancesFound of int (* This stuff is internal and should not be used. Currently a hack in the STM relies on it. *) -val evar_counter_summary_name : string +val evar_counter_summary_tag : int Summary.Dyn.tag (** {5 Deprecated functions} *) val create_evar_defs : evar_map -> evar_map |