Intégration des modifs de la branche mowgli :

- Simplification de strength qui est maintenant un simple drapeau Local/Global.
- Export des catégories de déclarations (Lemma/Theorem/Definition/.../
  Axiom/Parameter/..) vers les .vo (nouveau fichier library/decl_kinds.ml).
- Export des variables de section initialement associées à une déclaration
  (nouveau fichier library/dischargedhypsmap.ml).


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

6 files changed, 33 insertions, 14 deletions

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index bc3b1310a..2b452ecbb 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -21,7 +21,7 @@ open Declare
 open Term
 open Termops
 open Rawterm
-open Nametab
+open Decl_kinds
 
 (* usage qque peu general: utilise aussi dans record *)
 
@@ -100,8 +100,8 @@ let add_new_path x =
 
 let init () =
   class_tab:= []; 
-  add_new_class (CL_FUN,  { cl_param = 0; cl_strength = NeverDischarge });
-  add_new_class (CL_SORT, { cl_param = 0; cl_strength = NeverDischarge });
+  add_new_class (CL_FUN,  { cl_param = 0; cl_strength = Global });
+  add_new_class (CL_SORT, { cl_param = 0; cl_strength = Global });
   coercion_tab:= [];
   inheritance_graph:= []
 
@@ -257,7 +257,7 @@ let class_args_of c = snd (decompose_app c)
 let strength_of_cl = function 
   | CL_CONST kn -> constant_strength (sp_of_global None (ConstRef kn))
   | CL_SECVAR sp -> variable_strength sp
-  | _ -> NeverDischarge
+  | _ -> Global
 
 let string_of_class = function
   | CL_FUN -> "FUNCLASS"
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index d37588d06..50af9840c 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -10,8 +10,7 @@
 
 (*i*)
 open Names
-open Libnames
-open Nametab
+open Decl_kinds
 open Term
 open Evd
 open Environ
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 4fce79be2..9ba82bf1f 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -57,6 +57,10 @@ val ise_try :  evar_defs -> (unit -> bool) list -> bool
 val ise_undefined :  evar_defs -> constr -> bool
 val has_undefined_isevars :  evar_defs -> constr -> bool
 
+val new_isevar_sign :
+ Environ.env -> Evd.evar_map -> Term.constr -> Term.constr list ->
+  Evd.evar_map * Term.constr
+
 val new_isevar :  evar_defs -> env -> loc * hole_kind -> constr -> constr
 
 val is_eliminator : constr -> bool
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index bcb0b5499..44398099c 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -507,7 +507,7 @@ let declare_one_elimination ind =
         { const_entry_body = c;
           const_entry_type = t;
           const_entry_opaque = false }, 
-       NeverDischarge) in
+       Decl_kinds.IsDefinition) in
     Options.if_verbose ppnl (str na ++ str " is defined"); 
     kn
   in
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index eb798ee44..a2e484f53 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -540,6 +540,22 @@ let whd_meta metamap c = match kind_of_term c with
 let plain_instance s c = 
   let rec irec u = match kind_of_term u with
     | Meta p -> (try List.assoc p s with Not_found -> u)
+    | App (f,l) when isCast f ->
+        let (f,t) = destCast f in
+        let l' = Array.map irec l in 
+        (match kind_of_term f with
+          | Meta p ->
+              (* Don't flatten application nodes: this is used to extract a
+                 proof-term from a proof-tree and we want to keep the structure
+                 of the proof-tree *)
+              (try let g = List.assoc p s in
+              match kind_of_term g with
+                | App _ -> 
+                    let h = id_of_string "H" in
+                    mkLetIn (Name h,g,t,mkApp(mkRel 1,Array.map (lift 1) l'))
+                | _ -> mkApp (g,l')
+              with Not_found -> mkApp (f,l'))
+          | _ -> mkApp (irec f,l'))
     | Cast (m,_) when isMeta m ->
 	(try List.assoc (destMeta m) s with Not_found -> u)
     | _ -> map_constr irec u
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 3c746b49d..aa5d27d20 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -67,13 +67,13 @@ let typeur sigma metamap =
     | Ind ind -> body_of_type (type_of_inductive env ind)
     | Construct cstr -> body_of_type (type_of_constructor env cstr)
     | Case (_,p,c,lf) ->
-        (* TODO: could avoid computing the type of branches *)
-        let i =
-          try find_rectype env (type_of env c)
+        let Inductiveops.IndType(_,realargs) =
+          try Inductiveops.find_rectype env sigma (type_of env c)
           with Not_found -> anomaly "type_of: Bad recursive type" in
-        let pj = { uj_val = p; uj_type = type_of env p } in
-        let (_,ty,_) = type_case_branches env i pj c in
-        ty
+        let t = whd_beta (applist (p, realargs)) in
+        (match kind_of_term (whd_betadeltaiota env sigma (type_of env t)) with
+          | Prod _ -> whd_beta (applist (t, [c]))
+          | _ -> t)
     | Lambda (name,c1,c2) ->
           mkProd (name, c1, type_of (push_rel (name,None,c1) env) c2)
     | LetIn (name,b,c1,c2) ->
@@ -101,7 +101,7 @@ let typeur sigma metamap =
     | _ -> outsort env sigma (type_of env t)
 
   and sort_family_of env t =
-    match kind_of_term (whd_betadeltaiota env sigma t) with
+    match kind_of_term t with
     | Cast (c,s) when isSort s -> family_of_sort (destSort s)
     | Sort (Prop c) -> InType
     | Sort (Type u) -> InType