debug discharge et inductifs

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

10 files changed, 52 insertions, 56 deletions

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 6ae5bb931d..e46be516a6 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -133,7 +133,7 @@ let check_params nparams params c =
   try
     List.iter2 
       (fun (n1,t1) (n2,t2) ->
-	 if n1 <> n2 || strip_outer_cast t1 <> strip_outer_cast t2 then
+	 if n1 <> n2 || strip_all_casts t1 <> strip_all_casts t2 then
 	   raise (InductiveError BadEntry))
       eparams params
   with Invalid_argument _ ->
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index cbc3fe343e..195b4ce18f 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -1309,39 +1309,3 @@ let rec whd_ise1_metas sigma = function
   | DOP2(Cast,c,_) -> whd_ise1_metas sigma c
   | c -> c
 
-
-(* Fonction spéciale qui laisse les cast clés sous les Fix ou les MutCase *)
-
-let under_outer_cast f = function
-  | DOP2 (Cast,b,t) -> DOP2 (Cast,f b,f t)
-  | c -> f c
-
-let rec strip_all_casts t = 
-  match t with
-    | DOP2 (Cast, b, _) -> strip_all_casts b
-    | DOP0 _ as t -> t
-    (* Cas ad hoc *)
-    | DOPN(Fix _ as f,v) -> 
-	let n = Array.length v in
-	let ts = Array.sub v 0 (n-1) in
-	let b = v.(n-1) in 
-	DOPN(f, Array.append 
-	       (Array.map strip_all_casts ts)
-	       [|under_outer_cast strip_all_casts b|])
-    | DOPN(CoFix _ as f,v) -> 
-	let n = Array.length v in
-	let ts = Array.sub v 0 (n-1) in
-	let b = v.(n-1) in 
-	DOPN(f, Array.append 
-	       (Array.map strip_all_casts ts)
-	       [|under_outer_cast strip_all_casts b|])
-    | DOP1(oper,c) -> DOP1(oper,strip_all_casts c)
-    | DOP2(oper,c1,c2) -> DOP2(oper,strip_all_casts c1,strip_all_casts c2)
-    | DOPN(oper,cl) -> DOPN(oper,Array.map strip_all_casts cl)
-    | DOPL(oper,cl) -> DOPL(oper,List.map strip_all_casts cl)
-    | DLAM(na,c) -> DLAM(na,strip_all_casts c)
-    | DLAMV(na,c) -> DLAMV(na,Array.map (under_outer_cast strip_all_casts) c)
-    | VAR _ as t -> t
-    | Rel _ as t -> t
-
-
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 572d4bcff9..dd06af8adc 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -206,7 +206,3 @@ val find_mcoinductype :
 val check_mrectype_spec : env -> 'a evar_map -> constr -> constr
 val minductype_spec : env -> 'a evar_map -> constr -> constr
 val mrectype_spec : env -> 'a evar_map -> constr -> constr
-
-(* Special function, which keep the key casts under Fix and MutCase. *)
-
-val strip_all_casts : constr -> constr
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index a4cde03717..6722b023fb 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -367,7 +367,7 @@ let type_one_constructor env_ar nparams ar c =
     | Prop _ -> cst
   in
   let (j,cst'') = safe_machine env_ar c in
