From 44f87dae748f8c84b7c9290b00c4d76197e5497a Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 1 May 2019 10:02:21 +0200
Subject: [elaboration] Bidirectionality hints

This feature makes it possible to tell type inference to type
applications of a global `foo` using typing information from the context
once the `n` first arguments are known.

The syntax is: `Arguments foo x y | z`.

Closes #7910
---
 printing/prettyp.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'printing/prettyp.ml')

diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index fca33a24bf..f55bfb504f 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -304,6 +304,12 @@ let print_inductive_argument_scopes =
   print_args_data_of_inductive_ids
     Notation.find_arguments_scope (Option.has_some) print_argument_scopes
 
+let print_bidi_hints gr =
+  match Pretyping.get_bidirectionality_hint gr with
+  | None -> []
+  | Some nargs ->
+    [str "Using typing information from context after typing the " ++ int nargs ++ str " first arguments"]
+
 (*********************)
 (* "Locate" commands *)
 
@@ -841,7 +847,8 @@ let print_about_any ?loc env sigma k udecl =
 	print_name_infos ref @
 	(if Pp.ismt rb then [] else [rb]) @
 	print_opacity ref @
-	[hov 0 (str "Expands to: " ++ pr_located_qualid k)])
+  print_bidi_hints ref @
+  [hov 0 (str "Expands to: " ++ pr_located_qualid k)])
   | Syntactic kn ->
     let () = match Syntax_def.search_syntactic_definition kn with
     | [],Notation_term.NRef ref -> Dumpglob.add_glob ?loc ref
-- 
cgit v1.2.3