From 104471118454580c3ca4b2a3cce52a03263e5d15 Mon Sep 17 00:00:00 2001
From: vsiles
Date: Fri, 28 Sep 2007 09:59:12 +0000
Subject: 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
---
 contrib/interface/xlate.ml | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

(limited to 'contrib/interface')

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index af68c7cf91..fdaa2c5964 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"
-- 
cgit v1.2.3