aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/pretyping.mli
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-06-17 18:25:02 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-06-18 18:54:43 +0200
commit53ced0735f7e24735d78a02fc74588b8d9186eab (patch)
tree93661920f42d9be934e59f5f972d165ea24785b7 /pretyping/pretyping.mli
parent806e3bc0ecfbf0a6bfd20e80caa8250e60d39152 (diff)
Moving the typing_flags to the environment.
Diffstat (limited to 'pretyping/pretyping.mli')
-rw-r--r--pretyping/pretyping.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 2c02b4a21..824bb11aa 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -22,7 +22,7 @@ open Misctypes
(** An auxiliary function for searching for fixpoint guard indexes *)
-val search_guard : tflags:Declarations.typing_flags ->
+val search_guard :
Loc.t -> env -> int list list -> rec_declaration -> int array
type typing_constraint = OfType of types | IsType | WithoutTypeConstraint