diff options
Diffstat (limited to 'user-contrib')
| -rw-r--r-- | user-contrib/Ltac2/Constr.v | 2 | ||||
| -rw-r--r-- | user-contrib/Ltac2/tac2core.ml | 11 |
2 files changed, 6 insertions, 7 deletions
diff --git a/user-contrib/Ltac2/Constr.v b/user-contrib/Ltac2/Constr.v index 4cc9d99c64..72cac900cd 100644 --- a/user-contrib/Ltac2/Constr.v +++ b/user-contrib/Ltac2/Constr.v @@ -24,7 +24,7 @@ Ltac2 Type case. Ltac2 Type case_invert := [ | NoInvert -| CaseInvert (instance,constr array) +| CaseInvert (constr array) ]. Ltac2 Type kind := [ diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml index 1efbc80e93..64a2b24404 100644 --- a/user-contrib/Ltac2/tac2core.ml +++ b/user-contrib/Ltac2/tac2core.ml @@ -109,15 +109,14 @@ let to_rec_declaration (nas, cs) = let of_case_invert = let open Constr in function | NoInvert -> ValInt 0 - | CaseInvert {univs;args} -> - v_blk 0 [|of_instance univs; of_array of_constr args|] + | CaseInvert {indices} -> + v_blk 0 [|of_array of_constr indices|] let to_case_invert = let open Constr in function | ValInt 0 -> NoInvert - | ValBlk (0, [|univs;args|]) -> - let univs = to_instance univs in - let args = to_array to_constr args in - CaseInvert {univs;args} + | ValBlk (0, [|indices|]) -> + let indices = to_array to_constr indices in + CaseInvert {indices} | _ -> CErrors.anomaly Pp.(str "unexpected value shape") let of_result f = function |