diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-10-10 11:39:40 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-10-16 10:23:29 +0200 |
| commit | be66bcaa51298b302f798128fbf3215c123c57d8 (patch) | |
| tree | bff23a4a786c9703b5f5c7ac0054f448fddb7c0e /pretyping/evd.ml | |
| parent | aadc5aee48fc0ddb01e3ae0b743a0b66edf2ff4a (diff) | |
Evd: remove/update obsolete comments.
Diffstat (limited to 'pretyping/evd.ml')
| -rw-r--r-- | pretyping/evd.ml | 9 |
1 files changed, 1 insertions, 8 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index f85970a1f..0964baeff 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -220,13 +220,6 @@ let evar_ident_info evi = let env = reset_with_named_context evi.evar_hyps (Global.env()) in Namegen.id_of_name_using_hdchar env evi.evar_concl Anonymous -(* spiwack: Revised hierarchy : - - Evar.Map ( Maps of existential_keys ) - - EvarInfoMap ( .t = evar_info Evar.Map.t * evar_info Evar.Map ) - - EvarMap ( .t = EvarInfoMap.t * sort_constraints ) - - evar_map (exported) -*) - (* This exception is raised by *.existential_value *) exception NotInstantiatedEvar @@ -589,7 +582,7 @@ type evar_map = { evar_names : Id.t EvMap.t * existential_key Idmap.t; } -(*** Lifting primitive from EvarMap. ***) +(*** Lifting primitive from Evar.Map. ***) (* HH: The progress tactical now uses this function. *) let progress_evar_map d1 d2 = |