Few OCaml files in contrib/xml

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

7 files changed, 98 insertions, 191 deletions

diff --git a/.depend b/.depend
index 801ef3887f..5eb181f74d 100644
--- a/.depend
+++ b/.depend
@@ -185,7 +185,6 @@ toplevel/vernacentries.cmi: kernel/names.cmi kernel/term.cmi \
     toplevel/vernacinterp.cmi 
 toplevel/vernacinterp.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \
     proofs/proof_type.cmi 
-contrib/xml/cooking.cmi: kernel/names.cmi 
 contrib/xml/xmlcommand.cmi: kernel/names.cmi 
 config/coq_config.cmo: config/coq_config.cmi 
 config/coq_config.cmx: config/coq_config.cmi 
@@ -955,10 +954,8 @@ tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx kernel/evd.cmx \
     library/global.cmx proofs/logic.cmx kernel/names.cmx lib/pp.cmx \
     proofs/proof_trees.cmx kernel/reduction.cmx kernel/sign.cmx \
     proofs/tacmach.cmx kernel/term.cmx lib/util.cmx tactics/wcclausenv.cmi 
-tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo 
-tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx 
-tools/coqdep_lexer.cmo: config/coq_config.cmi 
-tools/coqdep_lexer.cmx: config/coq_config.cmx 
+tools/coqdep.cmo: config/coq_config.cmi 
+tools/coqdep.cmx: config/coq_config.cmx 
 toplevel/command.cmo: parsing/ast.cmi parsing/astterm.cmi parsing/coqast.cmi \
     kernel/declarations.cmi library/declare.cmi kernel/environ.cmi \
     kernel/evd.cmi library/global.cmi library/indrec.cmi kernel/inductive.cmi \
@@ -979,7 +976,7 @@ toplevel/coqinit.cmo: config/coq_config.cmi library/library.cmi \
     toplevel/mltop.cmi lib/options.cmi lib/pp.cmi lib/system.cmi \
     toplevel/toplevel.cmi toplevel/vernac.cmi toplevel/coqinit.cmi 
 toplevel/coqinit.cmx: config/coq_config.cmx library/library.cmx \
-    toplevel/mltop.cmx lib/options.cmx lib/pp.cmx lib/system.cmx \
+    toplevel/mltop.cmi lib/options.cmx lib/pp.cmx lib/system.cmx \
     toplevel/toplevel.cmx toplevel/vernac.cmx toplevel/coqinit.cmi 
 toplevel/coqtop.cmo: config/coq_config.cmi toplevel/coqinit.cmi \
     toplevel/errors.cmi library/lib.cmi library/library.cmi \
@@ -988,7 +985,7 @@ toplevel/coqtop.cmo: config/coq_config.cmi toplevel/coqinit.cmi \
     toplevel/usage.cmi lib/util.cmi toplevel/vernac.cmi toplevel/coqtop.cmi 
 toplevel/coqtop.cmx: config/coq_config.cmx toplevel/coqinit.cmx \
     toplevel/errors.cmx library/lib.cmx library/library.cmx \
-    toplevel/mltop.cmx lib/options.cmx lib/pp.cmx lib/profile.cmx \
+    toplevel/mltop.cmi lib/options.cmx lib/pp.cmx lib/profile.cmx \
     library/states.cmx lib/system.cmx toplevel/toplevel.cmx \
     toplevel/usage.cmx lib/util.cmx toplevel/vernac.cmx toplevel/coqtop.cmi 
 toplevel/discharge.cmo: pretyping/class.cmi pretyping/classops.cmi \
@@ -1049,12 +1046,6 @@ toplevel/minicoq.cmx: kernel/declarations.cmx toplevel/fhimsg.cmx \
     parsing/g_minicoq.cmi kernel/inductive.cmx kernel/names.cmx lib/pp.cmx \
     kernel/safe_typing.cmx kernel/sign.cmx kernel/term.cmx \
     kernel/type_errors.cmx lib/util.cmx 
