aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/pretyping.mli
diff options
context:
space:
mode:
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 e7a8374b5..974cba1b4 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -97,7 +97,7 @@ sig
rawconstr -> unsafe_type_judgment
val pretype_gen :
- evar_defs ref -> env ->
+ bool -> bool -> evar_defs ref -> env ->
var_map * (identifier * identifier option) list ->
typing_constraint -> rawconstr -> constr