diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-12 15:33:19 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-12 15:33:19 +0000 |
| commit | 7db3c187811a21761c7d13f4b5de8562eb59b5a9 (patch) | |
| tree | 0bf238c943bbba36095e9594cbaea95b69e650f4 | |
| parent | e8dc97576d5643e0ef8dd3eeec99c25c6d483c39 (diff) | |
Correction parser révélé par test-suite
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11114 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/interface/xlate.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index fa8f05713..7d1f57fe1 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -478,7 +478,7 @@ let xlate_hyp_location = CT_intype(xlate_ident id, nums_or_var_to_int_list (nums_of_occs occs)) | (occs, AI (_,id)), InHypValueOnly -> CT_invalue(xlate_ident id, nums_or_var_to_int_list (nums_of_occs occs)) - | ((true,[]), AI (_,id)), InHyp -> + | (occs, AI (_,id)), InHyp when occs = all_occurrences_expr -> CT_coerce_UNFOLD_to_HYP_LOCATION (CT_coerce_ID_to_UNFOLD (xlate_ident id)) | ((_,a::l as occs), AI (_,id)), InHyp -> @@ -488,7 +488,7 @@ let xlate_hyp_location = (CT_unfold_occ (xlate_ident id, CT_int_ne_list(num_or_var_to_int a, nums_or_var_to_int_list_aux l))) - | ((false,[]), AI (_,id)), InHyp -> xlate_error "Unused" + | (_, AI (_,id)), InHyp -> xlate_error "Unused" (* (true,]) *) | (_, MetaId _),_ -> xlate_error "MetaId not supported in xlate_hyp_location (should occur only in quotations)" |