diff options
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/debug_tac.ml4 | 10 | ||||
| -rw-r--r-- | contrib/interface/pbp.ml | 2 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 3 |
3 files changed, 8 insertions, 7 deletions
diff --git a/contrib/interface/debug_tac.ml4 b/contrib/interface/debug_tac.ml4 index 890bb3ce55..aad3a765de 100644 --- a/contrib/interface/debug_tac.ml4 +++ b/contrib/interface/debug_tac.ml4 @@ -113,7 +113,7 @@ let count_subgoals2 let rec local_interp : glob_tactic_expr -> report_holder -> tactic = function TacThens (a,l) -> (fun report_holder -> checked_thens report_holder a l) - | TacThen (a,b) -> + | TacThen (a,[||],b,[||]) -> (fun report_holder -> checked_then report_holder a b) | t -> (fun report_holder g -> @@ -279,7 +279,7 @@ let rec reconstruct_success_tac (tac:glob_tactic_expr) = | Failed n -> TacId [] | Tree_fail r -> reconstruct_success_tac a r | Mismatch (n,p) -> a) - | TacThen (a,b) -> + | TacThen (a,[||],b,[||]) -> (function Report_node(true, n, l) -> tac | Report_node(false, n, rl) -> @@ -340,7 +340,7 @@ Tacinterp.add_tactic "OnThen" on_then;; let rec clean_path tac l = match tac, l with - | TacThen (a,b), fst::tl -> + | TacThen (a,[||],b,[||]), fst::tl -> fst::(clean_path (if fst = 1 then a else b) tl) | TacThens (a,l), 1::tl -> 1::(clean_path a tl) @@ -390,7 +390,7 @@ let rec report_error | t::tl -> (report_error t the_goal the_ast returned_path (n::2::path)):: (fold_num (n + 1) tl) in fold_num 1 l) - | TacThen (a,b) -> + | TacThen (a,[||],b,[||]) -> let the_count = ref 1 in tclTHEN (fun g -> @@ -398,7 +398,7 @@ let rec report_error report_error a the_goal the_ast returned_path (1::path) g with e -> - (the_ast := TacThen (!the_ast, b); + (the_ast := TacThen (!the_ast,[||], b,[||]); raise e)) (fun g -> try diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml index d2f71bfc2f..b1809523c4 100644 --- a/contrib/interface/pbp.ml +++ b/contrib/interface/pbp.ml @@ -156,7 +156,7 @@ 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)) diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 57116c0709..6d52be45d9 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -775,10 +775,11 @@ and xlate_tactic = | TacFun (largs, t) -> let fst, rest = xlate_largs_to_id_opt largs in CT_tactic_fun (CT_id_opt_ne_list(fst, rest), xlate_tactic t) - | TacThen (t1,t2) -> + | TacThen (t1,[||],t2,[||]) -> (match xlate_tactic t1 with CT_then(a,l) -> CT_then(a,l@[xlate_tactic t2]) | t -> CT_then (t,[xlate_tactic t2])) + | TacThen _ -> xlate_error "TacThen generalization TODO" | TacThens(t1,[]) -> assert false | TacThens(t1,t::l) -> let ct = xlate_tactic t in |