diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/extraction/extraction.ml | 17 | ||||
| -rw-r--r-- | plugins/extraction/ocaml.ml | 6 |
2 files changed, 17 insertions, 6 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index a0e61c3b3f..a1a2c9db25 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -118,12 +118,27 @@ let _ = Hook.set type_scheme_nb_args_hook type_scheme_nb_args (*s [type_sign_vl] does the same, plus a type var list. *) +(* When generating type variables, we avoid any ' in their names + (otherwise this may cause a lexer conflict in ocaml with 'a'). + We also get rid of unicode characters. Anyway, since type variables + are local, the created name is just a matter of taste... + See also Bug #3227 *) + +let make_typvar n vl = + let id = id_of_name n in + let id' = + let s = Id.to_string id in + if not (String.contains s '\'') && Unicode.is_basic_ascii s then id + else id_of_name Anonymous + in + next_ident_away id' vl + let rec type_sign_vl env c = match kind_of_term (whd_betadeltaiota env none c) with | Prod (n,t,d) -> let s,vl = type_sign_vl (push_rel_assum (n,t) env) d in if not (is_info_scheme env t) then Kill Kother::s, vl - else Keep::s, (next_ident_away (id_of_name n) vl) :: vl + else Keep::s, (make_typvar n vl) :: vl | _ -> [],[] let rec nb_default_params env c = diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index d762358970..ef81d03228 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -23,11 +23,7 @@ open Common (*s Some utility functions. *) -let pp_tvar id = - let s = Id.to_string id in - if String.length s < 2 || s.[1] != '\'' - then str ("'"^s) - else str ("' "^s) +let pp_tvar id = str ("'" ^ Id.to_string id) let pp_abst = function | [] -> mt () |