diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-04-02 18:41:09 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-04-21 15:56:34 +0200 |
| commit | ce6bbd05b7d741750228956a7e045cb202ec0e74 (patch) | |
| tree | 317c23b46d0bf5d6a1a99a5f7ac369da6e5aa0df | |
| parent | a33f7ad548ed312a2665c87baca9fb7b233e8cbf (diff) | |
Some dead code.
| -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 |