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/funind/glob_term_to_relation.ml | |
| 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/funind/glob_term_to_relation.ml')
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 4 |
1 files changed, 2 insertions, 2 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 |