-toplevel/mltop.cmo: library/lib.cmi library/libobject.cmi library/library.cmi \
-    lib/pp.cmi library/summary.cmi lib/system.cmi lib/util.cmi \
-    toplevel/vernacinterp.cmi toplevel/mltop.cmi 
-toplevel/mltop.cmx: library/lib.cmx library/libobject.cmx library/library.cmx \
-    lib/pp.cmx library/summary.cmx lib/system.cmx lib/util.cmx \
-    toplevel/vernacinterp.cmx toplevel/mltop.cmi 
 toplevel/protectedtoplevel.cmo: toplevel/errors.cmi parsing/pcoq.cmi \
     lib/pp.cmi toplevel/vernac.cmi toplevel/vernacinterp.cmi \
     toplevel/protectedtoplevel.cmi 
@@ -1077,7 +1068,7 @@ toplevel/toplevel.cmo: parsing/ast.cmi toplevel/errors.cmi toplevel/mltop.cmi \
     kernel/names.cmi lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi \
     lib/pp.cmi toplevel/protectedtoplevel.cmi lib/util.cmi \
     toplevel/vernac.cmi toplevel/vernacinterp.cmi toplevel/toplevel.cmi 
-toplevel/toplevel.cmx: parsing/ast.cmx toplevel/errors.cmx toplevel/mltop.cmx \
+toplevel/toplevel.cmx: parsing/ast.cmx toplevel/errors.cmx toplevel/mltop.cmi \
     kernel/names.cmx lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx \
     lib/pp.cmx toplevel/protectedtoplevel.cmx lib/util.cmx \
     toplevel/vernac.cmx toplevel/vernacinterp.cmx toplevel/toplevel.cmi 
@@ -1171,25 +1162,19 @@ contrib/ring/ring.cmx: parsing/astterm.cmx kernel/closure.cmx \
     library/summary.cmx proofs/tacmach.cmx pretyping/tacred.cmx \
     tactics/tactics.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \
     toplevel/vernacinterp.cmx 
-contrib/xml/cooking.cmo: kernel/declarations.cmi library/global.cmi \
-    kernel/names.cmi kernel/term.cmi lib/util.cmi contrib/xml/xml.cmi \
-    contrib/xml/cooking.cmi 
-contrib/xml/cooking.cmx: kernel/declarations.cmx library/global.cmx \
-    kernel/names.cmx kernel/term.cmx lib/util.cmx contrib/xml/xml.cmx \
-    contrib/xml/cooking.cmi 
 contrib/xml/xml.cmo: contrib/xml/xml.cmi 
 contrib/xml/xml.cmx: contrib/xml/xml.cmi 
-contrib/xml/xmlcommand.cmo: contrib/xml/cooking.cmi kernel/declarations.cmi \
-    library/declare.cmi kernel/evd.cmi library/global.cmi library/lib.cmi \
-    library/libobject.cmi library/library.cmi kernel/names.cmi \
-    library/nametab.cmi proofs/pfedit.cmi proofs/proof_trees.cmi \
-    proofs/tacmach.cmi kernel/term.cmi lib/util.cmi contrib/xml/xml.cmi \
+contrib/xml/xmlcommand.cmo: kernel/declarations.cmi library/declare.cmi \
+    kernel/evd.cmi library/global.cmi library/lib.cmi library/libobject.cmi \
+    library/library.cmi kernel/names.cmi library/nametab.cmi \
+    proofs/pfedit.cmi proofs/proof_trees.cmi proofs/tacmach.cmi \
+    kernel/term.cmi lib/util.cmi contrib/xml/xml.cmi \
     contrib/xml/xmlcommand.cmi 
-contrib/xml/xmlcommand.cmx: contrib/xml/cooking.cmx kernel/declarations.cmx \
-    library/declare.cmx kernel/evd.cmx library/global.cmx library/lib.cmx \
-    library/libobject.cmx library/library.cmx kernel/names.cmx \
-    library/nametab.cmx proofs/pfedit.cmx proofs/proof_trees.cmx \
-    proofs/tacmach.cmx kernel/term.cmx lib/util.cmx contrib/xml/xml.cmx \
+contrib/xml/xmlcommand.cmx: kernel/declarations.cmx library/declare.cmx \
+    kernel/evd.cmx library/global.cmx library/lib.cmx library/libobject.cmx \
+    library/library.cmx kernel/names.cmx library/nametab.cmx \
+    proofs/pfedit.cmx proofs/proof_trees.cmx proofs/tacmach.cmx \
+    kernel/term.cmx lib/util.cmx contrib/xml/xml.cmx \
     contrib/xml/xmlcommand.cmi 
 contrib/xml/xmlentries.cmo: lib/util.cmi toplevel/vernacinterp.cmi \
     contrib/xml/xmlcommand.cmi 
