aboutsummaryrefslogtreecommitdiff
path: root/plugins/xml/doubleTypeInference.mli
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/xml/doubleTypeInference.mli')
-rw-r--r--plugins/xml/doubleTypeInference.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/xml/doubleTypeInference.mli b/plugins/xml/doubleTypeInference.mli
index 2e14b5580b..b604ec4c4c 100644
--- a/plugins/xml/doubleTypeInference.mli
+++ b/plugins/xml/doubleTypeInference.mli
@@ -12,7 +12,7 @@
(* http://helm.cs.unibo.it *)
(************************************************************************)
-type types = { synthesized : Term.types; expected : Term.types option; }
+type types = { synthesized : Term.types; expected : Term.types option; }
val cprop : Names.constant