retablissement make doc et make minicoq

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

3 files changed, 39 insertions, 34 deletions

diff --git a/toplevel/fhimsg.ml b/toplevel/fhimsg.ml
index dcc0a86976..9d0e9558a6 100644
--- a/toplevel/fhimsg.ml
+++ b/toplevel/fhimsg.ml
@@ -13,13 +13,13 @@ open Reduction
 open G_minicoq
 
 module type Printer = sig
-  val pr_term : path_kind -> context -> constr -> std_ppcmds
+  val pr_term : path_kind -> env -> constr -> std_ppcmds
 end
 
 module Make = functor (P : Printer) -> struct
 
-  let print_decl k sign (s,typ) =
-    let ptyp = P.pr_term k (gLOB sign) (body_of_type typ) in 
+  let print_decl k env (s,typ) =
+    let ptyp = P.pr_term k env (body_of_type typ) in 
     [< 'sPC; print_id s; 'sTR" : "; ptyp >]
   
   let print_binding k env = function
@@ -28,34 +28,38 @@ module Make = functor (P : Printer) -> struct
     | Name id,ty -> 
 	[< 'sPC; print_id id ; 'sTR" : "; P.pr_term k env (body_of_type ty) >]
 
+(****
   let sign_it_with f sign e =
-    snd (sign_it 
-	   (fun id t (sign,e) -> (add_sign (id,t) sign, f id t sign e))
-           sign (nil_sign,e))
+    snd (fold_var_context
+	   (fun (id,v,t) (sign,e) -> (add_var (id,v,t) sign, f id t sign e))
+           sign (empty_var_context,e))
 
   let dbenv_it_with f env e =
     snd (dbenv_it 
 	   (fun na t (env,e) -> (add_rel (na,t) env, f na t env e))
            env (gLOB(get_globals env),e))
+****)
       
   let pr_env k env =
     let sign_env =
