From faef5dcc656148273063f25716923d9bd1fe2497 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sun, 9 Feb 2020 19:49:33 +0100
Subject: Use thunks to univ instead of lazy constr for template typing

---
 pretyping/reductionops.mli | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

(limited to 'pretyping/reductionops.mli')

diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index e72f5f2793..c539ec55ed 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -236,12 +236,20 @@ val hnf_lam_applist  : env ->  evar_map -> constr -> constr list -> constr
 
 val splay_prod : env ->  evar_map -> constr -> (Name.t Context.binder_annot * constr) list * constr
 val splay_lam : env ->  evar_map -> constr -> (Name.t Context.binder_annot * constr) list * constr
+val splay_prod_assum : env ->  evar_map -> constr -> rel_context * constr
+
 val splay_arity : env ->  evar_map -> constr -> (Name.t Context.binder_annot * constr) list * ESorts.t
+(** Raises [Reduction.NotArity] *)
+
 val sort_of_arity : env -> evar_map -> constr -> ESorts.t
+(** Raises [Reduction.NotArity] *)
+
 val splay_prod_n : env ->  evar_map -> int -> constr -> rel_context * constr
+(** Raises [Invalid_argument] *)
+
 val splay_lam_n : env ->  evar_map -> int -> constr -> rel_context * constr
-val splay_prod_assum :
-  env ->  evar_map -> constr -> rel_context * constr
+(** Raises [Invalid_argument] *)
+
 
 type 'a miota_args = {
   mP      : constr;     (** the result type *)
-- 
cgit v1.2.3