diff options
Diffstat (limited to 'engine/evd.ml')
| -rw-r--r-- | engine/evd.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index d57ae89dd..e33c851f6 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -401,7 +401,7 @@ let rename evk id (evtoid, idtoev) = | None -> (EvMap.add evk id evtoid, Id.Map.add id evk idtoev) | Some id' -> if Id.Map.mem id idtoev then anomaly (str "Evar name already in use."); - (EvMap.update evk id evtoid (* overwrite old name *), Id.Map.add id evk (Id.Map.remove id' idtoev)) + (EvMap.set evk id evtoid (* overwrite old name *), Id.Map.add id evk (Id.Map.remove id' idtoev)) let reassign_name_defined evk evk' (evtoid, idtoev as names) = let id = try Some (EvMap.find evk evtoid) with Not_found -> None in @@ -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 |