diff options
| author | msozeau | 2007-01-29 12:20:10 +0000 |
|---|---|---|
| committer | msozeau | 2007-01-29 12:20:10 +0000 |
| commit | 72b9b70181ed0b1880ab296ef2eb01d557a676c6 (patch) | |
| tree | 60b7e47e2c01354f6427438b90c384427bb77221 /contrib/interface | |
| parent | 8878a1974cf41ea40e411785d1197f2722a50445 (diff) | |
Coqdoc patch for Program, fix xlate.ml warning and little subtac fixes.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9550 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/xlate.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 5224190301..bf5aed32e8 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1929,6 +1929,7 @@ let rec xlate_vernac = xlate_sort sort) in CT_ind_scheme (CT_scheme_spec_list (strip_ind lm, List.map strip_ind lmi)) + | VernacCombinedScheme _ -> xlate_error "TODO: Combined Scheme" | VernacSyntacticDefinition (id, c, false, _) -> CT_syntax_macro (xlate_ident id, xlate_formula c, xlate_int_opt None) | VernacSyntacticDefinition (id, c, true, _) -> |