diff options
| author | coqbot-app[bot] | 2021-01-06 13:04:20 +0000 |
|---|---|---|
| committer | GitHub | 2021-01-06 13:04:20 +0000 |
| commit | 30f497eaf34f2cf641c3fe854fc9066ae19eea67 (patch) | |
| tree | 473734cdc4ea6769de9a5563a0e9e6eeb56dce20 /vernac/auto_ind_decl.ml | |
| parent | 960178db193c8a78b9414abad13536693ee5b9b8 (diff) | |
| parent | a95654a21c350f19ad0da67713359cbf6c49e95a (diff) | |
Merge PR #13563: Revival of #9710 (Compact kernel representation of pattern-matching)
Reviewed-by: mattam82
Reviewed-by: SkySkimmer
Ack-by: gares
Ack-by: jfehrle
Diffstat (limited to 'vernac/auto_ind_decl.ml')
| -rw-r--r-- | vernac/auto_ind_decl.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index f715459616..cc59a96834 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -351,13 +351,13 @@ let build_beq_scheme mode kn = done; ar.(i) <- (List.fold_left (fun a decl -> mkLambda (RelDecl.get_annot decl, RelDecl.get_type decl, a)) - (mkCase (ci,do_predicate rel_list nb_cstr_args,NoInvert, - mkVar (Id.of_string "Y") ,ar2)) + (mkCase (Inductive.contract_case env ((ci,do_predicate rel_list nb_cstr_args, + NoInvert, mkVar (Id.of_string "Y") ,ar2)))) (constrsi.(i).cs_args)) done; mkNamedLambda (make_annot (Id.of_string "X") Sorts.Relevant) (mkFullInd ind (nb_ind-1+1)) ( mkNamedLambda (make_annot (Id.of_string "Y") Sorts.Relevant) (mkFullInd ind (nb_ind-1+2)) ( - mkCase (ci, do_predicate rel_list 0,NoInvert,mkVar (Id.of_string "X"),ar))) + mkCase (Inductive.contract_case env (ci, do_predicate rel_list 0,NoInvert,mkVar (Id.of_string "X"),ar)))) in (* build_beq_scheme *) let names = Array.make nb_ind (make_annot Anonymous Sorts.Relevant) and types = Array.make nb_ind mkSet and |