diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-10-01 09:41:57 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-10-01 09:41:57 +0000 |
| commit | f06fdb3f8d573345be82858966594200af84c83e (patch) | |
| tree | f90310c6db23c246f0696b1ba1064d0d1ca64f3b /contrib/interface/xlate.ml | |
| parent | 5fa0c98ea290cec817d233c7d25c2e874b5d41f1 (diff) | |
Une passe sur l'injection et la discrimination...
Efficacité:
- remplacement du typage par du re-typage léger
- suppression d'un pf_nf suspect (cf bug #1173) [quid de la compatibilité ?]
- remplacement des tests aveugles de projection impossible par un
test qui vérifie au fur et à mesure que les filtrages sont autorisés
Réorganisation:
- factorisation des parties communes de injEq/discrEq/decompEq
(à noter l'ordre inverse de génération des équations dans inj et decomp...)
- uniformisation des noms "e" et "ee" utilisés dans la construction des
combinateurs de discrimination
Extension:
- ajout d'une clause "as" à injection
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9195 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/interface/xlate.ml')
| -rw-r--r-- | contrib/interface/xlate.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index a7288de9a..de17ca0b6 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -939,6 +939,8 @@ and xlate_tac = CT_injection_eq (xlate_quantified_hypothesis_opt (out_gen (wit_opt rawwit_quant_hyp) idopt)) + | TacExtend (_,"injection_as", [idopt;ipat]) -> + xlate_error "TODO: injection as" | TacFix (idopt, n) -> CT_fixtactic (xlate_ident_opt idopt, CT_int n, CT_fix_tac_list []) | TacMutualFix (id, n, fixtac_list) -> |