diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index f388f9005..97b1b1645 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -201,13 +201,6 @@ let ise_and evd l = | UnifFailure _ as x -> x in ise_and evd l -(* This function requires to get the outermost arguments first. It is - a fold_right for backward compatibility. - - It tries to unify the suffix of 2 lists element by element and if - it reaches the end of a list, it returns the remaining elements in - the other list if there are some. -*) let ise_exact ise x1 x2 = match ise x1 x2 with | None, out -> out |