diff options
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/ascent.mli | 6 | ||||
| -rw-r--r-- | contrib/interface/vtp.ml | 9 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 16 |
3 files changed, 17 insertions, 14 deletions
diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli index 1f9fec6d58..456b00ea99 100644 --- a/contrib/interface/ascent.mli +++ b/contrib/interface/ascent.mli @@ -402,8 +402,8 @@ and ct_PREMISE_PATTERN = and ct_PROOF_SCRIPT = CT_proof_script of ct_COMMAND list and ct_RECCONSTR = - CT_coerce_CONSTR_to_RECCONSTR of ct_CONSTR - | CT_constr_coercion of ct_ID * ct_FORMULA + CT_coerce_CONSTR_to_RECCONSTR of ct_ID_OPT * ct_FORMULA + | CT_constr_coercion of ct_ID_OPT * ct_FORMULA and ct_RECCONSTR_LIST = CT_recconstr_list of ct_RECCONSTR list and ct_REC_TACTIC_FUN = @@ -526,7 +526,7 @@ and ct_TACTIC_COM = | CT_inversion of ct_INV_TYPE * ct_ID_OR_INT * ct_ID_LIST | CT_left of ct_SPEC_LIST | CT_let_ltac of ct_LET_CLAUSES * ct_LET_VALUE - | CT_lettac of ct_ID * ct_FORMULA * ct_CLAUSE + | CT_lettac of ct_ID_OPT * ct_FORMULA * ct_CLAUSE | 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_TACTIC_COM * ct_MATCH_TAC_RULES diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml index 5d7cff4cf5..9f8ece9b23 100644 --- a/contrib/interface/vtp.ml +++ b/contrib/interface/vtp.ml @@ -910,9 +910,12 @@ and fPROOF_SCRIPT = function (List.iter fCOMMAND l); fNODE "proof_script" (List.length l) and fRECCONSTR = function -| CT_coerce_CONSTR_to_RECCONSTR x -> fCONSTR x +| CT_coerce_CONSTR_to_RECCONSTR (x1,x2) -> + fID_OPT x1; + fFORMULA x2; + fNODE "CONSTR_to_RECCONSTR" 2 | CT_constr_coercion(x1, x2) -> - fID x1; + fID_OPT x1; fFORMULA x2; fNODE "constr_coercion" 2 and fRECCONSTR_LIST = function @@ -1244,7 +1247,7 @@ and fTACTIC_COM = function fLET_VALUE x2; fNODE "let_ltac" 2 | CT_lettac(x1, x2, x3) -> - fID x1; + fID_OPT x1; fFORMULA x2; fCLAUSE x3; fNODE "lettac" 3 diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 35357d3ab7..7cf169ec7d 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1022,8 +1022,8 @@ and xlate_tac = | TacInstantiate (a, b, _) -> xlate_error "TODO: Instantiate ... <clause>" - | TacLetTac (id, c, cl) -> - CT_lettac(xlate_ident id, xlate_formula c, + | TacLetTac (na, c, cl) -> + CT_lettac(xlate_id_opt ((0,0),na), xlate_formula c, (* TODO LATER: This should be shared with Unfold, but the structures are different *) xlate_clause cl) @@ -1032,8 +1032,8 @@ and xlate_tac = CT_pose(xlate_id_opt ((0,0), name), xlate_formula c) | TacForward (false, name, c) -> CT_assert(xlate_id_opt ((0,0),name), xlate_formula c) - | TacTrueCut (idopt, c) -> - CT_truecut(xlate_ident_opt idopt, xlate_formula c) + | TacTrueCut (na, c) -> + CT_truecut(xlate_id_opt ((0,0),na), xlate_formula c) | TacAnyConstructor(Some tac) -> CT_any_constructor (CT_coerce_TACTIC_COM_to_TACTIC_OPT(xlate_tactic tac)) @@ -1250,12 +1250,12 @@ let build_constructors l = let build_record_field_list l = let build_record_field (coe,d) = match d with - | AssumExpr ((_,id),c) -> - if coe then CT_constr_coercion (xlate_ident id, xlate_formula c) + | AssumExpr (id,c) -> + if coe then CT_constr_coercion (xlate_id_opt id, xlate_formula c) else CT_coerce_CONSTR_to_RECCONSTR - (CT_constr (xlate_ident id, xlate_formula c)) - | DefExpr ((_,id),c,topt) -> + (xlate_id_opt id, xlate_formula c) + | DefExpr (id,c,topt) -> xlate_error "TODO: manifest fields in Record" in CT_recconstr_list (List.map build_record_field l);; |