diff options
| author | Pierre-Marie Pédrot | 2017-08-28 20:31:33 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-28 20:31:33 +0200 |
| commit | ee7ebf17245c65b630d5b7c01de8ad9253bd9523 (patch) | |
| tree | 0393bed9b807406090c6e2bfe3362009e0642d51 /src | |
| parent | 99ec137899c2684da2a8c221f333e0e9adee2c48 (diff) | |
Fix coq/ltac2#6: Expected and actual types are flipped.
Diffstat (limited to 'src')
| -rw-r--r-- | src/tac2intern.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/tac2intern.ml b/src/tac2intern.ml index 5c1c90e924..9d22b18af4 100644 --- a/src/tac2intern.ml +++ b/src/tac2intern.ml @@ -947,7 +947,7 @@ and intern_case env loc e pl = in brT in - let () = unify ~loc:(loc_of_tacexpr br) env ret tbr in + let () = unify ~loc:(loc_of_tacexpr br) env tbr ret in intern_branch rem in let () = intern_branch pl in |