diff options
author | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
commit | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch) | |
tree | dabcac548e299fee1da464c93b3dba98484f45b1 /contrib/interface/pbp.ml | |
parent | 2281410e38ef99d025ea77194585a9bc019fdaa9 (diff) |
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'contrib/interface/pbp.ml')
-rw-r--r-- | contrib/interface/pbp.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml index d2f71bfc..06b957d9 100644 --- a/contrib/interface/pbp.ml +++ b/contrib/interface/pbp.ml @@ -156,29 +156,29 @@ let make_pbp_pattern x = let rec make_then = function | [] -> TacId [] | [t] -> t - | t1::t2::l -> make_then (TacThen (t1,t2)::l) + | t1::t2::l -> make_then (TacThen (t1,[||],t2,[||])::l) let make_pbp_atomic_tactic = function | PbpTryAssumption None -> TacTry (TacAtom (zz, TacAssumption)) | 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) + 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) | PbpLApply h -> TacAtom (zz, TacLApply (make_var h)) - | PbpApply h -> TacAtom (zz, TacApply (make_var h,NoBindings)) + | PbpApply h -> TacAtom (zz, TacApply (true,false,(make_var h,NoBindings))) | PbpElim (hyp_name, names) -> let bind = List.map (fun s ->(zz,NamedHyp s,make_pbp_pattern s)) names in TacAtom - (zz, TacElim ((make_var hyp_name,ExplicitBindings bind),None)) + (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) |