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

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

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;

plugins/ltac/pptactic.ml

@@ -529,8 +529,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

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 *

plugins/ltac/tacintern.ml

@@ -458,9 +458,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
 
@@ -797,7 +798,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

plugins/ltac/tacinterp.ml

@@ -1431,9 +1431,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
@@ -1446,9 +1446,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
 

test-suite/bugs/5996.v

@@ -0,0 +1,8 @@
+Goal Type.
+  let c := constr:(prod nat nat) in
+  let c' := (eval pattern nat in c) in
+  let c' := lazymatch c' with ?f _ => f end in
+  let c'' := lazymatch c' with fun x : Set => ?f => constr:(forall x : Type, f) end in
+  let _ := type of c'' in
+  exact c''.
+Defined.