diff options
| author | Pierre-Marie Pédrot | 2020-06-24 21:44:08 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-07-05 21:41:08 +0200 |
| commit | a659a12ca88bebaf1fa7f201023cc06be34849d9 (patch) | |
| tree | 2fd34dc2ca30a7f0bfda0d53a788d6785e073e1d /pretyping/reductionops.ml | |
| parent | 5c1730ca2533b17066e7ee5c672ae6aa5fdef1dc (diff) | |
Inline the Reductionops.fix_recarg function.
It was only used in Tacred, and with a type that forced to perform a
change of representation of stacks.
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 18a0637efa..20240a175d 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -572,14 +572,6 @@ let reduce_and_refold_fix recfun env sigma fix sk = (fun _ (t,sk') -> recfun (t,sk')) [] sigma raw_answer sk -let fix_recarg ((recindices,bodynum),_) stack = - assert (0 <= bodynum && bodynum < Array.length recindices); - let recargnum = Array.get recindices bodynum in - try - Some (recargnum, Stack.nth stack recargnum) - with Not_found -> - None - open Primred module CNativeEntries = |