correcting a little bug in Function

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15947 85f007b7-540e-0410-9357-904b9bb8a0f7

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