diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-09 15:25:58 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-09 15:25:58 +0000 |
| commit | a4be186e8ef56a0252450994251b51f97e31de25 (patch) | |
| tree | e088ca8fc627bcad14392eade405e53ac1b0ddd0 | |
| parent | 49356f9dd870d7d42e1e4ffbfc00906832197ef1 (diff) | |
Traduction semantique des InHyp de clause en InHypValue si local def
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4842 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/interface/xlate.ml | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 47370ef13..3d57d2485 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -401,10 +401,13 @@ let xlate_hyp = function let xlate_hyp_location = function - | InHyp (AI (_,id)) -> CT_coerce_ID_to_ID_OR_INTYPE (xlate_ident id) - | InHyp (MetaId _) -> xlate_error "MetaId should occur only in quotations" - | InHypType(AI (_, id)) -> CT_intype(xlate_ident id) - | InHypType _ -> xlate_error "MetaId not supported in xlate_hyp_location" + | AI (_,id), (InHypTypeOnly,_) -> CT_intype(xlate_ident id) + | AI (_,id), (InHyp,_) when !Options.v7 -> + CT_coerce_ID_to_ID_OR_INTYPE (xlate_ident id) + | AI (_,id), ((InHypValueOnly|InHyp),_) -> + xlate_error "TODO in v8: InHyp now means InHyp if variable but InHypValueOnly if a local definition" + | MetaId _, _ -> + xlate_error "MetaId not supported in xlate_hyp_location (should occur only in quotations)" let xlate_clause l = CT_id_or_intype_list (List.map xlate_hyp_location l) |