Adding support for syntax "let _ := e in e'" in Ltac.

Adding a file fixing #5996 and which uses this feature.

5 files changed, 17 insertions, 14 deletions

diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index c577cb219..116152568 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -232,10 +232,12 @@ GEXTEND Gram
       | l = ident -> Name.Name l ] ]
   ;
   let_clause:
-    [ [ id = identref; ":="; te = tactic_expr ->
-         (id, arg_of_expr te)
-      | id = identref; args = LIST1 input_fun; ":="; te = tactic_expr ->
-         (id, arg_of_expr (TacFun(args,te))) ] ]
+    [ [ (l,id) = identref; ":="; te = tactic_expr ->
+         ((l,Name id), arg_of_expr te)
+      | na = ["_" -> (Some !@loc,Anonymous)]; ":="; te = tactic_expr ->
+         (na, arg_of_expr te)
+      | (l,id) = identref; args = LIST1 input_fun; ":="; te = tactic_expr ->
+         ((l,Name id), arg_of_expr (TacFun(args,te))) ] ]
   ;
   match_pattern:
     [ [ IDENT "context";  oid = OPT Constr.ident;
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index e467d3e2c..28a13fb40 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -536,8 +536,8 @@ let pr_goal_selector ~toplevel s =
 
   let pr_funvar n = spc () ++ Name.print n
 
-  let pr_let_clause k pr (id,(bl,t)) =
-    hov 0 (keyword k ++ spc () ++ pr_lident id ++ prlist pr_funvar bl ++
+  let pr_let_clause k pr (na,(bl,t)) =
+    hov 0 (keyword k ++ spc () ++ pr_lname na ++ prlist pr_funvar bl ++
              str " :=" ++ brk (1,1) ++ pr (TacArg (Loc.tag t)))
 
   let pr_let_clauses recflag pr = function
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 163973688..9bd3efc6b 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -254,7 +254,7 @@ and 'a gen_tactic_expr =
   | TacFail of global_flag * int or_var * 'n message_token list
   | TacInfo of 'a gen_tactic_expr
   | TacLetIn of rec_flag *
-      (Id.t located * 'a gen_tactic_arg) list *
+      (Name.t located * 'a gen_tactic_arg) list *
       'a gen_tactic_expr
   | TacMatch of lazy_flag *
       'a gen_tactic_expr *
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index f171fd07d..b16b0a7ba 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -468,9 +468,10 @@ let rec intern_match_goal_hyps ist ?(as_type=false) lfun = function
 (* Utilities *)
 let extract_let_names lrc =
   let fold accu ((loc, name), _) =
-    if Id.Set.mem name accu then user_err ?loc
+    Nameops.Name.fold_right (fun id accu ->
+    if Id.Set.mem id accu then user_err ?loc
       ~hdr:"glob_tactic" (str "This variable is bound several times.")
-    else Id.Set.add name accu
+    else Id.Set.add id accu) name accu
   in
   List.fold_left fold Id.Set.empty lrc
 
@@ -812,7 +813,7 @@ let notation_subst bindings tac =
   let fold id c accu =
     let loc = Glob_ops.loc_of_glob_constr (fst c) in
     let c = ConstrMayEval (ConstrTerm c) in
-    ((loc, id), c) :: accu
+    ((loc, Name id), c) :: accu
   in
   let bindings = Id.Map.fold fold bindings [] in
   (** This is theoretically not correct due to potential variable capture, but
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index fd75862c6..1a8ec6d6f 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1397,9 +1397,9 @@ and tactic_of_value ist vle =
 and interp_letrec ist llc u =
   Proofview.tclUNIT () >>= fun () -> (* delay for the effects of [lref], just in case. *)
   let lref = ref ist.lfun in
-  let fold accu ((_, id), b) =
+  let fold accu ((_, na), b) =
     let v = of_tacvalue (VRec (lref, TacArg (Loc.tag b))) in
-    Id.Map.add id v accu
+    Name.fold_right (fun id -> Id.Map.add id v) na accu
   in
   let lfun = List.fold_left fold ist.lfun llc in
   let () = lref := lfun in
@@ -1412,9 +1412,9 @@ and interp_letin ist llc u =
   | [] ->
     let ist = { ist with lfun } in
     val_interp ist u
-  | ((_, id), body) :: defs ->
+  | ((_, na), body) :: defs ->
     Ftactic.bind (interp_tacarg ist body) (fun v ->
-    fold (Id.Map.add id v lfun) defs)
+    fold (Name.fold_right (fun id -> Id.Map.add id v) na lfun) defs)
   in
   fold ist.lfun llc