diff options
| author |  jforest <jforest@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-10-31 16:07:59 +0000 |
|---|---|---|
| committer | jforest <jforest@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-10-31 16:07:59 +0000 |
| commit | d214946779d440a2cca8053bd52f35ac748f2823 (patch) | |
| tree | a8cff7322549437eea8a48b3007cbce66364928d /plugins | |
| parent | 1408c0f1ff3c25089c328d3d0a31144de0e718d0 (diff) | |
correcting a little bug in Function
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15947 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 4 | ||||
| -rw-r--r-- | plugins/funind/invfun.ml | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 61390bb1a..593e274fb 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -488,7 +488,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let rt_as_constr = Pretyping.understand Evd.empty env rt in let rt_typ = Typing.type_of env Evd.empty rt_as_constr in let res_raw_type = Detyping.detype false [] (Termops.names_of_rel_context env) rt_typ in - let res = fresh_id args_res.to_avoid "res" in + let res = fresh_id args_res.to_avoid "_res" in let new_avoid = res::args_res.to_avoid in let res_rt = mkGVar res in let new_result = @@ -835,7 +835,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve let is_res id = try - String.sub (string_of_id id) 0 3 = "res" + String.sub (string_of_id id) 0 4 = "_res" with Invalid_argument _ -> false diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index d0ce489a8..517a1ce9c 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -126,7 +126,7 @@ let generate_type g_to_f f graph i = (*i We need to name the vars [res] and [fv] i*) let filter = function (Name id,_,_) -> Some id | (Anonymous,_,_) -> None in let named_ctxt = List.map_filter filter fun_ctxt in - let res_id = Namegen.next_ident_away_in_goal (id_of_string "res") named_ctxt in + let res_id = Namegen.next_ident_away_in_goal (id_of_string "_res") named_ctxt in let fv_id = Namegen.next_ident_away_in_goal (id_of_string "fv") (res_id :: named_ctxt) in (*i we can then type the argument to be applied to the function [f] i*) let args_as_rels = Array.of_list (args_from_decl 1 [] fun_ctxt) in |