diff options
Diffstat (limited to 'parsing/q_coqast.ml4')
| -rw-r--r-- | parsing/q_coqast.ml4 | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 57ca81de38..84efdbcac1 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -389,18 +389,18 @@ let rec mlexpr_of_atomic_tactic = function <:expr< Tacexpr.TacLetTac $id$ $mlexpr_of_constr c$ $cl$ >> (* Derived basic tactics *) - | Tacexpr.TacSimpleInduction h -> - <:expr< Tacexpr.TacSimpleInduction $mlexpr_of_quantified_hypothesis h$ >> + | Tacexpr.TacSimpleInduction (h,_) -> + <:expr< Tacexpr.TacSimpleInduction ($mlexpr_of_quantified_hypothesis h$,ref []) >> | Tacexpr.TacNewInduction (c,cbo,ids) -> let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in - let ids = mlexpr_of_list (mlexpr_of_list mlexpr_of_intro_pattern) ids in - <:expr< Tacexpr.TacNewInduction $mlexpr_of_induction_arg c$ $cbo$ $ids$>> + let ids = mlexpr_of_list (mlexpr_of_list mlexpr_of_intro_pattern) (fst ids) in + <:expr< Tacexpr.TacNewInduction $mlexpr_of_induction_arg c$ $cbo$ ($ids$,ref [])>> | Tacexpr.TacSimpleDestruct h -> <:expr< Tacexpr.TacSimpleDestruct $mlexpr_of_quantified_hypothesis h$ >> | Tacexpr.TacNewDestruct (c,cbo,ids) -> let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in - let ids = mlexpr_of_list (mlexpr_of_list mlexpr_of_intro_pattern) ids in - <:expr< Tacexpr.TacNewDestruct $mlexpr_of_induction_arg c$ $cbo$ $ids$ >> + let ids = mlexpr_of_list (mlexpr_of_list mlexpr_of_intro_pattern) (fst ids) in + <:expr< Tacexpr.TacNewDestruct $mlexpr_of_induction_arg c$ $cbo$ ($ids$,ref []) >> (* Context management *) | Tacexpr.TacClear l -> |