diff options
| author | herbelin | 2004-03-02 07:04:56 +0000 |
|---|---|---|
| committer | herbelin | 2004-03-02 07:04:56 +0000 |
| commit | 8a1ddc270137f40cd8bbff20de4f41e284055891 (patch) | |
| tree | d3d41549bcd3cff2bbd0db1fb7824e05851941dd /contrib/interface | |
| parent | 1a29faa00f1e2a6f2d71088a769fe2fbc823244a (diff) | |
Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id variable de ltac substituable dans la pratique par un intro_case_pattern dans induction, destruct et inversion
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5415 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/xlate.ml | 21 |
1 files changed, 7 insertions, 14 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index f5507e722d..3f3f8c4d28 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -696,16 +696,9 @@ let xlate_lettac_clauses = function CT_unfold_list((CT_coerce_ID_to_UNFOLD(CT_ident "Goal"))::res) | None -> CT_unfold_list res;; -let xlate_intro_patt_list = function - [] -> CT_coerce_ID_OPT_to_INTRO_PATT_OPT ctv_ID_OPT_NONE - | (fp::ll) -> - CT_coerce_INTRO_PATT_to_INTRO_PATT_OPT - (CT_disj_pattern - (CT_intro_patt_list(List.map xlate_intro_pattern fp), - List.map - (fun l -> - CT_intro_patt_list(List.map xlate_intro_pattern l)) - ll));; +let xlate_intro_patt_opt = function + None -> CT_coerce_ID_OPT_to_INTRO_PATT_OPT ctv_ID_OPT_NONE + | Some fp -> CT_coerce_INTRO_PATT_to_INTRO_PATT_OPT (xlate_intro_pattern fp) let rec (xlate_tacarg:raw_tactic_arg -> ct_TACTIC_ARG) = function @@ -1155,12 +1148,12 @@ and xlate_tac = | (*For translating tactics/Inv.v *) TacInversion (NonDepInversion (k,idl,l),quant_hyp) -> CT_inversion(compute_INV_TYPE k, xlate_quantified_hypothesis quant_hyp, - xlate_intro_patt_list l, + xlate_intro_patt_opt l, CT_id_list (List.map xlate_hyp idl)) | TacInversion (DepInversion (k,copt,l),quant_hyp) -> let id = xlate_quantified_hypothesis quant_hyp in CT_depinversion (compute_INV_TYPE k, id, - xlate_intro_patt_list l, xlate_formula_opt copt) + xlate_intro_patt_opt l, xlate_formula_opt copt) | TacInversion (InversionUsing (c,idlist), id) -> let id = xlate_quantified_hypothesis id in CT_use_inversion (id, xlate_formula c, @@ -1174,11 +1167,11 @@ and xlate_tac = | TacNewDestruct(a,b,(c,_)) -> CT_new_destruct (xlate_int_or_constr a, xlate_using b, - xlate_intro_patt_list c) + xlate_intro_patt_opt c) | TacNewInduction(a,b,(c,_)) -> CT_new_induction (xlate_int_or_constr a, xlate_using b, - xlate_intro_patt_list c) + xlate_intro_patt_opt c) | TacInstantiate (a, b, cl) -> CT_instantiate(CT_int a, xlate_formula b, xlate_clause cl) |