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 --------
 pretyping/reductionops.mli |  1 -
 pretyping/tacred.ml        | 16 ++++++++++++----
 3 files changed, 12 insertions(+), 13 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 =
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 58fff49faa..3b20a4f1f5 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -241,7 +241,6 @@ val is_arity : env ->  evar_map -> constr -> bool
 val is_sort : env -> evar_map -> types -> bool
 
 val contract_fix : evar_map -> fixpoint -> constr
-val fix_recarg : ('a, 'a) pfixpoint -> 'b Stack.t -> (int * 'b) option
 
 (** {6 Querying the kernel conversion oracle: opaque/transparent constants } *)
 val is_transparent : Environ.env -> Constant.t tableKey -> bool
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 352ced0c79..164ea4230a 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -557,6 +557,14 @@ let recargs = function
   | EvalVar _ | EvalRel _ | EvalEvar _ -> None
   | EvalConst c -> ReductionBehaviour.get (GlobRef.ConstRef c)
 
+let fix_recarg ((recindices,bodynum),_) stack =
+  assert (0 <= bodynum && bodynum < Array.length recindices);
+  let recargnum = Array.get recindices bodynum in
+  try
+    Some (recargnum, List.nth stack recargnum)
+  with Failure _ ->
+    None
+
 let reduce_projection env sigma p ~npars (recarg'hd,stack') stack =
   (match EConstr.kind sigma recarg'hd with
   | Construct _ ->
@@ -761,7 +769,7 @@ and whd_simpl_stack env sigma =
   redrec
 
 and reduce_fix env sigma fix stack =
-  match fix_recarg fix (Stack.append_app_list stack Stack.empty) with
+  match fix_recarg fix stack with
     | None -> NotReducible
     | Some (recargnum,recarg) ->
         let (recarg'hd,_ as recarg') = whd_construct_stack env sigma recarg in
@@ -771,7 +779,7 @@ and reduce_fix env sigma fix stack =
            | _ -> NotReducible)
 
 and reduce_fix_use_function env sigma f fix stack =
-  match fix_recarg fix (Stack.append_app_list stack Stack.empty) with
+  match fix_recarg fix stack with
     | None -> NotReducible
     | Some (recargnum,recarg) ->
         let (recarg'hd,_ as recarg') =
@@ -857,10 +865,10 @@ let try_red_product env sigma c =
       | App (f,l) ->
           (match EConstr.kind sigma f with
              | Fix fix ->
-                 let stack = Stack.append_app l Stack.empty in
-                 (match fix_recarg fix stack with
+                 (match fix_recarg fix (Array.to_list l) with
                     | None -> raise Redelimination
                     | Some (recargnum,recarg) ->
+                        let stack = Stack.append_app l Stack.empty in
                         let recarg' = redrec env recarg in
                         let stack' = Stack.assign stack recargnum recarg' in
                         simpfun (Stack.zip sigma (f,stack')))
-- 
cgit v1.2.3