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 /checker | |
| 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 'checker')
| -rw-r--r-- | checker/values.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/checker/values.ml b/checker/values.ml index 4e99d087df..907f9f7e32 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -147,7 +147,7 @@ let rec v_constr = [|v_puniverses v_cst|]; (* Const *) [|v_puniverses v_ind|]; (* Ind *) [|v_puniverses v_cons|]; (* Construct *) - [|v_caseinfo;v_constr;v_case_invert;v_constr;Array v_constr|]; (* Case *) + [|v_caseinfo;v_instance; Array v_constr; v_case_return; v_case_invert; v_constr; Array v_case_branch|]; (* Case *) [|v_fix|]; (* Fix *) [|v_cofix|]; (* CoFix *) [|v_proj;v_constr|]; (* Proj *) @@ -160,7 +160,11 @@ and v_prec = Tuple ("prec_declaration", [|Array (v_binder_annot v_name); Array v_constr; Array v_constr|]) and v_fix = Tuple ("pfixpoint", [|Tuple ("fix2",[|Array Int;Int|]);v_prec|]) and v_cofix = Tuple ("pcofixpoint",[|Int;v_prec|]) -and v_case_invert = Sum ("case_inversion", 1, [|[|v_instance;Array v_constr|]|]) +and v_case_invert = Sum ("case_inversion", 1, [|[|Array v_constr|]|]) + +and v_case_branch = Tuple ("case_branch", [|Array (v_binder_annot v_name); v_constr|]) + +and v_case_return = Tuple ("case_return", [|Array (v_binder_annot v_name); v_constr|]) let v_rdecl = v_sum "rel_declaration" 0 [| [|v_binder_annot v_name; v_constr|]; (* LocalAssum *) |