Quick fix to #4595 (making notations containing "ltac:" unused for printing).

Also getting rid of a global side-effect.

8 files changed, 33 insertions, 31 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index f98873aa66..194f5f1c2b 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2013,14 +2013,14 @@ let interp_notation_constr ?(impls=empty_internalization_env) nenv a =
 						tmp_scope = None; scopes = []; impls = impls}
     false (empty_ltac_sign, vl) a in
   (* Translate and check that [c] has all its free variables bound in [vars] *)
-  let a = notation_constr_of_glob_constr nenv c in
+  let a, reversible = notation_constr_of_glob_constr nenv c in
   (* Splits variables into those that are binding, bound, or both *)
   (* binding and bound *)
   let out_scope = function None -> None,[] | Some (a,l) -> a,l in
   let vars = Id.Map.map (fun (isonlybinding, sc, typ) ->
     (!isonlybinding, out_scope !sc, typ)) vl in
   (* Returns [a] and the ordered list of variables with their scopes *)
-  vars, a
+  vars, a, reversible
 
 (* Interpret binders and contexts  *)
 
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index eea76aa310..61e7c6f5cb 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -186,7 +186,7 @@ val global_reference_in_absolute_module : DirPath.t -> Id.t -> constr
 val interp_notation_constr : ?impls:internalization_env ->
   notation_interp_env -> constr_expr ->
   (bool * subscopes * notation_var_internalization_type) Id.Map.t *
-  notation_constr
+  notation_constr * reversibility_flag
 
 (** Globalization options *)
 val parsing_explicit : bool ref
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index cc81a00919..7b520c1c11 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -323,6 +323,7 @@ let compare_recursive_parts found f f' (iterator,subc) =
 
 let notation_constr_and_vars_of_glob_constr a =
   let found = ref ([],[],[]) in
+  let has_ltac = ref false in
   let rec aux c =
     let keepfound = !found in
     (* n^2 complexity but small and done only once per notation *)
@@ -368,7 +369,9 @@ let notation_constr_and_vars_of_glob_constr a =
       NRec (fk,idl,dll,Array.map aux tl,Array.map aux bl)
   | GCast (_,c,k) -> NCast (aux c,Miscops.map_cast_type aux k)
   | GSort (_,s) -> NSort s
-  | GHole (_,w,naming,arg) -> NHole (w, naming, arg)
+  | GHole (_,w,naming,arg) ->
+     if arg != None then has_ltac := true;
+     NHole (w, naming, arg)
   | GRef (_,r,_) -> NRef r
   | GEvar _ | GPatVar _ ->
       error "Existential variables not allowed in notations."
@@ -376,9 +379,10 @@ let notation_constr_and_vars_of_glob_constr a =
   in
   let t = aux a in
   (* Side effect *)
-  t, !found
+  t, !found, !has_ltac
 
-let check_variables nenv (found,foundrec,foundrecbinding) =
+let check_variables_and_reversibility nenv (found,foundrec,foundrecbinding) =
+  let injective = ref true in
   let recvars = nenv.ninterp_rec_vars in
   let fold _ y accu = Id.Set.add y accu in
   let useless_vars = Id.Map.fold fold recvars Id.Set.empty in
@@ -401,7 +405,7 @@ let check_variables nenv (found,foundrec,foundrecbinding) =
 	error
           (Id.to_string x ^
           " should not be bound in a recursive pattern of the right-hand side.")
-      else nenv.ninterp_only_parse <- true
+      else injective := false
   in
   let check_pair s x y where =
     if not (List.mem_f (pair_equal Id.equal Id.equal) (x,y) where) then
@@ -421,12 +425,13 @@ let check_variables nenv (found,foundrec,foundrecbinding) =
 	  with Not_found -> check_bound x
 	end
     | NtnInternTypeIdent -> check_bound x in
-  Id.Map.iter check_type vars
+  Id.Map.iter check_type vars;
+  !injective
 
 let notation_constr_of_glob_constr nenv a =
-  let a, found = notation_constr_and_vars_of_glob_constr a in
-  let () = check_variables nenv found in
-  a
+  let a, found, has_ltac = notation_constr_and_vars_of_glob_constr a in
+  let injective = check_variables_and_reversibility nenv found in
+  a, not has_ltac && injective
 
 (**********************************************************************)
 (* Substitution of kernel names, avoiding a list of bound identifiers *)
@@ -436,7 +441,6 @@ let notation_constr_of_constr avoiding t =
   let nenv = {
     ninterp_var_type = Id.Map.empty;
     ninterp_rec_vars = Id.Map.empty;
-    ninterp_only_parse = false;
   } in
   notation_constr_of_glob_constr nenv t
 
@@ -454,7 +458,7 @@ let rec subst_notation_constr subst bound raw =
   | NRef ref ->
       let ref',t = subst_global subst ref in
 	if ref' == ref then raw else
-	  notation_constr_of_constr bound t
+	  fst (notation_constr_of_constr bound t)
 
   | NVar _ -> raw
 
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index 4ebd3ddd80..c8fcbf7410 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -29,7 +29,7 @@ val ldots_var : Id.t
     bound by the notation; also interpret recursive patterns           *)
 
 val notation_constr_of_glob_constr : notation_interp_env ->
