diff options
| author | Maxime Dénès | 2017-11-13 11:11:44 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-13 11:11:44 +0100 |
| commit | 1f9dcdee40d95ee56ef91876579f2c059939e04a (patch) | |
| tree | a018b8cddb19e2f909238e74311f59f1ab284003 /plugins/ltac/tacinterp.ml | |
| parent | d9f79d97dbc503e149cba2df1b228a94d7ac970b (diff) | |
| parent | 8c6092e8c43a74a8a175a532580284124c06e34f (diff) | |
Merge PR #6000: Adding support for syntax "let _ := e in e'" in Ltac.
Diffstat (limited to 'plugins/ltac/tacinterp.ml')
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index fd75862c6f..1a8ec6d6f6 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 |