diff options
| author |  bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-11-14 13:27:07 +0000 |
|---|---|---|
| committer | bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-11-14 13:27:07 +0000 |
| commit | 67df3e8485ad7ce4a4f4ba38e9abcc3b6b18759b (patch) | |
| tree | 5c2563f71615c78d8f72fa846962794b78b6f7de /contrib/interface | |
| parent | 7b724fa3c22ccffba5ed0e2694c837879527a32a (diff) | |
adds the the case VernacShow(ShowMatch _) in the pattern-matching construct,
but only maps to an error message. Avoid warnings about unused variables.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7561 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/xlate.ml | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index e860b987a..391cc0f7c 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -399,9 +399,6 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function xlate_id_opt_ne_list l, xlate_formula c, xlate_formula b) | COrderedCase (_,c,v,e,l) -> - let case_string = match c with - Term.MatchStyle -> "Match" - | _ -> "Case" in CT_elimc(CT_case "Case", xlate_formula_opt v, xlate_formula e, CT_formula_list(List.map xlate_formula l)) | CSort(_, s) -> CT_coerce_SORT_TYPE_to_FORMULA(xlate_sort s) @@ -1520,11 +1517,11 @@ let rec xlate_module_type = function let mty1 = xlate_module_type mty in (match decl with CWith_Definition((_, idl), c) -> - CT_module_type_with_def(xlate_module_type mty, + CT_module_type_with_def(mty1, CT_id_list (List.map xlate_ident idl), xlate_formula c) | CWith_Module((_, idl), (_, qid)) -> - CT_module_type_with_mod(xlate_module_type mty, + CT_module_type_with_mod(mty1, CT_id_list (List.map xlate_ident idl), CT_ident (xlate_qualid qid)));; @@ -1768,6 +1765,7 @@ let rec xlate_vernac = | VernacShow (ShowGoalImplicitly (Some n)) -> CT_show_implicit (CT_int n) | VernacShow ShowExistentials -> CT_show_existentials | VernacShow ShowScript -> CT_show_script + | VernacShow(ShowMatch _) -> xlate_error "TODO: VernacShow(ShowMatch _)" | VernacGo arg -> CT_go (xlate_locn arg) | VernacShow ExplainProof l -> CT_explain_proof (nums_to_int_list l) | VernacShow ExplainTree l -> |