-  let issmall = is_small_type env_par c in
+  let issmall = is_small_type env_par dc in
   ((issmall,j), Constraint.union cst' cst'')
 
 let logic_constr env c =
diff --git a/kernel/term.ml b/kernel/term.ml
index 8e9c94c711..31e52ebb3f 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -331,6 +331,42 @@ let rec strip_outer_cast = function
   | DOP2(Cast,c,_) -> strip_outer_cast c
   | c -> c
 
+
+
+(* Fonction spéciale qui laisse les cast clés sous les Fix ou les MutCase *)
+
+let under_outer_cast f = function
+  | DOP2 (Cast,b,t) -> DOP2 (Cast,f b,f t)
+  | c -> f c
+
+let rec strip_all_casts t = 
+  match t with
+    | DOP2 (Cast, b, _) -> strip_all_casts b
+    | DOP0 _ as t -> t
+    (* Cas ad hoc *)
+    | DOPN(Fix _ as f,v) -> 
+	let n = Array.length v in
+	let ts = Array.sub v 0 (n-1) in
+	let b = v.(n-1) in 
+	DOPN(f, Array.append 
+	       (Array.map strip_all_casts ts)
+	       [|under_outer_cast strip_all_casts b|])
+    | DOPN(CoFix _ as f,v) -> 
+	let n = Array.length v in
+	let ts = Array.sub v 0 (n-1) in
+	let b = v.(n-1) in 
+	DOPN(f, Array.append 
+	       (Array.map strip_all_casts ts)
+	       [|under_outer_cast strip_all_casts b|])
+    | DOP1(oper,c) -> DOP1(oper,strip_all_casts c)
+    | DOP2(oper,c1,c2) -> DOP2(oper,strip_all_casts c1,strip_all_casts c2)
+    | DOPN(oper,cl) -> DOPN(oper,Array.map strip_all_casts cl)
+    | DOPL(oper,cl) -> DOPL(oper,List.map strip_all_casts cl)
+    | DLAM(na,c) -> DLAM(na,strip_all_casts c)
+    | DLAMV(na,c) -> DLAMV(na,Array.map (under_outer_cast strip_all_casts) c)
+    | VAR _ as t -> t
+    | Rel _ as t -> t
+
 (* Destructs the product (x:t1)t2 *)
 let destProd = function 
   | DOP2 (Prod, t1, (DLAM (x,t2))) -> (x,t1,t2) 
diff --git a/kernel/term.mli b/kernel/term.mli
index 869e65ca40..ff296c2dd3 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -260,6 +260,9 @@ val isCast : constr -> bool
    [strip_outer_cast] (Cast (Cast ... (Cast c, t) ... ))] is [c]. *)
 val strip_outer_cast : constr -> constr
 
+(* Special function, which keep the key casts under Fix and MutCase. *)
+val strip_all_casts : constr -> constr
+
 (* Destructs the product $(x:t_1)t_2$ *)
 val destProd : constr -> name * constr * constr
 val hd_of_prod : constr -> constr
diff --git a/library/declare.ml b/library/declare.ml
index 8da7753625..3063d801c9 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -288,7 +288,8 @@ let mind_path = function
 
 let declare_eliminations sp i =
   let oper = MutInd (sp,i) in
-  let ids = ids_of_sign (Global.var_context()) in
+  let mib = Global.lookup_mind sp in
+  let ids = ids_of_sign mib.mind_hyps in
   let mind = DOPN(oper, Array.of_list (List.map (fun id -> VAR id) ids)) in
   let mispec = Global.lookup_mind_specif mind in 
   let mindstr = string_of_id (mis_typename mispec) in
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index e43c9ed0ad..96b226be4b 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -327,8 +327,6 @@ GEXTEND Gram
           <:ast< (RestoreState $id) >>
       | IDENT "Remove";  IDENT "State"; id = identarg; "." ->
           <:ast< (RemoveState $id) >>
-      | IDENT "Reset"; IDENT "after"; id = identarg; "." ->
-          <:ast< (ResetAfter $id) >>
       | IDENT "Reset"; IDENT "Initial"; "." -> <:ast< (ResetInitial) >>
       | IDENT "Reset"; IDENT "Section"; id = identarg; "." ->
           <:ast< (ResetSection $id) >>
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 5d968321a7..474b247a68 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -58,13 +58,17 @@ let getenv_else s dft = try Sys.getenv s with Not_found -> dft
 let init_load_path () =
   (* default load path; only if COQLIB is defined *)
   let coqlib = getenv_else "COQLIB" Coq_config.coqlib in
-  if coqlib <> "" then
-    List.iter
-      (fun s -> add_include (Filename.concat coqlib s))
-      ("states" :: 
+  let coqtop = getenv_else "COQTOP" Coq_config.coqtop in
+  if coqlib = coqtop then
+    (* local installation *)
+    List.iter 
+      (fun s -> add_include (Filename.concat coqtop s))
+      ("states" :: "dev" ::
        (List.map 
 	  (fun s -> Filename.concat "theories" (hm2 s))
-          Coq_config.theories_dirs));
+          Coq_config.theories_dirs))
+  else
+    add_include coqlib;
   let camlp4 = getenv_else "CAMLP4LIB" Coq_config.camlp4lib in
   add_include camlp4;
   add_include ".";
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 17127518c0..e1396fb3a9 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -236,12 +236,6 @@ let _ =
 
 (***
 let _ =
-  add "ResetAfter"
-    (function 
-       | [VARG_IDENTIFIER id] -> (fun () -> reset_keeping_name id)
-       | _ -> bad_vernac_args "ResetAfter")
-
-let _ =
   add "ResetInitial"
     (function 
        | [] -> (fun () -> reset_initial ())