diff options
Diffstat (limited to 'contrib/interface/pbp.ml')
| -rw-r--r-- | contrib/interface/pbp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml index 4abcb5f96f..74ecdaaa3d 100644 --- a/contrib/interface/pbp.ml +++ b/contrib/interface/pbp.ml @@ -177,7 +177,7 @@ let make_pbp_atomic_tactic = function TacAtom (zz, TacElim ((make_var hyp_name,ExplicitBindings bind),None)) | PbpTryClear l -> - TacTry (TacAtom (zz, TacClear (List.map (fun s -> AN s) l))) + TacTry (TacAtom (zz, TacClear (List.map (fun s -> AI (zz,s)) l))) | PbpSplit -> TacAtom (zz, TacSplit (false,NoBindings));; let rec make_pbp_tactic = function |