diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-10-21 19:59:24 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-10-21 19:59:24 +0000 |
| commit | 59e3d9cb722b305802869941256415083eb4765d (patch) | |
| tree | 67ed2759a31830dbadf04525be3ff0d07ac14102 /parsing/q_coqast.ml4 | |
| parent | b19a4f3e8a785247ccb7d5b7464c15ccd4c3b3ce (diff) | |
Ajout d'un suffixe "as [ names ]" pour nommer manuellement les
variables introduites par NewDestruct et NewInduction
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3169 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/q_coqast.ml4')
| -rw-r--r-- | parsing/q_coqast.ml4 | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index ac9726106..086eed8a5 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -355,14 +355,16 @@ let rec mlexpr_of_atomic_tactic = function (* Derived basic tactics *) | Tacexpr.TacOldInduction h -> <:expr< Tacexpr.TacOldInduction $mlexpr_of_quantified_hypothesis h$ >> - | Tacexpr.TacNewInduction (c,cbo) -> + | Tacexpr.TacNewInduction (c,cbo,ids) -> let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in - <:expr< Tacexpr.TacNewInduction $mlexpr_of_induction_arg c$ $cbo$ >> + let ids = mlexpr_of_list (mlexpr_of_list mlexpr_of_ident) ids in + <:expr< Tacexpr.TacNewInduction $mlexpr_of_induction_arg c$ $cbo$ $ids$>> | Tacexpr.TacOldDestruct h -> <:expr< Tacexpr.TacOldDestruct $mlexpr_of_quantified_hypothesis h$ >> - | Tacexpr.TacNewDestruct (c,cbo) -> + | Tacexpr.TacNewDestruct (c,cbo,ids) -> let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in - <:expr< Tacexpr.TacNewDestruct $mlexpr_of_induction_arg c$ $cbo$ >> + let ids = mlexpr_of_list (mlexpr_of_list mlexpr_of_ident) ids in + <:expr< Tacexpr.TacNewDestruct $mlexpr_of_induction_arg c$ $cbo$ $ids$ >> (* Context management *) | Tacexpr.TacClear l -> |