From a659a12ca88bebaf1fa7f201023cc06be34849d9 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 24 Jun 2020 21:44:08 +0200
Subject: 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.
---
 pretyping/reductionops.ml | 8 --------
 1 file changed, 8 deletions(-)

(limited to 'pretyping/reductionops.ml')

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 =
-- 
cgit v1.2.3