From f06fdb3f8d573345be82858966594200af84c83e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 1 Oct 2006 09:41:57 +0000
Subject: 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
---
 contrib/interface/xlate.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'contrib/interface')

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index a7288de9a7..de17ca0b67 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) ->
-- 
cgit v1.2.3