From 8ffd4e54ba8a05cb57f09d4333a7990f96a4cfd0 Mon Sep 17 00:00:00 2001
From: Pierre Boutillier
Date: Wed, 23 Apr 2014 14:03:27 +0200
Subject: Reduction.Stack.Fix/Case stores Cst_stack.t

---
 pretyping/reductionops.mli | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'pretyping/reductionops.mli')

diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 091eb7c81b..ef013d5b13 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -51,9 +51,9 @@ module Stack : sig
 
   type 'a member =
   | App of 'a app_node
-  | Case of case_info * 'a * 'a array * ('a * 'a list) option
+  | Case of case_info * 'a * 'a array * 'a Cst_stack.t
   | Proj of int * int * projection
-  | Fix of fixpoint * 'a t * ('a * 'a list) option
+  | Fix of fixpoint * 'a t * 'a Cst_stack.t
   | Shift of int
   | Update of 'a
   and 'a t = 'a member list
@@ -230,7 +230,7 @@ val is_arity : env ->  evar_map -> constr -> bool
 val is_sort : env -> evar_map -> types -> bool
 
 val contract_fix : ?env:Environ.env -> fixpoint ->
-  (constr * constr list) option -> constr
+  constr Cst_stack.t -> constr
 val fix_recarg : fixpoint -> constr Stack.t -> (int * constr) option
 
 (** {6 Querying the kernel conversion oracle: opaque/transparent constants } *)
-- 
cgit v1.2.3