diff options
| author | herbelin | 2008-06-29 16:27:16 +0000 |
|---|---|---|
| committer | herbelin | 2008-06-29 16:27:16 +0000 |
| commit | 110db6ddf023c98a76c719caf602559942ba089e (patch) | |
| tree | 7529b263aae3ff3f1466ba3d40bd6a575ea8dee3 /contrib/interface | |
| parent | 6735186e6458fedd57efd663c900166af0d6fce3 (diff) | |
Correction bug "parser" suite changement syntaxe
discriminate/injection/simplify_eq.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11189 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/xlate.ml | 29 |
1 files changed, 16 insertions, 13 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 07cc101889..8b805cc26b 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -928,23 +928,26 @@ and xlate_tac = | TacExtend (_,"contradiction",[]) -> CT_contradiction | TacDoubleInduction (n1, n2) -> CT_tac_double (xlate_quantified_hypothesis n1, xlate_quantified_hypothesis n2) - | TacExtend (_,"discriminate", [idopt]) -> + | TacExtend (_,"discriminate", []) -> + CT_discriminate_eq (CT_coerce_ID_OPT_to_ID_OR_INT_OPT ctv_ID_OPT_NONE) + | TacExtend (_,"discriminate", [id]) -> CT_discriminate_eq (xlate_quantified_hypothesis_opt - (out_gen (wit_opt rawwit_quant_hyp) idopt)) - | TacExtend (_,"simplify_eq", [idopt]) -> - let idopt1 = out_gen (wit_opt rawwit_quant_hyp) idopt in - let idopt2 = match idopt1 with - None -> CT_coerce_ID_OPT_to_ID_OR_INT_OPT - (CT_coerce_NONE_to_ID_OPT CT_none) - | Some v -> - CT_coerce_ID_OR_INT_to_ID_OR_INT_OPT - (xlate_quantified_hypothesis v) in - CT_simplify_eq idopt2 - | TacExtend (_,"injection", [idopt]) -> + (Some (out_gen rawwit_quant_hyp id))) + | TacExtend (_,"simplify_eq", []) -> + CT_simplify_eq (CT_coerce_ID_OPT_to_ID_OR_INT_OPT + (CT_coerce_NONE_to_ID_OPT CT_none)) + | TacExtend (_,"simplify_eq", [id]) -> + let id1 = out_gen rawwit_quant_hyp id in + let id2 = CT_coerce_ID_OR_INT_to_ID_OR_INT_OPT + (xlate_quantified_hypothesis id1) in + CT_simplify_eq id2 + | TacExtend (_,"injection", []) -> + CT_injection_eq (CT_coerce_ID_OPT_to_ID_OR_INT_OPT ctv_ID_OPT_NONE) + | TacExtend (_,"injection", [id]) -> CT_injection_eq (xlate_quantified_hypothesis_opt - (out_gen (wit_opt rawwit_quant_hyp) idopt)) + (Some (out_gen rawwit_quant_hyp id))) | TacExtend (_,"injection_as", [idopt;ipat]) -> xlate_error "TODO: injection as" | TacFix (idopt, n) -> |