diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/interface/xlate.ml | 22 | ||||
| -rw-r--r-- | contrib/setoid_ring/newring.ml4 | 4 |
2 files changed, 11 insertions, 15 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 6cc7942f8e..c261d57e97 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -775,11 +775,12 @@ and xlate_red_tactic = and xlate_local_rec_tac = function (* TODO LATER: local recursive tactics and global ones should be handled in the same manner *) - | ((_,x),(argl,tac)) -> + | ((_,x),Tacexp (TacFun (argl,tac))) -> let fst, rest = xlate_largs_to_id_opt argl in CT_rec_tactic_fun(xlate_ident x, CT_id_opt_ne_list(fst, rest), xlate_tactic tac) + | _ -> xlate_error "TODO: more general argument of 'let rec in'" and xlate_tactic = function @@ -837,36 +838,31 @@ and xlate_tactic = | TacMatchContext (false,true,rule1::rules) -> CT_match_context_reverse(xlate_context_rule rule1, List.map xlate_context_rule rules) - | TacLetIn (l, t) -> + | TacLetIn (false, l, t) -> let cvt_clause = function - ((_,s),None,ConstrMayEval v) -> + ((_,s),ConstrMayEval v) -> CT_let_clause(xlate_ident s, CT_coerce_NONE_to_TACTIC_OPT CT_none, CT_coerce_DEF_BODY_to_LET_VALUE (formula_to_def_body v)) - | ((_,s),None,Tacexp t) -> + | ((_,s),Tacexp t) -> CT_let_clause(xlate_ident s, CT_coerce_NONE_to_TACTIC_OPT CT_none, CT_coerce_TACTIC_COM_to_LET_VALUE (xlate_tactic t)) - | ((_,s),None,t) -> + | ((_,s),t) -> CT_let_clause(xlate_ident s, CT_coerce_NONE_to_TACTIC_OPT CT_none, CT_coerce_TACTIC_COM_to_LET_VALUE - (xlate_call_or_tacarg t)) - | ((_,s),Some c,t) -> - CT_let_clause(xlate_ident s, - CT_coerce_TACTIC_COM_to_TACTIC_OPT(xlate_tactic c), - CT_coerce_TACTIC_COM_to_LET_VALUE - (xlate_call_or_tacarg t)) in + (xlate_call_or_tacarg t)) in let cl_l = List.map cvt_clause l in (match cl_l with | [] -> assert false | fst::others -> CT_let_ltac (CT_let_clauses(fst, others), mk_let_value t)) - | TacLetRecIn([], _) -> xlate_error "recursive definition with no definition" - | TacLetRecIn(f1::l, t) -> + | TacLetIn(true, [], _) -> xlate_error "recursive definition with no definition" + | TacLetIn(true, f1::l, t) -> let tl = CT_rec_tactic_fun_list (xlate_local_rec_tac f1, List.map xlate_local_rec_tac l) in CT_rec_tactic_in(tl, xlate_tactic t) diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4 index 2c6e0ebcd4..6c3b6337af 100644 --- a/contrib/setoid_ring/newring.ml4 +++ b/contrib/setoid_ring/newring.ml4 @@ -771,7 +771,7 @@ let ring_lookup (f:glob_tactic_expr) lH rl t gl = let posttac = Tacexp(TacFun([None],e.ring_post_tac)) in Tacinterp.eval_tactic (TacLetIn - ([(dummy_loc,id_of_string"f"),None,Tacexp f], + (false,[(dummy_loc,id_of_string"f"),Tacexp f], ltac_lcall "f" [req;sth;ext;morph;th;cst_tac;pow_tac; lemma1;lemma2;pretac;posttac;lH;rl])) gl @@ -1112,7 +1112,7 @@ let field_lookup (f:glob_tactic_expr) lH rl t gl = let posttac = Tacexp(TacFun([None],e.field_post_tac)) in Tacinterp.eval_tactic (TacLetIn - ([(dummy_loc,id_of_string"f"),None,Tacexp f], + (false,[(dummy_loc,id_of_string"f"),Tacexp f], ltac_lcall "f" [req;cst_tac;pow_tac;field_ok;field_simpl_ok;field_simpl_eq_ok; field_simpl_eq_in_ok;cond_ok;pretac;posttac;lH;rl])) gl |