aboutsummaryrefslogtreecommitdiff
path: root/src/tac2stdlib.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/tac2stdlib.ml')
-rw-r--r--src/tac2stdlib.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index 28d4967874..9ed3d5b32e 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -186,9 +186,9 @@ let to_strategy v = match Value.to_int v with
let strategy = make_to_repr to_strategy
let to_inversion_kind v = match Value.to_int v with
-| 0 -> Misctypes.SimpleInversion
-| 1 -> Misctypes.FullInversion
-| 2 -> Misctypes.FullInversionClear
+| 0 -> Inv.SimpleInversion
+| 1 -> Inv.FullInversion
+| 2 -> Inv.FullInversionClear
| _ -> assert false
let inversion_kind = make_to_repr to_inversion_kind