diff options
Diffstat (limited to 'contrib/interface/pbp.ml')
| -rw-r--r-- | contrib/interface/pbp.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml index 0680cc23e5..c16cde7d72 100644 --- a/contrib/interface/pbp.ml +++ b/contrib/interface/pbp.ml @@ -163,12 +163,12 @@ let make_pbp_atomic_tactic = function | PbpTryAssumption (Some a) -> TacTry (TacAtom (zz, TacExact (make_var a))) | PbpExists x -> - TacAtom (zz, TacSplit (true,ImplicitBindings [make_pbp_pattern x])) + 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]) - | PbpLeft -> TacAtom (zz, TacLeft NoBindings) - | PbpRight -> TacAtom (zz, TacRight NoBindings) + | PbpLeft -> TacAtom (zz, TacLeft (false,NoBindings)) + | PbpRight -> TacAtom (zz, TacRight (false,NoBindings)) | PbpIntros l -> TacAtom (zz, TacIntroPattern l) | PbpLApply h -> TacAtom (zz, TacLApply (make_var h)) | PbpApply h -> TacAtom (zz, TacApply (true,false,(make_var h,NoBindings))) @@ -178,7 +178,7 @@ let make_pbp_atomic_tactic = function (zz, TacElim (false,(make_var hyp_name,ExplicitBindings bind),None)) | PbpTryClear l -> TacTry (TacAtom (zz, TacClear (false,List.map (fun s -> AI (zz,s)) l))) - | PbpSplit -> TacAtom (zz, TacSplit (false,NoBindings));; + | PbpSplit -> TacAtom (zz, TacSplit (false,false,NoBindings));; let rec make_pbp_tactic = function | PbpThen tl -> make_then (List.map make_pbp_atomic_tactic tl) |