diff options
Diffstat (limited to 'parsing/q_coqast.ml4')
| -rw-r--r-- | parsing/q_coqast.ml4 | 24 |
1 files changed, 14 insertions, 10 deletions
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 6e3b3f35..02311fe4 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -343,11 +343,13 @@ let rec mlexpr_of_atomic_tactic = function (mlexpr_of_pair mlexpr_of_occ_constr mlexpr_of_name) cl$ >> | Tacexpr.TacGeneralizeDep c -> <:expr< Tacexpr.TacGeneralizeDep $mlexpr_of_constr c$ >> - | Tacexpr.TacLetTac (na,c,cl,b) -> + | Tacexpr.TacLetTac (na,c,cl,b,e) -> let na = mlexpr_of_name na in let cl = mlexpr_of_clause_pattern cl in <:expr< Tacexpr.TacLetTac $na$ $mlexpr_of_constr c$ $cl$ - $mlexpr_of_bool b$ >> + $mlexpr_of_bool b$ + (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern) e) + >> (* Derived basic tactics *) | Tacexpr.TacSimpleInductionDestruct (isrec,h) -> @@ -355,13 +357,15 @@ let rec mlexpr_of_atomic_tactic = function $mlexpr_of_quantified_hypothesis h$ >> | Tacexpr.TacInductionDestruct (isrec,ev,l) -> <:expr< Tacexpr.TacInductionDestruct $mlexpr_of_bool isrec$ $mlexpr_of_bool ev$ - $mlexpr_of_pair (mlexpr_of_list (mlexpr_of_triple - (mlexpr_of_list mlexpr_of_induction_arg) - (mlexpr_of_option mlexpr_of_constr_with_binding) - (mlexpr_of_pair - (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern)) - (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern))))) - (mlexpr_of_option mlexpr_of_clause) l$ >> + $mlexpr_of_triple + (mlexpr_of_list + (mlexpr_of_pair + mlexpr_of_induction_arg + (mlexpr_of_pair + (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern)) + (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern))))) + (mlexpr_of_option mlexpr_of_constr_with_binding) + (mlexpr_of_option mlexpr_of_clause) l$ >> (* Context management *) | Tacexpr.TacClear (b,l) -> |