diff options
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/ascent.mli | 4 | ||||
| -rw-r--r-- | contrib/interface/vtp.ml | 4 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 12 |
3 files changed, 9 insertions, 11 deletions
diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli index 428606be7..84c07dc71 100644 --- a/contrib/interface/ascent.mli +++ b/contrib/interface/ascent.mli @@ -338,7 +338,7 @@ and ct_IN_OR_OUT_MODULES = | CT_in_modules of ct_ID_NE_LIST | CT_out_modules of ct_ID_NE_LIST and ct_LET_CLAUSE = - CT_let_clause of ct_ID * ct_DEF_BODY_OPT * ct_LET_VALUE + CT_let_clause of ct_ID * ct_TACTIC_OPT * ct_LET_VALUE and ct_LET_CLAUSES = CT_let_clauses of ct_LET_CLAUSE * ct_LET_CLAUSE list and ct_LET_VALUE = @@ -524,7 +524,7 @@ and ct_TACTIC_COM = | CT_lettac of ct_ID * ct_FORMULA * ct_UNFOLD_LIST | CT_match_context of ct_CONTEXT_RULE * ct_CONTEXT_RULE list | CT_match_context_reverse of ct_CONTEXT_RULE * ct_CONTEXT_RULE list - | CT_match_tac of ct_LET_VALUE * ct_MATCH_TAC_RULES + | CT_match_tac of ct_TACTIC_COM * ct_MATCH_TAC_RULES | CT_move_after of ct_ID * ct_ID | CT_new_destruct of ct_FORMULA_OR_INT * ct_USING * ct_ID_LIST_LIST | CT_new_induction of ct_FORMULA_OR_INT * ct_USING * ct_ID_LIST_LIST diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml index df83a0499..677f7edc9 100644 --- a/contrib/interface/vtp.ml +++ b/contrib/interface/vtp.ml @@ -795,7 +795,7 @@ and fIN_OR_OUT_MODULES = function and fLET_CLAUSE = function | CT_let_clause(x1, x2, x3) -> fID x1; - fDEF_BODY_OPT x2; + fTACTIC_OPT x2; fLET_VALUE x3; fNODE "let_clause" 3 and fLET_CLAUSES = function @@ -1243,7 +1243,7 @@ and fTACTIC_COM = function (List.iter fCONTEXT_RULE l); fNODE "match_context_reverse" (1 + (List.length l)) | CT_match_tac(x1, x2) -> - fLET_VALUE x1; + fTACTIC_COM x1; fMATCH_TAC_RULES x2; fNODE "match_tac" 2 | CT_move_after(x1, x2) -> diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 02300fdfd..6fd12a010 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -710,7 +710,7 @@ and xlate_tactic = | TacProgress t -> CT_progress(xlate_tactic t) | TacOrelse(t1,t2) -> CT_orelse(xlate_tactic t1, xlate_tactic t2) | TacMatch (exp, rules) -> - CT_match_tac(CT_coerce_DEF_BODY_to_LET_VALUE(formula_to_def_body exp), + CT_match_tac(xlate_tactic exp, match List.map (function | Pat ([],p,tac) -> @@ -737,23 +737,22 @@ and xlate_tactic = function ((_,s),None,ConstrMayEval v) -> CT_let_clause(xlate_ident s, - ctv_DEF_BODY_OPT_NONE, + CT_coerce_NONE_to_TACTIC_OPT CT_none, CT_coerce_DEF_BODY_to_LET_VALUE (formula_to_def_body v)) | ((_,s),None,Tacexp t) -> CT_let_clause(xlate_ident s, - ctv_DEF_BODY_OPT_NONE, + CT_coerce_NONE_to_TACTIC_OPT CT_none, CT_coerce_TACTIC_COM_to_LET_VALUE (xlate_tactic t)) | ((_,s),None,t) -> CT_let_clause(xlate_ident s, - ctv_DEF_BODY_OPT_NONE, + 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_DEF_BODY_to_DEF_BODY_OPT - (formula_to_def_body c), + CT_coerce_TACTIC_COM_to_TACTIC_OPT(xlate_tactic c), CT_coerce_TACTIC_COM_to_LET_VALUE (xlate_call_or_tacarg t)) in let cl_l = List.map cvt_clause l in @@ -761,7 +760,6 @@ and xlate_tactic = | [] -> assert false | fst::others -> CT_let_ltac (CT_let_clauses(fst, others), mk_let_value t)) - | TacLetCut _ -> xlate_error "Unclear future of syntax Let x := t" | TacLetRecIn([], _) -> xlate_error "recursive definition with no definition" | TacLetRecIn(f1::l, t) -> let tl = CT_rec_tactic_fun_list |