diff options
| author | Pierre-Marie Pédrot | 2021-01-04 10:52:38 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-01-12 13:20:29 +0100 |
| commit | 71b5649acf83acb3fe6f1c5ddc468d5c504b7983 (patch) | |
| tree | 1c8bf4e04fbd91e30d613819ca39522cc8302715 /pretyping/detyping.ml | |
| parent | bedea3079b35982abefe4b78ae7aa0f6819842f6 (diff) | |
Change the case representation of patterns.
Diffstat (limited to 'pretyping/detyping.ml')
| -rw-r--r-- | pretyping/detyping.ml | 15 |
1 files changed, 0 insertions, 15 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index bb5125f5ed..722a0a2048 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -1160,18 +1160,3 @@ let rec subst_glob_constr env subst = DAst.map (function GArray(u,t',def',ty') ) - -(* Utilities to transform kernel cases to simple pattern-matching problem *) - -let simple_cases_matrix_of_branches ind brs = - List.map (fun (i,n,b) -> - let nal,c = it_destRLambda_or_LetIn_names n b in - let mkPatVar na = DAst.make @@ PatVar na in - let p = DAst.make @@ PatCstr ((ind,i+1),List.map mkPatVar nal,Anonymous) in - let ids = List.map_filter Nameops.Name.to_option nal in - CAst.make @@ (ids,[p],c)) - brs - -let return_type_of_predicate ind nrealargs_tags pred = - let nal,p = it_destRLambda_or_LetIn_names (nrealargs_tags@[false]) pred in - (List.hd nal, Some (CAst.make (ind, List.tl nal))), Some p |