align modes

FissoreD · Jan 24, 2024 · 1619ffa · 1619ffa
1 parent cbe7639
commit 1619ffa
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 6 deletions.
diff --git a/coq-builtin.elpi b/coq-builtin.elpi
@@ -1223,9 +1223,9 @@ coq.CS.canonical-projections I L :-
 
 % Hint Mode
 kind hint-mode type.
-type mode-ground hint-mode. % No Evar
-type mode-input hint-mode. % No Head Evar
-type mode-output hint-mode. % Anything
+type mode-ground hint-mode. % No Evar (+)
+type mode-input  hint-mode. % No Head Evar (!)
+type mode-output hint-mode. % Anything (-)
 
 % [coq.hints.add-mode GR DB Mode] Adds a mode declaration to DB about
 % GR.

diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml
@@ -992,13 +992,13 @@ let mode = let open API.AlgebraicData in let open Hints in declare {
   doc = "Hint Mode";
   pp = (fun fmt (x : hint_mode) -> Pp.pp_with fmt (pp_hint_mode x));
   constructors = [
-    K ("mode-ground", "No Evar",N,
+    K ("mode-ground", "No Evar (+)",N,
       B ModeInput,
       M (fun ~ok ~ko -> function ModeInput -> ok | _ -> ko ()));
-    K("mode-input","No Head Evar",N,
+    K("mode-input ","No Head Evar (!)",N,
       B ModeNoHeadEvar,
       M (fun ~ok ~ko -> function ModeNoHeadEvar -> ok | _ -> ko ()));
-    K("mode-output","Anything",N,
+    K("mode-output","Anything (-)",N,
       B ModeOutput,
       M (fun ~ok ~ko -> function ModeOutput -> ok | _ -> ko ()));
   ]