Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et commandes vernaculaires (cf dev/changements.txt pour plus de précisions)

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

6 files changed, 28 insertions, 15 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index f424f79db..74e33cdfb 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -151,9 +151,4 @@ let import = import
 
 let env_of_safe_env e = e
 
-(* Exported typing functions *)
-
-let typing env c = 
-  let (j,cst) = safe_infer env c in
-  let _ = add_constraints cst env in
-  j
+let typing = Typeops.typing
diff --git a/kernel/term.ml b/kernel/term.ml
index 62f21de5f..95968f6c8 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -353,6 +353,9 @@ let isRel c = match kind_of_term c with Rel _ -> true | _ -> false
 (* Tests if a variable *)
 let isVar c = match kind_of_term c with Var _ -> true | _ -> false
 
+(* Tests if an inductive *)
+let isInd c = match kind_of_term c with Ind _ -> true | _ -> false
+
 (* Destructs the product (x:t1)t2 *)
 let destProd c = match kind_of_term c with 
   | Prod (x,t1,t2) -> (x,t1,t2) 
diff --git a/kernel/term.mli b/kernel/term.mli
index 73f29ddbe..643d06443 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -222,6 +222,7 @@ val kind_of_type : types -> (constr, types) kind_of_type
 
 val isRel  : constr -> bool
 val isVar  : constr -> bool
+val isInd  : constr -> bool
 val isEvar : constr -> bool
 val isMeta : constr -> bool
 val isSort : constr -> bool
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 4606734fe..6da58adbc 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -477,3 +477,10 @@ let infer_local_decls env decls =
       push_rel d env, add_rel_decl d l, Constraint.union cst1 cst2
   | [] -> env, empty_rel_context, Constraint.empty in
   inferec env decls
+
+(* Exported typing functions *)
+
+let typing env c = 
+  let (j,cst) = infer env c in
+  let _ = add_constraints cst env in
+  j
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 6980c9759..94d4e0844 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -89,3 +89,7 @@ val judge_of_case : env -> case_info
 (* Typecheck general fixpoint (not checking guard conditions) *)
 val type_fixpoint : env -> name array -> types array 
     -> unsafe_judgment array -> constraints
+
+(* Kernel safe typing but applicable to partial proofs *)
+val typing : env -> constr -> unsafe_judgment
+
diff --git a/kernel/univ.ml b/kernel/univ.ml
index c5b998380..9242e9d8a 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -112,8 +112,8 @@ let declare_univ u g =
   else
     g
 
-(* The universes of Prop and Set: Type_0, Type_1 and the
-   resulting graph. *)
+(* When typing Prop and Set, there is no constraint on the level,
+   hence the definition of prop_univ *)
 
 let initial_universes = UniverseMap.empty
 let prop_univ = Max ([],[])
@@ -406,17 +406,20 @@ let num_edges g =
   UniverseMap.fold (fun _ a n -> n + (reln_len a)) g 0
     
 let pr_arc = function 
-  | Canonical {univ=u; gt=gt; ge=ge} -> 
-      hov 2
-        (pr_uni_level u ++ spc () ++
-         prlist_with_sep pr_spc (fun v -> str ">" ++ pr_uni_level v) gt ++
-         prlist_with_sep pr_spc (fun v -> str ">=" ++ pr_uni_level v) ge)
+  | Canonical {univ=u; gt=[]; ge=[]} ->
+      mt ()
+  | Canonical {univ=u; gt=gt; ge=ge} ->
+      pr_uni_level u ++ str " " ++
+      v 0
+        (prlist_with_sep pr_spc (fun v -> str "> " ++ pr_uni_level v) gt ++
+         prlist_with_sep pr_spc (fun v -> str ">= " ++ pr_uni_level v) ge) ++
+      fnl ()
   | Equiv (u,v) -> 
-      pr_uni_level u  ++ str "=" ++ pr_uni_level v
+      pr_uni_level u  ++ str " = " ++ pr_uni_level v ++ fnl ()
 
 let pr_universes g =
   let graph = UniverseMap.fold (fun k a l -> (k,a)::l) g [] in
-  prlist_with_sep pr_fnl (function (_,a) -> pr_arc a) graph
+  prlist (function (_,a) -> pr_arc a) graph
     
 
 (* Dumping constrains to a file *)