diff options
Diffstat (limited to 'contrib/interface/vtp.ml')
| -rw-r--r-- | contrib/interface/vtp.ml | 25 |
1 files changed, 19 insertions, 6 deletions
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml index ff418523..5a7ccc26 100644 --- a/contrib/interface/vtp.ml +++ b/contrib/interface/vtp.ml @@ -407,6 +407,9 @@ and fCOMMAND = function fNODE "print_about" 1 | CT_print_all -> fNODE "print_all" 0 | CT_print_classes -> fNODE "print_classes" 0 +| CT_print_ltac id -> + fID id; + fNODE "print_ltac" 1 | CT_print_coercions -> fNODE "print_coercions" 0 | CT_print_grammar(x1) -> fGRAMMAR x1; @@ -418,6 +421,9 @@ and fCOMMAND = function | CT_print_hintdb(x1) -> fID_OR_STAR x1; fNODE "print_hintdb" 1 +| CT_print_rewrite_hintdb(x1) -> + fID x1; + fNODE "print_rewrite_hintdb" 1 | CT_print_id(x1) -> fID x1; fNODE "print_id" 1 @@ -451,6 +457,7 @@ and fCOMMAND = function | CT_print_scope(x1) -> fID x1; fNODE "print_scope" 1 +| CT_print_setoids -> fNODE "print_setoids" 0 | CT_print_scopes -> fNODE "print_scopes" 0 | CT_print_section(x1) -> fID x1; @@ -1153,12 +1160,12 @@ and fMODULE_TYPE = function | CT_coerce_ID_to_MODULE_TYPE x -> fID x | CT_module_type_with_def(x1, x2, x3) -> fMODULE_TYPE x1; - fID x2; + fID_LIST x2; fFORMULA x3; fNODE "module_type_with_def" 3 | CT_module_type_with_mod(x1, x2, x3) -> fMODULE_TYPE x1; - fID x2; + fID_LIST x2; fID x3; fNODE "module_type_with_mod" 3 and fMODULE_TYPE_CHECK = function @@ -1281,6 +1288,7 @@ and fRED_COM = function fPATTERN_NE_LIST x1; fNODE "pattern" 1 | CT_red -> fNODE "red" 0 +| CT_cbvvm -> fNODE "vm_compute" 0 | CT_simpl(x1) -> fPATTERN_OPT x1; fNODE "simpl" 1 @@ -1545,6 +1553,9 @@ and fTACTIC_COM = function | CT_exact(x1) -> fFORMULA x1; fNODE "exact" 1 +| CT_exact_no_check(x1) -> + fFORMULA x1; + fNODE "exact_no_check" 1 | CT_exists(x1) -> fSPEC_LIST x1; fNODE "exists" 1 @@ -1649,12 +1660,12 @@ and fTACTIC_COM = function fID x2; fNODE "move_after" 2 | CT_new_destruct(x1, x2, x3) -> - fFORMULA_OR_INT x1; + (List.iter fFORMULA_OR_INT x1); (* Julien F. Est-ce correct? *) fUSING x2; fINTRO_PATT_OPT x3; fNODE "new_destruct" 3 | CT_new_induction(x1, x2, x3) -> - fFORMULA_OR_INT x1; + (List.iter fFORMULA_OR_INT x1); (* Pierre C. Est-ce correct? *) fUSING x2; fINTRO_PATT_OPT x3; fNODE "new_induction" 3 @@ -1697,10 +1708,12 @@ and fTACTIC_COM = function | CT_repeat(x1) -> fTACTIC_COM x1; fNODE "repeat" 1 -| CT_replace_with(x1, x2) -> +| CT_replace_with(x1, x2,x3,x4) -> fFORMULA x1; fFORMULA x2; - fNODE "replace_with" 2 + fID_OPT x3; + fTACTIC_OPT x4; + fNODE "replace_with" 4 | CT_rewrite_lr(x1, x2, x3) -> fFORMULA x1; fSPEC_LIST x2; |