diff options
| author | Gaëtan Gilbert | 2020-12-11 13:20:54 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-01-04 14:02:02 +0100 |
| commit | 868b948f8a7bd583d467c5d02dfb34d328d53d37 (patch) | |
| tree | 045e0b730c5abebafe6300fa382b71034519a024 /user-contrib | |
| parent | b6d5332c6e3127ba3fec466abe502ee40c031ed2 (diff) | |
Remove redundant univ and parameter info from CaseInvert
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 |