diff --git a/.depend.coq b/.depend.coq
index bf1435e813..ca000362bb 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -1,7 +1,7 @@
 theories/Zarith/zarith_aux.vo: theories/Zarith/zarith_aux.v theories/Arith/Arith.vo theories/Zarith/fast_integer.vo
 theories/Zarith/fast_integer.vo: theories/Zarith/fast_integer.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Mult.vo theories/Arith/Minus.vo
 theories/Zarith/auxiliary.vo: theories/Zarith/auxiliary.v theories/Arith/Arith.vo theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo
-theories/Zarith/Zsyntax.vo: theories/Zarith/Zsyntax.v theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo parsing/g_zsyntax.cmo
+theories/Zarith/Zsyntax.vo: theories/Zarith/Zsyntax.v theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo
 theories/Zarith/Zmisc.vo: theories/Zarith/Zmisc.v theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Zarith/auxiliary.vo theories/Zarith/Zsyntax.vo theories/Bool/Bool.vo
 theories/Zarith/ZArith_dec.vo: theories/Zarith/ZArith_dec.v theories/Bool/Sumbool.vo theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Zarith/auxiliary.vo theories/Zarith/Zsyntax.vo
 theories/Zarith/ZArith.vo: theories/Zarith/ZArith.v theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Zarith/auxiliary.vo theories/Zarith/Zsyntax.vo theories/Zarith/ZArith_dec.vo theories/Zarith/Zmisc.vo theories/Zarith/Wf_Z.vo
@@ -90,11 +90,11 @@ theories/Arith/Div.vo: theories/Arith/Div.v theories/Arith/Le.vo theories/Arith/
 theories/Arith/Compare_dec.vo: theories/Arith/Compare_dec.v theories/Arith/Le.vo theories/Arith/Lt.vo
 theories/Arith/Compare.vo: theories/Arith/Compare.v theories/Arith/Arith.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo theories/Arith/Wf_nat.vo theories/Arith/Min.vo
 theories/Arith/Between.vo: theories/Arith/Between.v theories/Arith/Le.vo theories/Arith/Lt.vo
-theories/Arith/Arith.vo: theories/Arith/Arith.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Gt.vo theories/Arith/Minus.vo theories/Arith/Mult.vo theories/Arith/Between.vo parsing/g_natsyntax.cmo
+theories/Arith/Arith.vo: theories/Arith/Arith.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Gt.vo theories/Arith/Minus.vo theories/Arith/Mult.vo theories/Arith/Between.vo
 test-suite/tactics/TestRefine.vo: test-suite/tactics/TestRefine.v tactics/Refine.vo theories/Init/Wf.vo theories/Arith/Wf_nat.vo theories/Arith/Compare_dec.vo theories/Arith/Lt.vo
 test-suite/bench/lists_100.vo: test-suite/bench/lists_100.v
 test-suite/bench/lists-100.vo: test-suite/bench/lists-100.v
-contrib/xml/Xml.vo: contrib/xml/Xml.v contrib/xml/xml.cmo contrib/xml/cooking.cmo contrib/xml/xmlcommand.cmo contrib/xml/xmlentries.cmo
+contrib/xml/Xml.vo: contrib/xml/Xml.v contrib/xml/xml.cmo contrib/xml/xmlcommand.cmo contrib/xml/xmlentries.cmo
 contrib/ring/ZArithRing.vo: contrib/ring/ZArithRing.v contrib/ring/ArithRing.vo theories/Zarith/ZArith.vo theories/Logic/Eqdep_dec.vo
 contrib/ring/Ring_theory.vo: contrib/ring/Ring_theory.v theories/Bool/Bool.vo
 contrib/ring/Ring_normalize.vo: contrib/ring/Ring_normalize.v contrib/ring/Ring_theory.vo contrib/ring/Quote.vo
