Printing notations: Cleaning in anticipation of fixing #4592.

- Making a clear distinction between expressions of the notation which
  are associated to binding variables only (as in `Notation "'lam' x ,
  P" := (fun x => P)" or `Notation "'exists2' x : t , p & q" := (ex2
  (fun x:t => p) (fun x:t => q))') and those which are associated to
  at list one subterm (e.g. `Notation "x .+1" := (S x)' but also
  "Notation "{# x | P }" := (ex2 _ (fun y => x = F y) (fun x => P))'
  as in #4592). The former have type NtnTypeOnlyBinder.
- Thus avoiding in particular encoding too early Anonymous as GHole
  and "Name id" as "GVar id".

There is a non-trivial alpha-conversion work to do to get #4592
working. See comments in Notation_ops.add_env.

1 files changed, 13 insertions, 7 deletions

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 0d002aa8e..98d1a2377 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -1017,9 +1017,10 @@ let make_internalization_vars recvars mainvars typs =
   let extratyps = List.map (fun (x,y) -> (y,List.assoc x maintyps)) recvars in
   maintyps @ extratyps
 
-let make_interpretation_type isrec = function
+let make_interpretation_type isrec isonlybinding = function
   | NtnInternTypeConstr when isrec -> NtnTypeConstrList
-  | NtnInternTypeConstr | NtnInternTypeIdent -> NtnTypeConstr
+  | NtnInternTypeConstr | NtnInternTypeIdent ->
+     if isonlybinding then NtnTypeOnlyBinder else NtnTypeConstr
   | NtnInternTypeBinder when isrec -> NtnTypeBinderList
   | NtnInternTypeBinder -> error "Type not allowed in recursive notation."
 
@@ -1029,16 +1030,16 @@ let make_interpretation_vars recvars allvars =
     List.equal String.equal l1 l2
   in
   let check (x, y) =
-    let (scope1, _) = Id.Map.find x allvars in
-    let (scope2, _) = Id.Map.find y allvars in
+    let (_,scope1, _) = Id.Map.find x allvars in
+    let (_,scope2, _) = Id.Map.find y allvars in
     if not (eq_subscope scope1 scope2) then error_not_same_scope x y
   in
   let () = List.iter check recvars in
   let useless_recvars = List.map snd recvars in
   let mainvars =
     Id.Map.filter (fun x _ -> not (Id.List.mem x useless_recvars)) allvars in
-  Id.Map.mapi (fun x (sc, typ) ->
-    (sc, make_interpretation_type (Id.List.mem_assoc x recvars) typ)) mainvars
+  Id.Map.mapi (fun x (isonlybinding, sc, typ) ->
+    (sc, make_interpretation_type (Id.List.mem_assoc x recvars) isonlybinding typ)) mainvars
 
 let check_rule_productivity l =
   if List.for_all (function NonTerminal _ -> true | _ -> false) l then
@@ -1492,7 +1493,12 @@ let add_syntactic_definition ident (vars,c) local onlyparse =
       } in
       let nvars, pat = interp_notation_constr nenv c in
       let () = nonprintable := nenv.ninterp_only_parse in
-      let map id = let (sc, _) = Id.Map.find id nvars in (id, sc) in
+      let map id =
+        let (isonlybinding,sc, _) = Id.Map.find id nvars in
+        (* if a notation contains an ltac:, the body is not analyzed
+           and onlybinding detection fails *)
+        assert (!nonprintable || not isonlybinding);
+        (id, sc) in
       List.map map vars, pat
   in
   let onlyparse = match onlyparse with