diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-10-22 23:50:11 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-04 14:12:45 +0100 |
| commit | 8c6092e8c43a74a8a175a532580284124c06e34f (patch) | |
| tree | ece4db520837006b2e3bffcc165b7c76a45b1bd1 /plugins/ltac/tacinterp.ml | |
| parent | f281a8a88e8fc7c41cc5680db2443d9da33b47b7 (diff) | |
Adding support for syntax "let _ := e in e'" in Ltac.
Adding a file fixing #5996 and which uses this feature.
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 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 |