aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/pretyping.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/pretyping.mli')
-rw-r--r--pretyping/pretyping.mli3
1 files changed, 1 insertions, 2 deletions
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index eba26bafe..18a6b03a7 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -81,8 +81,7 @@ sig
val understand_judgment_tcc : evar_map ref -> env -> rawconstr -> unsafe_judgment
(**/**)
- (** Internal of Pretyping...
- *)
+ (** Internal of Pretyping... *)
val pretype :
type_constraint -> env -> evar_map ref ->
var_map * (identifier * identifier option) list ->