diff options
| author | Matthieu Sozeau | 2018-10-17 17:10:32 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2019-02-08 11:17:56 +0100 |
| commit | 66892881c69cfb91fe1cd772cd88ac2c73c99bbe (patch) | |
| tree | 6f8ad1a7fb6056fe5c5f28f8ada44024935f8e04 | |
| parent | 8a5cd826ee8d7d51c85c834c28f090466dda33a5 (diff) | |
Fix warning unused variable
| -rw-r--r-- | pretyping/evarconv.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 96d7cff152..7b510cfd5c 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -768,7 +768,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty Feedback.msg_notice (v 0 (pr_state env evd appr1 ++ cut () ++ pr_state env evd appr2 ++ cut ())) in match (flex_kind_of_term flags env evd term1 sk1, flex_kind_of_term flags env evd term2 sk2) with - | Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) -> + | Flexible (sp1,al1), Flexible (sp2,al2) -> (* sk1[?ev1] =? sk2[?ev2] *) let f1 i = first_order env i term1 term2 sk1 sk2 and f2 i = |