diff options
| author | Emilio Jesus Gallego Arias | 2018-05-22 00:07:26 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-06-12 14:42:28 +0200 |
| commit | 368a25e4ef14512b00f5799e26c3f615bc540201 (patch) | |
| tree | 29602372307ff70f2a7b06f0a27609a73caa5666 /engine/evarutil.ml | |
| parent | 36a98d55576ebdb106a55c3bd682961da8d77dee (diff) | |
[api] Misctypes removal: several moves:
- move_location to proofs/logic.
- intro_pattern_naming to Namegen.
Diffstat (limited to 'engine/evarutil.ml')
| -rw-r--r-- | engine/evarutil.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 648f960354..82be4791fc 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -436,12 +436,12 @@ let new_pure_evar_full evd evi = (evd, evk) let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) sign evd typ = - let default_naming = Misctypes.IntroAnonymous in + let default_naming = IntroAnonymous in let naming = Option.default default_naming naming in let name = match naming with - | Misctypes.IntroAnonymous -> None - | Misctypes.IntroIdentifier id -> Some id - | Misctypes.IntroFresh id -> + | IntroAnonymous -> None + | IntroIdentifier id -> Some id + | IntroFresh id -> let has_name id = try let _ = Evd.evar_key id evd in true with Not_found -> false in let id = Namegen.next_ident_away_from id has_name in Some id |