diff --git a/Makefile b/Makefile
index 1254d5415c..38d6aa49e8 100644
--- a/Makefile
+++ b/Makefile
@@ -125,7 +125,7 @@ USERTACCMX=$(USERTAC:.ml4=.cmx)
 
 CONTRIB=contrib/omega/omega.cmo contrib/omega/coq_omega.cmo \
         contrib/ring/quote.cmo contrib/ring/ring.cmo \
-        contrib/xml/xml.cmo contrib/xml/cooking.cmo \
+        contrib/xml/xml.cmo \
 	contrib/xml/xmlcommand.cmo contrib/xml/xmlentries.cmo
 
 CMA=$(CLIBS) $(CAMLP4OBJS)
diff --git a/contrib/xml/Xml.v b/contrib/xml/Xml.v
index d0737b3116..0c82ae6698 100644
--- a/contrib/xml/Xml.v
+++ b/contrib/xml/Xml.v
@@ -8,7 +8,7 @@
 (*                                 17/11/1999                                 *)
 (******************************************************************************)
 
-Declare ML Module "xml" "cooking" "xmlcommand" "xmlentries".
+Declare ML Module "xml" "xmlcommand" "xmlentries".
 
 Grammar vernac vernac : Ast :=
   xml_print [ "Print" "XML" identarg($id) "." ] ->
