mise en place commandes minicoq

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

6 files changed, 36 insertions, 34 deletions

diff --git a/kernel/constant.ml b/kernel/constant.ml
index 9699d68a75..ba932b7885 100644
--- a/kernel/constant.ml
+++ b/kernel/constant.ml
@@ -18,7 +18,7 @@ type recipe =
 
 type constant_entry = {
   const_entry_body : constr;
-  const_entry_type : constr }
+  const_entry_type : constr option }
 
 type constant_body = {
   const_kind : path_kind;
diff --git a/kernel/constant.mli b/kernel/constant.mli
index bc3d1a4e3d..d8aeb7670e 100644
--- a/kernel/constant.mli
+++ b/kernel/constant.mli
@@ -17,7 +17,7 @@ type recipe =
 
 type constant_entry = {
   const_entry_body : constr;
-  const_entry_type : constr }
+  const_entry_type : constr option }
 
 type constant_body = {
   const_kind : path_kind;
diff --git a/kernel/term.ml b/kernel/term.ml
index a166250234..3871f6ce17 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -150,8 +150,10 @@ let mkMutInd sp i l = (DOPN (MutInd (sp,i), l))
 let mkMutConstruct sp i j l =  (DOPN ((MutConstruct ((sp,i),j),l))) 
 
 (* Constructs the term <p>Case c of c1 | c2 .. | cn end *)
-let mkMutCase ci p c ac = DOPN (MutCase ci,Array.append [|p;c|] (Array.of_list ac))
-let mkMutCaseA ci p c ac = DOPN (MutCase ci,Array.append [|p;c|] ac)
+let mkMutCase ci p c ac = 
+  DOPN (MutCase ci, Array.append [|p;c|] (Array.of_list ac))
+let mkMutCaseA ci p c ac = 
+  DOPN (MutCase ci, Array.append [|p;c|] ac)
 
 (* If recindxs = [|i1,...in|] 
       typarray = [|t1,...tn|]
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 7e81618654..325d9fff37 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -32,6 +32,7 @@ let typed_type_of_judgment env j =
     | DOP0(Sort s) -> { body = j.uj_val; typ = s }
     | _ -> error_not_type CCI env j.uj_val
 
+(* same function, but with a different error message *)
 let assumption_of_judgement env j =
   match whd_betadeltaiota env j.uj_type with
     | DOP0(Sort s) -> { body = j.uj_val; typ = s }
diff --git a/kernel/typing.ml b/kernel/typing.ml
index e69c846658..13a809b034 100644
--- a/kernel/typing.ml
+++ b/kernel/typing.ml
@@ -18,22 +18,9 @@ open Indtypes
 
 type judgment = unsafe_judgment
 
-(* Fonctions temporaires pour relier la forme castée de la forme jugement *)
-
-let tjudge_of_cast env = function
-  | DOP2 (Cast, b, t) ->
-      (match whd_betadeltaiota env t with
-	 | DOP0 (Sort s) -> {body=b; typ=s}
-	 | DOP2 (Cast, b',t') -> anomaly "Supercast (tjudge_of_cast) [Mach]"
-	 | _ -> anomaly "Not a type (tjudge_of_cast) [Mach]")
-  | _ -> anomaly "Not casted (tjudge_of_cast)"
-	
-let tjudge_of_judge env j =
-  { body = j.uj_val;
-    typ = match whd_betadeltaiota env j.uj_type with
-      (* Nécessaire pour ZFC *)
-      | DOP0 (Sort s) -> s
-      | _ -> anomaly "Not a type (tjudge_ofjudge)" }
+let j_val j = j.uj_val
+let j_type j = j.uj_type
+let j_kind j = j.uj_kind
 
 let vect_lift = Array.mapi lift
 let vect_lift_type = Array.mapi (fun i t -> typed_app (lift i) t)
@@ -293,20 +280,28 @@ let push_rels vars env =
 let add_constant sp ce env =
   let (jb,u) = safe_machine env ce.const_entry_body in
   let env' = set_universes u env in
-  let (jt,u') = safe_machine env ce.const_entry_type in
-  let env'' = set_universes u' env' in
-  match conv env'' jb.uj_type jt.uj_val with
-    | Convertible u'' -> 
-	let cb = { 
-	  const_kind = kind_of_path sp;
-	  const_body = Some (ref (Cooked ce.const_entry_body));
-	  const_type = typed_type_of_judgment env'' jt;
-	  const_hyps = get_globals (context env);
-	  const_opaque = false } 
-	in
-	add_constant sp cb (set_universes u'' env'')
-    | NotConvertible -> 
-	error_actual_type CCI env jb.uj_val jb.uj_type jt.uj_val
+  let (env'',ty) = 
+    match ce.const_entry_type with
+      | None -> 
+	  env', typed_type_of_judgment env' jb
+      | Some ty -> 
+	  let (jt,u') = safe_machine env ty in
+	  let env'' = set_universes u' env' in
+	  match conv env'' jb.uj_type jt.uj_val with
+	    | Convertible u'' -> 
+		let env'' = set_universes u'' env' in
+		env'', typed_type_of_judgment env'' jt
+	    | NotConvertible -> 
+		error_actual_type CCI env jb.uj_val jb.uj_type jt.uj_val
+  in
+  let cb = { 
+    const_kind = kind_of_path sp;
+    const_body = Some (ref (Cooked ce.const_entry_body));
+    const_type = ty;
+    const_hyps = get_globals (context env);
+    const_opaque = false } 
+  in
+  add_constant sp cb env''
 
 let type_from_judgment env j =
   match whd_betadeltaiota env j.uj_kind with
diff --git a/kernel/typing.mli b/kernel/typing.mli
index ec3ca5d7d9..d9d410c542 100644
--- a/kernel/typing.mli
+++ b/kernel/typing.mli
@@ -45,6 +45,10 @@ val lookup_meta : int -> 'a environment -> constr
 
 type judgment
 
+val j_val : judgment -> constr
+val j_type : judgment -> constr
+val j_kind : judgment -> constr
+
 val safe_machine : 'a environment -> constr -> judgment * universes
 val safe_machine_type : 'a environment -> constr -> typed_type