Permalink
Browse files

correcting a little bug in Function

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15947 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information...
1 parent 1408c0f commit d214946779d440a2cca8053bd52f35ac748f2823 jforest committed Oct 31, 2012
Showing with 3 additions and 3 deletions.
  1. +2 −2 plugins/funind/glob_term_to_relation.ml
  2. +1 −1 plugins/funind/invfun.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
View
@@ -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

0 comments on commit d214946

Please sign in to comment.