diff options
| author |  vsiles <vsiles@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-09-28 09:59:12 +0000 |
|---|---|---|
| committer | vsiles <vsiles@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-09-28 09:59:12 +0000 |
| commit | 104471118454580c3ca4b2a3cce52a03263e5d15 (patch) | |
| tree | 0af98148e169638789c3d97f3c38ecef73492a24 /contrib/interface | |
| parent | 3d0f2b7ecfb78308bbb17d135fcceefd121f7624 (diff) | |
Modification of the Scheme command.
Now you can forget to provide the name of the scheme, it will be
built automatically depending of the sorts involved.
e.g. Scheme Induction for nat Sort Set.
will build nat_rec
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10148 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/xlate.ml | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index af68c7cf9..fdaa2c596 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1940,12 +1940,17 @@ let rec xlate_vernac = | VernacScheme [] -> xlate_error "induction scheme" | VernacScheme (lm :: lmi) -> let strip_ind = function - | ((_,id), InductionScheme (depstr, inde, sort)) -> + | (Some (_,id), InductionScheme (depstr, inde, sort)) -> CT_scheme_spec (xlate_ident id, xlate_dep depstr, CT_coerce_ID_to_FORMULA (loc_qualid_to_ct_ID inde), xlate_sort sort) - | ((_,id), EqualityScheme _) -> xlate_error "TODO: Scheme Equality" in + | (None, InductionScheme (depstr, inde, sort)) -> + CT_scheme_spec + (xlate_ident (id_of_string ""), xlate_dep depstr, + CT_coerce_ID_to_FORMULA (loc_qualid_to_ct_ID inde), + xlate_sort sort) + | (_, EqualityScheme _) -> xlate_error "TODO: Scheme Equality" in CT_ind_scheme (CT_scheme_spec_list (strip_ind lm, List.map strip_ind lmi)) | VernacCombinedScheme _ -> xlate_error "TODO: Combined Scheme" |