diff --git a/contrib/xml/cooking.ml b/contrib/xml/cooking.ml
deleted file mode 100644
index 10c8d80efa..0000000000
--- a/contrib/xml/cooking.ml
+++ /dev/null
@@ -1,87 +0,0 @@
-(******************************************************************************)
-(*                                                                            *)
-(*                               PROJECT HELM                                 *)
-(*                                                                            *)
-(*                     A tactic to print Coq objects in XML                   *)
-(*                                                                            *)
-(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
-(*                                 02/12/1999                                 *)
-(*                                                                            *)
-(* This module compute the list of variables occurring in a term from the     *)
-(* term and the list of variables possibly occuring in it                     *)
-(*                                                                            *)
-(******************************************************************************)
-
-let get_depth_of_var vl v =
- let rec aux n =
-  function
-     [] -> None
-   | (he::tl) -> if List.mem v he then Some n else aux (n + 1) tl
- in
-  aux 0 vl
-;;
-
-exception CookingInternalError;;
-
-let string_of_vars_list =
- let add_prefix n s = string_of_int n ^ ": " ^ s in
- let rec aux =
-  function
-     [n,v] -> (n,v)
-   | (n,v)::tl ->
-      let (k,s) = aux tl in
-       if k = n then (k, v ^ " " ^ s) else (n, v ^ " " ^ add_prefix k s)
-   | [] -> raise CookingInternalError
- in
-  function
-     [] -> ""
-   | vl -> let (k,s) = aux vl in add_prefix k s
-;;
-
-(*CSC commento sbagliato ed obsoleto *)
-(* If t is \v1. ... \vn.t' where v1, ..., vn are in the variable list vl then *)
-(* get_params_from_type vl t returns [v1; ...; vn]                            *)
-let get_params_from_type vl t =
- let rec rget t l =
-  let module T = Term in
-  let module N = Names in
-   match T.kind_of_term t with
-      T.IsProd (N.Name id, _, target) ->
-       let id' = N.string_of_id id in
-        (match get_depth_of_var vl id' with
-            None   -> l
-          | Some n -> rget target ((n,id')::l)
-        )
-    | T.IsCast (term, _) -> rget term l
-    | _ -> l
- in
-  let pl = List.rev (rget t []) in
-   string_of_vars_list pl
-;;
-
-(* add_cooking_information csp vl                               *)
-(*  when  csp is the section path of the most cooked object co  *)
-(*  and   vl  is the list of variables possibly occuring in co  *)
-(* returns the list of variables actually occurring in co       *)
-let add_cooking_information sp vl =
- let module D = Declarations in
- let module G = Global in
- let module N = Names in
- let module T = Term in
- let module X = Xml in
-  try
-   let {D.const_body=val0 ; D.const_type = typ} = G.lookup_constant sp in
-   let typ = T.body_of_type typ in
-    get_params_from_type vl typ
-  with
-   Not_found ->
-    try
-     let {D.mind_packets=packs ; D.mind_nparams=nparams} =
-      G.lookup_mind sp
-     in
-      let {D.mind_nf_arity=arity} = packs.(0) in
-      let arity = T.body_of_type arity in
-       get_params_from_type vl arity
-    with
-     Not_found -> Util.anomaly "Cooking of an uncoockable term required"
-;;
diff --git a/contrib/xml/cooking.mli b/contrib/xml/cooking.mli
deleted file mode 100644
index 6eb5b4330d..0000000000
--- a/contrib/xml/cooking.mli
+++ /dev/null
@@ -1,20 +0,0 @@
-(******************************************************************************)
-(*                                                                            *)
-(*                               PROJECT HELM                                 *)
-(*                                                                            *)
-(*                     A tactic to print Coq objects in XML                   *)
-(*                                                                            *)
-(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
-(*                                 17/11/1999                                 *)
-(*                                                                            *)
-(* This module compute the list of variables occurring in a term from the     *)
-(* term and the list of variables possibly occuring in it                     *)
-(*                                                                            *)
-(******************************************************************************)
-
-(* add_cooking_information csp vl                               *)
-(*  when  csp is the section path of the most cooked object co  *)
-(*  and   vl  is the list of variables possibly occuring in co  *)
-(* returns the list of variables actually occurring in co       *)
-val add_cooking_information :
-  Names.section_path -> string list list -> string
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index d0cb0bf88c..bb8ab61257 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -17,15 +17,6 @@
 let dtdname = "http://localhost:8081/getdtd?url=cic.dtd";;
 let verbose = ref false;; (* always set to true during a "Print XML All" *)
 
-
-
-exception ImpossiblePossible;;
-type formal_parameters =
-   Actual of string
- | Possible of string
-;;
-
-
 (* UTILITY FUNCTIONS *)
 
 let print_if_verbose s = if !verbose then print_string s;;
@@ -146,7 +137,23 @@ let string_of_name =
 (* list of variables availables in the actual section *)
 let pvars = ref [];;
 
-let pvars_to_string pvars =
+let string_of_vars_list =
+ let add_prefix n s = string_of_int n ^ ": " ^ s in
+ let rec aux =
+  function
+     [n,v] -> (n,v)
+   | (n,v)::tl ->
+      let (k,s) = aux tl in
+       if k = n then (k, v ^ " " ^ s) else (n, v ^ " " ^ add_prefix k s)
+   | [] -> assert false
+ in
+  function
+     [] -> ""
+   | vl -> let (k,s) = aux vl in add_prefix k s
+;;
+
+(*
+let string_of_pvars pvars hyps =
  let rec aux =
   function
      [] -> (0, "")
@@ -159,6 +166,20 @@ let pvars_to_string pvars =
  in
   snd (aux (List.rev pvars))
 ;;
+*)
+
+let string_of_pvars pvars hyps =
+ let find_depth pvars v =
+  let rec aux n =
+   function
+      [] -> assert false
+    | l::_ when List.mem v l -> (n,v)
+    | _::tl -> aux (n+1) tl
+  in
+   aux 0 pvars
+ in
+  string_of_vars_list (List.map (find_depth pvars) hyps)
+;;
 
 exception XmlCommandInternalError;;
 
@@ -370,38 +391,36 @@ let print_current_proof c typ id mv =
 (*  and   id          is the identifier (name) of a                        *)
 (*  and   params      is the list of formal params for a                   *)
 (* returns a stream of XML tokens suitable to be pretty printed via Xml.pp *)
-let print_axiom id typ fv =
+let print_axiom id typ fv hyps =
  let module X = Xml in
  let module N = Names in
   reset_id () ;
   [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
      X.xml_cdata ("<!DOCTYPE Axiom SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
      X.xml_nempty "Axiom"
-      (["name",(N.string_of_id id) ; "id", get_next_id ()] @
-       match fv with
-          Possible _ -> raise ImpossiblePossible
-        | Actual fv' -> ["params",fv']
-      ) [< X.xml_nempty "type" [] (print_term [] typ) >]
+      ["name",(N.string_of_id id) ;
+        "id", get_next_id () ;
+        "params",(string_of_pvars fv hyps)]
+      [< X.xml_nempty "type" [] (print_term [] typ) >]
   >]
 ;;
 
-(* print_definition id term type params                                    *)
+(* print_definition id term type params hyps                               *)
 (*  where id          is the identifier (name) of a definition d           *)
 (*  and   term        is the term (body) of d                              *)
 (*  and   type        is the type of d                                     *)
 (*  and   params      is the list of formal params for d                   *)
 (* returns a stream of XML tokens suitable to be pretty printed via Xml.pp *)
-let print_definition id c typ fv =
+let print_definition id c typ fv hyps =
  let module X = Xml in
  let module N = Names in
   reset_id () ;
   [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
      X.xml_cdata ("<!DOCTYPE Definition SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
      X.xml_nempty "Definition"
-      (["name",(N.string_of_id id) ; "id", get_next_id ()] @
-       match fv with
-          Possible fv' -> ["params",fv' ; "paramMode","POSSIBLE"]
-        | Actual fv' -> ["params",fv'])
+      ["name",(N.string_of_id id) ;
+       "id", get_next_id () ;
+       "params",(string_of_pvars fv hyps)]
       [< X.xml_nempty "body" [] (print_term [] c) ;
          X.xml_nempty "type"  [] (print_term [] typ) >]
   >]
@@ -464,7 +483,7 @@ let print_mutual_inductive_packet names p =
 (*  and   nparams     is the number of "parameters" in the arity of the    *)
 (*                    mutual inductive types                               *)
 (* returns a stream of XML tokens suitable to be pretty printed via Xml.pp *)
-let print_mutual_inductive packs fv nparams =
+let print_mutual_inductive packs fv hyps nparams =
  let module D = Declarations in
  let module X = Xml in
  let module N = Names in
@@ -478,10 +497,9 @@ let print_mutual_inductive packs fv nparams =
       X.xml_cdata ("<!DOCTYPE InductiveDefinition SYSTEM \"" ^
        dtdname ^ "\">\n\n") ;
       X.xml_nempty "InductiveDefinition"
-       (["noParams",string_of_int nparams ; "id",get_next_id ()] @
-        (match fv with
-            Possible fv' -> ["params",fv' ; "paramMode","POSSIBLE"]
-          | Actual fv' -> ["params",fv']))
+       ["noParams",string_of_int nparams ;
+        "id",get_next_id () ;
+        "params",(string_of_pvars fv hyps)]
        [< (Array.fold_right
             (fun x i -> [< print_mutual_inductive_packet names x ; i >])
             packs
@@ -491,6 +509,14 @@ let print_mutual_inductive packs fv nparams =
    >]
 ;;
 
+let string_list_of_named_context_list =
+ List.map
+  (function
+      (n,None,_) -> Names.string_of_id n
+    | _          -> assert false
+  )
+;;
+
 (* print id dest                                                          *)
 (*  where id   is the identifier (name) of a definition/theorem or of an  *)
 (*             inductive definition                                       *)
@@ -510,14 +536,16 @@ let print id fn =
   let pp_cmds =
    begin
     try
-     let {D.const_body=val0 ; D.const_type = typ} = G.lookup_constant sp in
+     let {D.const_body=val0 ; D.const_type = typ ; D.const_hyps = hyps} =
+      G.lookup_constant sp in
+     let hyps = string_list_of_named_context_list hyps in
      let typ = T.body_of_type typ in
       begin
        match val0 with
-          None -> print_axiom id typ (Actual "")
+          None -> print_axiom id typ [] hyps
         | Some lcvr ->
            match !lcvr with
-              D.Cooked c -> print_definition id c typ (Actual "")
+              D.Cooked c -> print_definition id c typ [] hyps
             | D.Recipe _ ->
                print_string " COOKING THE RECIPE\n" ;
                ignore (D.cook_constant lcvr) ;
@@ -527,17 +555,18 @@ let print id fn =
                 begin
                  match val0 with
                    Some {contents= D.Cooked c} ->
-                    print_definition id c typ (Actual "")
+                    print_definition id c typ [] hyps
                  | _ -> Util.error "COOKING FAILED"
                 end
           end
     with
      Not_found ->
       try
-       let {D.mind_packets=packs ; D.mind_nparams=nparams} =
+       let {D.mind_packets=packs ; D.mind_nparams=nparams ; D.mind_hyps=hyps} =
         G.lookup_mind sp
        in
-        print_mutual_inductive packs (Actual "") nparams
+        let hyps = string_list_of_named_context_list hyps in
+         print_mutual_inductive packs [] hyps nparams
       with
        Not_found ->
         try
@@ -619,28 +648,29 @@ let print_object o id sp dn fv =
    match tag with
       "CONSTANT"  (* = Definition, Theorem *)
     | "PARAMETER" (* = Axiom *) ->
-         (*CSC: QUI CI SONO ANCHE LE VARIABILI, CREDO, CHIAMATE const_hyps *)
-(*
-         let {D.const_body=val0 ; D.const_type = typ} = G.lookup_constant sp in
-*)
-let {D.const_body=val0 ; D.const_type = typ ; D.const_hyps = hyps} = G.lookup_constant sp in
-if (Names.string_of_id id) = "SN" then
- List.iter (fun (id,_,_) -> print_string ("*** " ^ N.string_of_id id ^ "\n")) hyps ;
+        let {D.const_body=val0 ; D.const_type = typ ; D.const_hyps = hyps} =
+         G.lookup_constant sp
+        in
+         let hyps = string_list_of_named_context_list hyps in
          let typ = T.body_of_type typ in
           begin
            match val0 with
-              None -> print_axiom id typ fv
+              None -> print_axiom id typ fv hyps
             | Some lcvr ->
                match !lcvr with
-                  D.Cooked c -> print_definition id c typ fv
+                  D.Cooked c -> print_definition id c typ fv hyps
                 | D.Recipe _ -> Util.anomaly "trying to print a recipe"
           end
     | "INDUCTIVE" ->
          (*CSC: QUI CI SONO ANCHE LE VARIABILI, CREDO, CHIAMATE mind_hyps *)
-         let {D.mind_packets=packs ; D.mind_nparams=nparams} =
-          G.lookup_mind sp
+         let
+          {D.mind_packets=packs ;
+           D.mind_nparams=nparams ;
+           D.mind_hyps = hyps
+          } = G.lookup_mind sp
          in
-           print_mutual_inductive packs fv nparams
+          let hyps = string_list_of_named_context_list hyps in
+           print_mutual_inductive packs fv hyps nparams
     | "VARIABLE" ->
 (*V7 DON'T KNOW HOW TO DO IT
         let (_,typ) = G.lookup_named id in
@@ -698,7 +728,7 @@ and print_node n id sp bprintleaf dn =
             toprint := (id,sp,sp,o,!pvars,dn)::!toprint
            else
             (* this is a local term *)
-            print_object o id sp dn (Possible (pvars_to_string !pvars)) ;
+            print_object o id sp dn !pvars ;
             print_if_verbose ("OK, stampo " ^ Names.string_of_id id ^ "\n")
           end
          else
@@ -738,7 +768,6 @@ and print_node n id sp bprintleaf dn =
 (* print_library_segment on all its sons                                     *)
 let print_closed_section s ls dn =
  let module L = Lib in
- let module C = Cooking in
   toprint := [] ;
   (*CSC: this should always be empty yet! But just to be sure... :-) *)
   pvars := [] ;
@@ -750,10 +779,10 @@ let print_closed_section s ls dn =
       (id,usp,csp,uo,pv,dn) ->
        print_if_verbose ("\nCooked=" ^ (Names.string_of_path csp) ^
         "\tUncooked=" ^ (Names.string_of_path usp)) ;
-       let formal_vars = C.add_cooking_information csp pv in
+       let formal_vars = pv in
         pvars := pv ;
         (*CSC Actual was Some *)
-        print_object uo id usp dn (Actual formal_vars)
+        print_object uo id usp dn formal_vars
    ) !toprint ;
   print_if_verbose "\n/Module\n" ;
 ;;