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 ac152f906..06b957d9c 100644 --- a/contrib/interface/pbp.ml +++ b/contrib/interface/pbp.ml @@ -166,7 +166,7 @@ let make_pbp_atomic_tactic = function TacAtom (zz, TacSplit (false,true,ImplicitBindings [make_pbp_pattern x])) | PbpGeneralize (h,args) -> let l = List.map make_pbp_pattern args in - TacAtom (zz, TacGeneralize [([],make_app (make_var h) l),Anonymous]) + TacAtom (zz, TacGeneralize [((true,[]),make_app (make_var h) l),Anonymous]) | PbpLeft -> TacAtom (zz, TacLeft (false,NoBindings)) | PbpRight -> TacAtom (zz, TacRight (false,NoBindings)) | PbpIntros l -> TacAtom (zz, TacIntroPattern l) |