aboutsummaryrefslogtreecommitdiff
path: root/pretyping/reductionops.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/reductionops.mli')
-rw-r--r--pretyping/reductionops.mli1
1 files changed, 0 insertions, 1 deletions
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