Modification of VernacScheme to handle a new scheme: Equality (equality in

boolean, will be added later) and update so everything is fine with the new
syntax. 

New Type:

type scheme =
  | InductionScheme of bool * lreference * sort_expr
  | EqualityScheme of lreference
...
  | VernacScheme of (lident * scheme) list



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9860 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 22 insertions, 2 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 6fd56536b9..6c4fe20571 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -648,8 +648,15 @@ let build_corecursive l b =
   interp_recursive IsCoFixpoint fixl b
 
 (* 3d| Schemes *)
-
-let build_scheme lnamedepindsort = 
+let rec split_scheme = function
+  | [] -> [],[]
+  | (id,t)::q -> let l1,l2 = split_scheme q in 
+    ( match t with
+      | InductionScheme (x,y,z) -> ((id,x,y,z)::l1),l2
+      | EqualityScheme  x -> l1,((id,x)::l2)
+    )
+
+let build_induction_scheme lnamedepindsort = 
   let lrecnames = List.map (fun ((_,f),_,_,_) -> f) lnamedepindsort
   and sigma = Evd.empty
   and env0 = Global.env() in
@@ -675,6 +682,19 @@ let build_scheme lnamedepindsort =
   let _ = List.fold_right2 declare listdecl lrecnames [] in
   if_verbose ppnl (recursive_message Fixpoint lrecnames)
 
+let build_scheme l = 
+  let ischeme,escheme = split_scheme l in
+    if (ischeme <> []) && (escheme <> []) 
+    then
+      error "Do not declare equality and induction scheme at the same time."
+    else (
+      if ischeme <> [] then build_induction_scheme ischeme;
+    List.iter ( fun (_,eq)-> let ind = Nametab.global_inductive eq
+(* vsiles :This will be replace with the boolean when it will be commited *)
+      in Pp.msgnl (print_constr (mkInd ind))
+    ) escheme
+  )
+
 let rec get_concl n t = 
   if n = 0 then t
   else