diff options
Diffstat (limited to 'pretyping/tacred.ml')
| -rw-r--r-- | pretyping/tacred.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 024f190f2..1c7cfa9f6 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -362,7 +362,7 @@ let make_elim_fun (names,(nbfix,lv,n)) largs = let dummy = mkProp let vfx = id_of_string"_expanded_fix_" -let vfun = id_of_string"_elimminator_function_" +let vfun = id_of_string"_eliminator_function_" (* Mark every occurrence of substituted vars (associated to a function) as a problem variable: an evar that can be instantiated either by |