-  glob_constr -> notation_constr
+  glob_constr -> notation_constr * reversibility_flag
 
 (** Re-interpret a notation as a [glob_constr], taking care of binders *)
 
diff --git a/intf/notation_term.mli b/intf/notation_term.mli
index 883b017727..1ab9980a5c 100644
--- a/intf/notation_term.mli
+++ b/intf/notation_term.mli
@@ -73,10 +73,11 @@ type interpretation =
     (Id.t * (subscopes * notation_var_instance_type)) list *
     notation_constr
 
+type reversibility_flag = bool
+
 type notation_interp_env = {
   ninterp_var_type : notation_var_internalization_type Id.Map.t;
   ninterp_rec_vars : Id.t Id.Map.t;
-  mutable ninterp_only_parse : bool;
 }
 
 type grammar_constr_prod_item =
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index e89c3ea719..7e33cc1d4a 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -2577,6 +2577,9 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e
 	typing_function = typing_fun } in
 
     let j = compile pb in
+
+    (* We coerce to the tycon (if an elim predicate was provided) *)
+    let j = inh_conv_coerce_to_tycon loc env myevdref j tycon in
     evdref := !myevdref;
     j in
 
@@ -2587,6 +2590,4 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e
   (* We check for unused patterns *)
   List.iter (check_unused_pattern env) matx;
 
-  (* We coerce to the tycon (if an elim predicate was provided) *)
-  inh_conv_coerce_to_tycon loc env evdref j tycon
-
+  j
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index ce8798c713..42f65dfb52 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -890,12 +890,12 @@ let warn_non_reversible_notation =
          (fun () ->
           strbrk "This notation will not be used for printing as it is not reversible.")
 
-let is_not_printable onlyparse noninjective = function
+let is_not_printable onlyparse nonreversible = function
 | NVar _ ->
   if not onlyparse then warn_notation_bound_to_variable ();
   true
 | _ ->
-   if not onlyparse && noninjective then
+   if not onlyparse && nonreversible then
      (warn_non_reversible_notation (); true)
   else onlyparse
 
@@ -1182,12 +1182,11 @@ let add_notation_in_scope local df c mods scope =
   let nenv = {
     ninterp_var_type = to_map i_vars;
     ninterp_rec_vars = to_map recvars;
-    ninterp_only_parse = false;
   } in
-  let (acvars, ac) = interp_notation_constr nenv c in
+  let (acvars, ac, reversible) = interp_notation_constr nenv c in
   let interp = make_interpretation_vars recvars acvars in
   let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in
-  let onlyparse = is_not_printable onlyparse nenv.ninterp_only_parse ac in
+  let onlyparse = is_not_printable onlyparse (not reversible) ac in
   let notation = {
     notobj_local = local;
     notobj_scope = scope;
@@ -1222,12 +1221,11 @@ let add_notation_interpretation_core local df ?(impls=empty_internalization_env)
   let nenv = {
     ninterp_var_type = to_map i_vars;
     ninterp_rec_vars = to_map recvars;
-    ninterp_only_parse = false;
   } in
-  let (acvars, ac) = interp_notation_constr ~impls nenv c in
+  let (acvars, ac, reversible) = interp_notation_constr ~impls nenv c in
   let interp = make_interpretation_vars recvars acvars in
   let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in
-  let onlyparse = is_not_printable onlyparse nenv.ninterp_only_parse ac in
+  let onlyparse = is_not_printable onlyparse (not reversible) ac in
   let notation = {
     notobj_local = local;
     notobj_scope = scope;
@@ -1364,10 +1362,9 @@ let add_syntactic_definition ident (vars,c) local onlyparse =
       let nenv = {
         ninterp_var_type = i_vars;
         ninterp_rec_vars = Id.Map.empty;
-        ninterp_only_parse = false;
       } in
-      let nvars, pat = interp_notation_constr nenv c in
-      let () = nonprintable := nenv.ninterp_only_parse in
+      let nvars, pat, reversible = interp_notation_constr nenv c in
+      let () = nonprintable := not reversible in
       let map id = let (_,sc,_) = Id.Map.find id nvars in (id, sc) in
       List.map map vars, pat
   in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index e16b9128e4..d639811c56 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1153,7 +1153,6 @@ let vernac_declare_arguments locality r l nargs flags =
 let default_env () = {
   Notation_term.ninterp_var_type = Id.Map.empty;
   ninterp_rec_vars = Id.Map.empty;
-  ninterp_only_parse = false;
 }
 
 let vernac_reserve bl =
@@ -1162,7 +1161,7 @@ let vernac_reserve bl =
     let sigma = Evd.from_env env in
     let t,ctx = Constrintern.interp_type env sigma c in
     let t = Detyping.detype false [] env (Evd.from_ctx ctx) t in
-    let t = Notation_ops.notation_constr_of_glob_constr (default_env ()) t in
+    let t,_ = Notation_ops.notation_constr_of_glob_constr (default_env ()) t in
     Reserve.declare_reserved_type idl t)
   in List.iter sb_decl bl