-      sign_it_with
-	(fun id t sign pps ->
-           let pidt =  print_decl k sign (id,t) in [<  pps ; 'fNL ; pidt >])
-	(get_globals env) [< >] 
+      fold_var_context
+	(fun env (id,_,t) pps ->
+           let pidt =  print_decl k env (id,t) in [<  pps ; 'fNL ; pidt >])
+	env [< >] 
     in
     let db_env =
-      dbenv_it_with 
-	(fun na t env pps ->
+      fold_rel_context
+	(fun env (na,_,t) pps ->
            let pnat = print_binding k env (na,t) in [<  pps ; 'fNL ; pnat >])
 	env [< >]
     in 
     [< sign_env; db_env >]
     
-  let pr_ne_ctx header k = function
-    | ENVIRON (s1,s2) when s1=nil_sign & s2=nil_dbsign -> [< >]
-    | env -> [< header; pr_env k env >]
+  let pr_ne_ctx header k env =
+    if rel_context env = [] && var_context env = [] then
+      [< >]
+    else
+      [< header; pr_env k env >]
 
 
 let explain_unbound_rel k ctx n =
@@ -129,7 +133,7 @@ let explain_ill_formed_branch k ctx c i actty expty =
 let explain_generalization k ctx (name,var) c =
   let pe = pr_ne_ctx [< 'sTR"in environment" >] k ctx in
   let pv = P.pr_term k ctx (body_of_type var) in
-  let pc = P.pr_term k (add_rel (name,var) ctx) c in
+  let pc = P.pr_term k (push_rel (name,None,var) ctx) c in
   [< 'sTR"Illegal generalization: "; pe; 'fNL;
      'sTR"Cannot generalize"; 'bRK(1,1); pv; 'sPC;
      'sTR"over"; 'bRK(1,1); pc; 'sPC;
diff --git a/toplevel/fhimsg.mli b/toplevel/fhimsg.mli
index eb8d615538..ad0e7e6646 100644
--- a/toplevel/fhimsg.mli
+++ b/toplevel/fhimsg.mli
@@ -15,53 +15,53 @@ open Type_errors
    context. *)
 
 module type Printer = sig
-  val pr_term : path_kind -> context -> constr -> std_ppcmds
+  val pr_term : path_kind -> env -> constr -> std_ppcmds
 end
 
 (*s The result is a module which provides a function [explain_type_error]
-  to explain a type error for a given kind in a given context, which are 
+  to explain a type error for a given kind in a given env, which are 
   usually the three arguments carried by the exception [TypeError] 
   (see \refsec{typeerrors}). *)
 
 module Make (P : Printer) : sig
 
-val explain_type_error : path_kind -> context -> type_error -> std_ppcmds
+val explain_type_error : path_kind -> env -> type_error -> std_ppcmds
 
-val pr_ne_ctx : std_ppcmds -> path_kind -> context -> std_ppcmds
+val pr_ne_ctx : std_ppcmds -> path_kind -> env -> std_ppcmds
 
-val explain_unbound_rel : path_kind -> context -> int -> std_ppcmds
+val explain_unbound_rel : path_kind -> env -> int -> std_ppcmds
 
-val explain_not_type : path_kind -> context -> constr -> std_ppcmds
+val explain_not_type : path_kind -> env -> constr -> std_ppcmds
 
-val explain_bad_assumption : path_kind -> context -> constr -> std_ppcmds
+val explain_bad_assumption : path_kind -> env -> constr -> std_ppcmds
  
 val explain_reference_variables : identifier -> std_ppcmds
 
 val explain_elim_arity : 
-  path_kind -> context -> constr -> constr list -> constr 
+  path_kind -> env -> constr -> constr list -> constr 
     -> constr -> constr -> (constr * constr * string) option -> std_ppcmds
 
 val explain_case_not_inductive : 
-  path_kind -> context -> constr -> constr -> std_ppcmds
+  path_kind -> env -> constr -> constr -> std_ppcmds
 
 val explain_number_branches : 
-  path_kind -> context -> constr -> constr -> int -> std_ppcmds
+  path_kind -> env -> constr -> constr -> int -> std_ppcmds
 
 val explain_ill_formed_branch :
-  path_kind -> context -> constr -> int -> constr -> constr -> std_ppcmds
+  path_kind -> env -> constr -> int -> constr -> constr -> std_ppcmds
 
 val explain_generalization :
-  path_kind -> context -> name * typed_type -> constr -> std_ppcmds
+  path_kind -> env -> name * typed_type -> constr -> std_ppcmds
 
 val explain_actual_type :
-  path_kind -> context -> constr -> constr -> constr -> std_ppcmds
+  path_kind -> env -> constr -> constr -> constr -> std_ppcmds
 
 val explain_ill_formed_rec_body :
-  path_kind -> context -> std_ppcmds -> 
+  path_kind -> env -> std_ppcmds -> 
     name list -> int -> constr array -> std_ppcmds
 
 val explain_ill_typed_rec_body  :
-  path_kind -> context -> int -> name list -> unsafe_judgment array 
+  path_kind -> env -> int -> name list -> unsafe_judgment array 
     -> typed_type array -> std_ppcmds
 
 end
diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml
index 59253eb072..5df900c264 100644
--- a/toplevel/minicoq.ml
+++ b/toplevel/minicoq.ml
@@ -23,7 +23,8 @@ let lookup_var id =
   in
   look 1
 
-let args sign = Array.of_list (List.map (fun id -> VAR id) (ids_of_sign sign))
+let args sign = 
+  Array.of_list (List.map (fun id -> VAR id) (ids_of_var_context sign))
 
 let rec globalize bv = function
   | VAR id -> lookup_var id bv
@@ -45,7 +46,7 @@ let check c =
   let c = globalize [] c in
   let (j,u) = safe_machine !env c in
   let ty = j_type j in
-  let pty = pr_term CCI (context !env) ty in
+  let pty = pr_term CCI (env_of_safe_env !env) ty in
   mSGNL (hOV 0 [< 'sTR"  :"; 'sPC; hOV 0 pty; 'fNL >])
 
 let definition id ty c =
@@ -65,7 +66,7 @@ let parameter id t =
 
 let variable id t =
   let t = globalize [] t in
-  env := push_var (id,t) !env;
+  env := push_var_decl (id,t) !env;
   mSGNL (hOV 0 [< 'sTR"variable"; 'sPC; print_id id; 
 		  'sPC; 'sTR"is declared"; 'fNL >])