From 04f22df647f35080b499b720bca7bc0eb1794c64 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 28 Aug 2008 10:33:25 +0000
Subject: [PATCH] cicDischarge: new module for discharging the explicit
 variables occurring in a               CiC object. This is used in the
 procedural/declarative 	      reconstruction of Coq's library (es
 Coq/CoRN devels) cicUniv: we add a default_ugraph set for now to
 oblivio_ugraph acic_procedural: improved error handling depend, depend.opt:
 we updated some

---
 .../components/acic_procedural/.depend        |   4 +-
 .../components/acic_procedural/.depend.opt    |   4 +-
 .../acic_procedural/acic2Procedural.ml        |  20 +-
 .../acic_procedural/proceduralConversion.ml   |  14 +-
 .../acic_procedural/proceduralHelpers.ml      | 138 +++++++++-
 .../acic_procedural/proceduralHelpers.mli     |   6 +-
 .../acic_procedural/proceduralOptimizer.ml    |  38 +--
 helm/software/components/cic/.depend          |   8 +-
 helm/software/components/cic/.depend.opt      |   8 +-
 helm/software/components/cic/cicUniv.ml       |   2 +
 helm/software/components/cic/cicUniv.mli      |   4 +
 .../components/cic_disambiguation/.depend     |   4 +-
 .../components/cic_disambiguation/.depend.opt |   4 +-
 .../components/cic_proof_checking/.depend     |   2 +
 .../components/cic_proof_checking/.depend.opt |   2 +
 .../components/cic_proof_checking/Makefile    |   1 +
 .../cic_proof_checking/cicDischarge.ml        | 247 ++++++++++++++++++
 .../cic_proof_checking/cicDischarge.mli       |  34 +++
 helm/software/components/content_pres/.depend |   4 +-
 .../components/content_pres/.depend.opt       |  15 +-
 helm/software/components/tactics/.depend      |  48 ++--
 helm/software/components/tactics/.depend.opt  |  48 ++--
 22 files changed, 526 insertions(+), 129 deletions(-)
 create mode 100644 helm/software/components/cic_proof_checking/cicDischarge.ml
 create mode 100644 helm/software/components/cic_proof_checking/cicDischarge.mli

diff --git a/helm/software/components/acic_procedural/.depend b/helm/software/components/acic_procedural/.depend
index f0b67ebc3..caf6b8d45 100644
--- a/helm/software/components/acic_procedural/.depend
+++ b/helm/software/components/acic_procedural/.depend
@@ -10,8 +10,8 @@ proceduralTypes.cmo: proceduralHelpers.cmi proceduralTypes.cmi
 proceduralTypes.cmx: proceduralHelpers.cmx proceduralTypes.cmi 
 proceduralMode.cmo: proceduralClassify.cmi proceduralMode.cmi 
 proceduralMode.cmx: proceduralClassify.cmx proceduralMode.cmi 
-proceduralConversion.cmo: proceduralConversion.cmi 
-proceduralConversion.cmx: proceduralConversion.cmi 
+proceduralConversion.cmo: proceduralHelpers.cmi proceduralConversion.cmi 
+proceduralConversion.cmx: proceduralHelpers.cmx proceduralConversion.cmi 
 acic2Procedural.cmo: proceduralTypes.cmi proceduralHelpers.cmi \
     proceduralConversion.cmi proceduralClassify.cmi acic2Procedural.cmi 
 acic2Procedural.cmx: proceduralTypes.cmx proceduralHelpers.cmx \
diff --git a/helm/software/components/acic_procedural/.depend.opt b/helm/software/components/acic_procedural/.depend.opt
index f0b67ebc3..caf6b8d45 100644
--- a/helm/software/components/acic_procedural/.depend.opt
+++ b/helm/software/components/acic_procedural/.depend.opt
@@ -10,8 +10,8 @@ proceduralTypes.cmo: proceduralHelpers.cmi proceduralTypes.cmi
 proceduralTypes.cmx: proceduralHelpers.cmx proceduralTypes.cmi 
 proceduralMode.cmo: proceduralClassify.cmi proceduralMode.cmi 
 proceduralMode.cmx: proceduralClassify.cmx proceduralMode.cmi 
-proceduralConversion.cmo: proceduralConversion.cmi 
-proceduralConversion.cmx: proceduralConversion.cmi 
+proceduralConversion.cmo: proceduralHelpers.cmi proceduralConversion.cmi 
+proceduralConversion.cmx: proceduralHelpers.cmx proceduralConversion.cmi 
 acic2Procedural.cmo: proceduralTypes.cmi proceduralHelpers.cmi \
     proceduralConversion.cmi proceduralClassify.cmi acic2Procedural.cmi 
 acic2Procedural.cmx: proceduralTypes.cmx proceduralHelpers.cmx \
diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index 380e52efe..deb3088f2 100644
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -146,12 +146,6 @@ try
    with Not_found -> `Type (CicUniv.fresh())
 with Invalid_argument _ -> failwith "A2P.get_sort"
 *)
-let get_type msg st bo =
-try   
-   let ty, _ = TC.type_of_aux' [] st.context (H.cic bo) Un.oblivion_ugraph in
-   ty
-with e -> failwith (msg ^ ": " ^ Printexc.to_string e)
-
 let get_entry st id =
    let rec aux = function
       | []                                        -> assert false
@@ -160,16 +154,6 @@ let get_entry st id =
    in
    aux st.context
 
-let get_ind_names uri tno =
-try   
-   let ts = match E.get_obj Un.oblivion_ugraph uri with
-      | C.InductiveDefinition (ts, _, _, _), _ -> ts 
-      | _                                      -> assert false
-   in
-   match List.nth ts tno with
-      | (_, _, _, cs) -> List.map fst cs  
-with Invalid_argument _ -> failwith "A2P.get_ind_names"
-
 let string_of_atomic = function
    | C.ARel (_, _, _, s)               -> s
    | C.AVar (_, uri, _)                -> H.name_of_uri uri None None
@@ -187,6 +171,8 @@ let get_sub_names head l =
    let names, _ = List.fold_left map ([], 1) l in 
    List.rev names
 
+let get_type msg st t = H.get_type msg st.context (H.cic t) 
+
 (* proof construction *******************************************************)
 
 let anonymous_premise = C.Name "PREMISE"
@@ -378,7 +364,7 @@ and proc_appl st what hd tl =
 	    let classes2, tl2, _, where = split2_last classes tl in
 	    let script2 = List.rev (mk_arg st where) @ script in
 	    let synth2 = I.S.add 1 synth in
-	    let names = get_ind_names uri tyno in
+	    let names = H.get_ind_names uri tyno in
 	    let qs = proc_bkd_proofs (next st) synth2 names classes2 tl2 in
             if List.length qs <> List.length names then
 	       let qs = proc_bkd_proofs (next st) synth [] classes tl in
diff --git a/helm/software/components/acic_procedural/proceduralConversion.ml b/helm/software/components/acic_procedural/proceduralConversion.ml
index e42ad490e..3eadc2fcf 100644
--- a/helm/software/components/acic_procedural/proceduralConversion.ml
+++ b/helm/software/components/acic_procedural/proceduralConversion.ml
@@ -26,18 +26,16 @@
 module C    = Cic
 module E    = CicEnvironment
 module Un   = CicUniv
-module TC   = CicTypeChecker 
-module D    = Deannotate
+module TC   = CicTypeChecker
 module UM   = UriManager
 module Rd   = CicReduction
 module PEH  = ProofEngineHelpers
 module PT   = PrimitiveTactics
-
 module DTI  = DoubleTypeInference
 
-(* helpers ******************************************************************)
+module H    = ProceduralHelpers
 
-let cic = D.deannotate_term
+(* helpers ******************************************************************)
 
 let rec list_sub start length = function
    | _  :: tl when start  > 0 -> list_sub (pred start) length tl
@@ -126,7 +124,7 @@ let clear_absts m =
       | C.ALambda (_, _, _, t) when n > 0  -> 
          aux 0 (pred n) (lift 1 (-1) t)
       | t                      when n > 0  ->
-	    Printf.eprintf "CLEAR: %u %s\n" n (CicPp.ppterm (cic t));
+	    Printf.eprintf "CLEAR: %u %s\n" n (CicPp.ppterm (H.cic t));
 	    assert false 
       | t                                  -> t
    in 
@@ -240,8 +238,8 @@ let clear c hyp =
    aux [] c
 
 let elim_inferred_type context goal arg using cpattern =
-   let metasenv, ugraph = [], Un.oblivion_ugraph in 
-   let ety, _ugraph = TC.type_of_aux' metasenv context using ugraph in
+   let metasenv, ugraph = [], Un.default_ugraph in
+   let ety = H.get_type "elim_inferred_type" context using in
    let _splits, args_no = PEH.split_with_whd (context, ety) in
    let _metasenv, predicate, _arg, actual_args = PT.mk_predicate_for_elim 
       ~context ~metasenv ~ugraph ~goal ~arg ~using ~cpattern ~args_no
diff --git a/helm/software/components/acic_procedural/proceduralHelpers.ml b/helm/software/components/acic_procedural/proceduralHelpers.ml
index d6f844d71..91f7016cd 100644
--- a/helm/software/components/acic_procedural/proceduralHelpers.ml
+++ b/helm/software/components/acic_procedural/proceduralHelpers.ml
@@ -35,6 +35,102 @@ module D    = Deannotate
 module PER  = ProofEngineReduction
 module Ut   = CicUtil
 
+(* raw cic prettyprinter ****************************************************)
+
+let xiter out so ss sc map l =
+   let rec aux = function
+      | hd :: tl when tl <> [] -> map hd; out ss; aux tl
+      | hd :: tl               -> map hd; aux tl
+      | []                     -> ()
+   in
+   out so; aux l; out sc
+
+let abst s w = Some (s, C.Decl w)
+
+let abbr s v w = Some (s, C.Def (v, w))
+
+let pp_sort out = function
+   | C.Type _  -> out "\Type"
+   | C.Prop    -> out "\Prop"
+   | C.CProp _ -> out "\CProp"
+   | C.Set     -> out "\Set"
+
+let pp_name out = function
+   | C.Name s    -> out s
+   | C.Anonymous -> out "_"
+
+let pp_rel out c i =
+   try match List.nth c (pred i) with
+      | None           -> out (Printf.sprintf "%u[?]" i)
+      | Some (s, _)    -> out (Printf.sprintf "%u[" i); pp_name out s; out "]"
+   with Failure "nth" -> out (Printf.sprintf "%u[%u]" i (List.length c - i))
+
+let pp_implict out = function
+   | None         -> out "?"
+   | Some `Closed -> out "?[Closed]" 
+   | Some `Type   -> out "?[Type]"
+   | Some `Hole   -> out "?[Hole]"
+
+let pp_uri out a =
+   out (Printf.sprintf "%s<%s>" (UM.name_of_uri a) (UM.string_of_uri a)) 
+
+let rec pp_term out e c = function
+   | C.Sort h                      -> pp_sort out h
+   | C.Rel i                       -> pp_rel out c i
+   | C.Implicit x                  -> pp_implict out x
+   | C.Meta (i, iss)               ->
+      let map = function None   -> out "_" | Some v -> pp_term out e c v in
+      out (Printf.sprintf "?%u" i); xiter out "[" "; " "]" map iss
+   | C.Var (a, xss)              ->
+      pp_uri out a; pp_xss out e c xss
+   | C.Const (a, xss)              ->
+      pp_uri out a; pp_xss out e c xss
+   | C.MutInd (a, m, xss)          ->
+      pp_uri out a; out (Printf.sprintf "/%u" m);
+      pp_xss out e c xss
+   | C.MutConstruct (a, m, n, xss) ->
+      pp_uri out a; out (Printf.sprintf "/%u/%u" m n);
+      pp_xss out e c xss
+   | C.Cast (v, w)                 ->
+      out "type "; pp_term out e c w; out " contains "; pp_term out e c v
+   | C.Appl vs                     ->
+      xiter out "(" " @ " ")" (pp_term out e c) vs
+   | C.MutCase (a, m, w, v, vs)    ->
+      out "match "; pp_term out e c v;
+      out " of "; pp_uri out a; out (Printf.sprintf "/%u" m);
+      out " to "; pp_term out e c w;
+      xiter out " cases " " | " "" (pp_term out e c) vs
+   | C.Prod (s, w, t)             ->
+      out "forall "; pp_name out s; out " of "; pp_term out e c w;
+      out " in "; pp_term out e (abst s w :: c) t
+   | C.Lambda (s, w, t)            ->
+      out "fun "; pp_name out s; out " of "; pp_term out e c w;
+      out " in "; pp_term out e (abst s w :: c) t
+   | C.LetIn (s, v, w, t)          ->
+      out "let "; pp_name out s; 
+      out " def "; pp_term out e c v; out " of "; pp_term out e c w;
+      out " in "; pp_term out e (abbr s v w :: c) t
+   | C.Fix (i, fs)                 ->
+      let map c (s, _, w, v) = abbr (C.Name s) v w :: c in
+      let c' = List.fold_left map c fs in
+      let map (s, i, w, v) =
+         out (Printf.sprintf "%s[%u] def " s i); pp_term out e c' v; 
+	 out " of "; pp_term out e c w;
+      in
+      xiter out "let rec " " and " " in " map fs; pp_rel out c' (succ i)
+   | C.CoFix (i, fs)                 ->
+      let map c (s, w, v) = abbr (C.Name s) v w :: c in
+      let c' = List.fold_left map c fs in
+      let map (s, w, v) =
+         out s; pp_term out e c' v; 
+	 out " of "; pp_term out e c w;
+      in
+      xiter out "let corec " " and " " in " map fs; pp_rel out c' (succ i)
+
+and pp_xss out e c xss = 
+   let map (a, v) = pp_uri out a; out " <- "; pp_term out e c v in
+   xiter out "[" "; " "]" map xss 
+
 (* fresh name generator *****************************************************)
 
 let split name =
@@ -83,19 +179,25 @@ let compose f g x = f (g x)
 let fst3 (x, _, _) = x
 
 let refine c t =
-   try let t, _, _, _ = Rf.type_of_aux' [] c t Un.oblivion_ugraph in t
+   try let t, _, _, _ = Rf.type_of_aux' [] c t Un.default_ugraph in t
    with e -> 
       Printf.eprintf "REFINE EROR: %s\n" (Printexc.to_string e);
       Printf.eprintf "Ref: context: %s\n" (Pp.ppcontext c);
       Printf.eprintf "Ref: term   : %s\n" (Pp.ppterm t);
       raise e
 
-let get_type c t =
-   try let ty, _ = TC.type_of_aux' [] c t Un.oblivion_ugraph in ty
-   with e -> 
-      Printf.eprintf "TC: context: %s\n" (Pp.ppcontext c);
-      Printf.eprintf "TC: term   : %s\n" (Pp.ppterm t);
-      raise e
+let get_type msg c t =
+   let log s =
+      prerr_endline ("TC: " ^ s); 
+      prerr_endline ("TC: context: " ^ Pp.ppcontext c);
+      prerr_string "TC: term   : "; pp_term prerr_string [] c t;
+      prerr_newline (); prerr_endline ("TC: location: " ^ msg)
+   in   
+   try let ty, _ = TC.type_of_aux' [] c t Un.default_ugraph in ty with
+      | TC.TypeCheckerFailure s as e ->
+        log ("failure: " ^ Lazy.force s); raise e        
+      | TC.AssertFailure s as e      -> 
+        log ("assert : " ^ Lazy.force s); raise e
 
 let get_tail c t =
    match PEH.split_with_whd (c, t) with
@@ -103,7 +205,7 @@ let get_tail c t =
       | _               -> assert false
 
 let is_proof c t =
-   match get_tail c (get_type c (get_type c t)) with
+   match get_tail c (get_type "is_proof 1" c (get_type "is_proof 2" c t)) with
       | C.Sort C.Prop -> true
       | C.Sort _      -> false
       | _             -> assert false 
@@ -126,13 +228,23 @@ let is_not_atomic = function
 let is_atomic t = not (is_not_atomic t)
 
 let get_ind_type uri tyno =
-   match E.get_obj Un.oblivion_ugraph uri with
+   match E.get_obj Un.default_ugraph uri with
       | C.InductiveDefinition (tys, _, lpsno, _), _ -> lpsno, List.nth tys tyno
       | _                                           -> assert false
 
+let get_ind_names uri tno =
+try   
+   let ts = match E.get_obj Un.default_ugraph uri with
+      | C.InductiveDefinition (ts, _, _, _), _ -> ts 
+      | _                                      -> assert false
+   in
+   match List.nth ts tno with
+      | (_, _, _, cs) -> List.map fst cs  
+with Invalid_argument _ -> failwith "get_ind_names"
+
 let get_default_eliminator context uri tyno ty =
    let _, (name, _, _, _) = get_ind_type uri tyno in
-   let ext = match get_tail context (get_type context ty) with
+   let ext = match get_tail context (get_type "get_def_elim" context ty) with
       | C.Sort C.Prop      -> "_ind"
       | C.Sort C.Set       -> "_rec"
       | C.Sort (C.CProp _) -> "_rect"
@@ -146,13 +258,13 @@ let get_default_eliminator context uri tyno ty =
    C.Const (uri, [])
 
 let get_ind_parameters c t =
-   let ty = get_type c t in
+   let ty = get_type "get_ind_pars 1" c t in
    let ps = match get_tail c ty with
       | C.MutInd _                  -> []
       | C.Appl (C.MutInd _ :: args) -> args
       | _                           -> assert false
    in
-   let disp = match get_tail c (get_type c ty) with
+   let disp = match get_tail c (get_type "get_ind_pars 2" c ty) with
       | C.Sort C.Prop -> 0
       | C.Sort _      -> 1
       | _             -> assert false
@@ -175,7 +287,7 @@ let name_of_uri uri tyno cno =
    let get_ind_type tys tyno =
       let s, _, _, cs = List.nth tys tyno in s, cs
    in
-   match (fst (E.get_obj Un.oblivion_ugraph uri)), tyno, cno with
+   match (fst (E.get_obj Un.default_ugraph uri)), tyno, cno with
       | C.Variable (s, _, _, _, _), _, _                     -> s
       | C.Constant (s, _, _, _, _), _, _                     -> s
       | C.InductiveDefinition (tys, _, _, _), Some i, None   ->
diff --git a/helm/software/components/acic_procedural/proceduralHelpers.mli b/helm/software/components/acic_procedural/proceduralHelpers.mli
index a02d8ab1d..770534af6 100644
--- a/helm/software/components/acic_procedural/proceduralHelpers.mli
+++ b/helm/software/components/acic_procedural/proceduralHelpers.mli
@@ -23,6 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
+val pp_term:
+   (string -> unit) -> Cic.metasenv -> Cic.context -> Cic.term -> unit
 val mk_fresh_name:
    Cic.context -> Cic.name -> Cic.name
 val list_map_cps:
@@ -36,7 +38,7 @@ val fst3:
 val refine:
    Cic.context -> Cic.term -> Cic.term
 val get_type:
-   Cic.context -> Cic.term -> Cic.term
+   string -> Cic.context -> Cic.term -> Cic.term
 val is_proof:
    Cic.context -> Cic.term -> bool
 val is_sort:
@@ -49,6 +51,8 @@ val is_atomic:
    Cic.term -> bool
 val get_ind_type:
    UriManager.uri -> int -> int * Cic.inductiveType
+val get_ind_names:
+   UriManager.uri -> int -> string list
 val get_default_eliminator:
   Cic.context -> UriManager.uri -> int -> Cic.term -> Cic.term
 val get_ind_parameters:
diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml
index e16828fa7..20e04d322 100644
--- a/helm/software/components/acic_procedural/proceduralOptimizer.ml
+++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml
@@ -23,9 +23,11 @@
  * http://cs.unibo.it/helm/.
  *)
 
+module UM   = UriManager
 module C    = Cic
 module Pp   = CicPp
 module I    = CicInspect
+module E    = CicEnvironment
 module S    = CicSubstitution
 module DTI  = DoubleTypeInference
 module HEL  = HExtlib
@@ -40,15 +42,9 @@ module Cl   = ProceduralClassify
 
 let defined_premise = "DEFINED"
 
-let get_type msg c bo =
-try   
-   let ty, _ = TC.type_of_aux' [] c bo Un.oblivion_ugraph in
-   ty
-with e -> failwith (msg ^ ": " ^ Printexc.to_string e)
-
 let define c v =
    let name = C.Name defined_premise in
-   let ty = get_type "define" c v in
+   let ty = H.get_type "define" c v in
    C.LetIn (name, v, ty, C.Rel 1)
 
 let clear_absts m =
@@ -80,7 +76,7 @@ let rec opt1_letin g es c name v w t =
       let g = function
          | C.LetIn (nname, vv, ww, tt) when H.is_proof c v ->
 	    let eentry = Some (nname, C.Def (vv, ww)) in
-	    let ttw = get_type "opt1_letin 1" (eentry :: c) tt in
+	    let ttw = H.get_type "opt1_letin 1" (eentry :: c) tt in
 	    let x = C.LetIn (nname, vv, ww,
              C.LetIn (name, tt, ttw, S.lift_from 2 1 t)) in
 	    HLog.warn "Optimizer: swap 1"; opt1_proof g true c x 
@@ -109,7 +105,7 @@ and opt1_appl g es c t vs =
 	    HLog.warn "Optimizer: swap 2"; opt1_proof g true c x
          | C.Lambda (name, ww, tt) ->
 	    let v, vs = List.hd vs, List.tl vs in
-            let w = get_type "opt1_appl 1" c v in
+            let w = H.get_type "opt1_appl 1" c v in
 	    let x = C.Appl (C.LetIn (name, v, w, tt) :: vs) in
 	    HLog.warn "Optimizer: remove 2"; opt1_proof g true c x
 	 | C.Appl vvs              ->
@@ -129,7 +125,7 @@ and opt1_appl g es c t vs =
 	       | _, []                   -> assert false
 	    in
 	    let h () =
-	       let classes, conclusion = Cl.classify c (H.get_type c t) in
+	       let classes, conclusion = Cl.classify c (H.get_type "opt1_appl 3" c t) in
 	       let csno, vsno = List.length classes, List.length vs in
 	       if csno < vsno then
 	          let vvs, vs = HEL.split_nth csno vs in
@@ -150,7 +146,7 @@ and opt1_appl g es c t vs =
                   let prev = List.map (S.lift 1) prev in
                   let vs = List.map (S.lift 1) vs in
 		  let y = C.Appl (t :: List.rev prev @ tt :: vs) in
-                  let ww = get_type "opt1_appl 2" c vv in
+                  let ww = H.get_type "opt1_appl 2" c vv in
 		  let x = C.LetIn (name, vv, ww, y) in  
 		  HLog.warn "Optimizer: swap 3"; opt1_proof g true c x
 	       | v :: vs                      -> aux h (v :: prev) vs
@@ -247,9 +243,9 @@ and opt2_appl g c t vs =
    let g vs =
       let x = C.Appl (t :: vs) in
       let vsno = List.length vs in
-      let _, csno = PEH.split_with_whd (c, H.get_type c t) in
+      let _, csno = PEH.split_with_whd (c, H.get_type "opt2_appl 1" c t) in
       if vsno < csno then 
-         let tys, _ = PEH.split_with_whd (c, H.get_type c x) in
+         let tys, _ = PEH.split_with_whd (c, H.get_type "opt2_appl 2" c x) in
 	 let tys = List.rev (List.tl tys) in
 	 let tys, _ = HEL.split_nth (csno - vsno) tys in
          HLog.warn "Optimizer: eta 1"; eta_expand g tys x
@@ -258,7 +254,7 @@ and opt2_appl g c t vs =
    H.list_map_cps g (fun h -> opt2_term h c) vs
 
 and opt2_other g c t =
-   let tys, csno = PEH.split_with_whd (c, H.get_type c t) in
+   let tys, csno = PEH.split_with_whd (c, H.get_type "opt2_other" c t) in
    if csno > 0 then begin
       let tys = List.rev (List.tl tys) in      
       HLog.warn "Optimizer: eta 2"; eta_expand g tys t 
@@ -281,11 +277,19 @@ let optimize_obj = function
       let g bo = 
          Printf.eprintf "Optimized : %s\nPost Nodes: %u\n" 
 	    (Pp.ppterm bo) (I.count_nodes 0 bo);
-	 let _ = H.get_type [] (C.Cast (bo, ty)) in
+	 prerr_string "H.pp_term : ";
+	 H.pp_term prerr_string [] [] bo; prerr_newline ();
+	 let _ = H.get_type "opt" [] (C.Cast (bo, ty)) in
 	 C.Constant (name, Some bo, ty, pars, attrs)
       in
       Printf.eprintf "BEGIN: %s\nPre Nodes : %u\n" 
          name (I.count_nodes 0 bo);
-      begin try opt1_term g (* (opt2_term g []) *) true [] bo
-      with e -> failwith ("PPP: " ^ Printexc.to_string e) end
+      begin try opt1_term g (* (opt2_term g []) *) true [] bo with
+        | E.Object_not_found uri ->
+	   let msg = "optimize_obj: object not found: " ^ UM.string_of_uri uri in
+	   failwith msg 
+        | e                      -> 
+	   let msg = "optimize_obj: " ^ Printexc.to_string e in
+	   failwith msg
+      end
    | obj                                         -> obj
diff --git a/helm/software/components/cic/.depend b/helm/software/components/cic/.depend
index 538d4b10d..595fd4b3a 100644
--- a/helm/software/components/cic/.depend
+++ b/helm/software/components/cic/.depend
@@ -9,12 +9,12 @@ path_indexing.cmi: cic.cmo
 cicInspect.cmi: cic.cmo 
 cic.cmo: cicUniv.cmi 
 cic.cmx: cicUniv.cmx 
-unshare.cmo: cic.cmo unshare.cmi 
-unshare.cmx: cic.cmx unshare.cmi 
 cicUniv.cmo: cicUniv.cmi 
 cicUniv.cmx: cicUniv.cmi 
-deannotate.cmo: cic.cmo deannotate.cmi 
-deannotate.cmx: cic.cmx deannotate.cmi 
+unshare.cmo: cicUniv.cmi cic.cmo unshare.cmi 
+unshare.cmx: cicUniv.cmx cic.cmx unshare.cmi 
+deannotate.cmo: unshare.cmi cic.cmo deannotate.cmi 
+deannotate.cmx: unshare.cmx cic.cmx deannotate.cmi 
 cicParser.cmo: deannotate.cmi cicUniv.cmi cic.cmo cicParser.cmi 
 cicParser.cmx: deannotate.cmx cicUniv.cmx cic.cmx cicParser.cmi 
 cicUtil.cmo: cicUniv.cmi cic.cmo cicUtil.cmi 
diff --git a/helm/software/components/cic/.depend.opt b/helm/software/components/cic/.depend.opt
index c1e2b0beb..0ff8e697c 100644
--- a/helm/software/components/cic/.depend.opt
+++ b/helm/software/components/cic/.depend.opt
@@ -9,12 +9,12 @@ path_indexing.cmi: cic.cmx
 cicInspect.cmi: cic.cmx 
 cic.cmo: cicUniv.cmi 
 cic.cmx: cicUniv.cmx 
-unshare.cmo: cic.cmx unshare.cmi 
-unshare.cmx: cic.cmx unshare.cmi 
 cicUniv.cmo: cicUniv.cmi 
 cicUniv.cmx: cicUniv.cmi 
-deannotate.cmo: cic.cmx deannotate.cmi 
-deannotate.cmx: cic.cmx deannotate.cmi 
+unshare.cmo: cicUniv.cmi cic.cmx unshare.cmi 
+unshare.cmx: cicUniv.cmx cic.cmx unshare.cmi 
+deannotate.cmo: unshare.cmi cic.cmx deannotate.cmi 
+deannotate.cmx: unshare.cmx cic.cmx deannotate.cmi 
 cicParser.cmo: deannotate.cmi cicUniv.cmi cic.cmx cicParser.cmi 
 cicParser.cmx: deannotate.cmx cicUniv.cmx cic.cmx cicParser.cmi 
 cicUtil.cmo: cicUniv.cmi cic.cmx cicUtil.cmi 
diff --git a/helm/software/components/cic/cicUniv.ml b/helm/software/components/cic/cicUniv.ml
index 03088410f..3074f2a78 100644
--- a/helm/software/components/cic/cicUniv.ml
+++ b/helm/software/components/cic/cicUniv.ml
@@ -357,6 +357,8 @@ type universe_graph = bag * UriManager.UriSet.t * bool
 
 let empty_ugraph = empty_bag, UriManager.UriSet.empty, false
 let oblivion_ugraph = empty_bag, UriManager.UriSet.empty, true
+(* FG: default choice for a ugraph ??? *)
+let default_ugraph = oblivion_ugraph   
 
 let current_index_anon = ref (-1)
 let current_index_named = ref (-1)
diff --git a/helm/software/components/cic/cicUniv.mli b/helm/software/components/cic/cicUniv.mli
index fa7f544c0..8a24614c2 100644
--- a/helm/software/components/cic/cicUniv.mli
+++ b/helm/software/components/cic/cicUniv.mli
@@ -60,6 +60,10 @@ val empty_ugraph: universe_graph
 (* an universe that does nothing: i.e. no constraints are kept, no merges.. *)
 val oblivion_ugraph: universe_graph
 
+(* one of the previous two, no set to empty_ugraph *)
+val default_ugraph: universe_graph
+
+
 (*
   These are the real functions to add eq/ge/gt constraints 
   to the passed graph, returning an updated graph or raising
diff --git a/helm/software/components/cic_disambiguation/.depend b/helm/software/components/cic_disambiguation/.depend
index 2ca28ce61..ca4124461 100644
--- a/helm/software/components/cic_disambiguation/.depend
+++ b/helm/software/components/cic_disambiguation/.depend
@@ -8,5 +8,5 @@ disambiguate.cmo: disambiguateTypes.cmi disambiguateChoices.cmi \
     disambiguate.cmi 
 disambiguate.cmx: disambiguateTypes.cmx disambiguateChoices.cmx \
     disambiguate.cmi 
-number_notation.cmo: disambiguateChoices.cmi 
-number_notation.cmx: disambiguateChoices.cmx 
+number_notation.cmo: disambiguateTypes.cmi disambiguateChoices.cmi 
+number_notation.cmx: disambiguateTypes.cmx disambiguateChoices.cmx 
diff --git a/helm/software/components/cic_disambiguation/.depend.opt b/helm/software/components/cic_disambiguation/.depend.opt
index 2ca28ce61..ca4124461 100644
--- a/helm/software/components/cic_disambiguation/.depend.opt
+++ b/helm/software/components/cic_disambiguation/.depend.opt
@@ -8,5 +8,5 @@ disambiguate.cmo: disambiguateTypes.cmi disambiguateChoices.cmi \
     disambiguate.cmi 
 disambiguate.cmx: disambiguateTypes.cmx disambiguateChoices.cmx \
     disambiguate.cmi 
-number_notation.cmo: disambiguateChoices.cmi 
-number_notation.cmx: disambiguateChoices.cmx 
+number_notation.cmo: disambiguateTypes.cmi disambiguateChoices.cmi 
+number_notation.cmx: disambiguateTypes.cmx disambiguateChoices.cmx 
diff --git a/helm/software/components/cic_proof_checking/.depend b/helm/software/components/cic_proof_checking/.depend
index 06b9188a0..84367a6e9 100644
--- a/helm/software/components/cic_proof_checking/.depend
+++ b/helm/software/components/cic_proof_checking/.depend
@@ -22,3 +22,5 @@ freshNamesGenerator.cmo: cicTypeChecker.cmi cicSubstitution.cmi \
     freshNamesGenerator.cmi 
 freshNamesGenerator.cmx: cicTypeChecker.cmx cicSubstitution.cmx \
     freshNamesGenerator.cmi 
+cicDischarge.cmo: cicEnvironment.cmi cicDischarge.cmi 
+cicDischarge.cmx: cicEnvironment.cmx cicDischarge.cmi 
diff --git a/helm/software/components/cic_proof_checking/.depend.opt b/helm/software/components/cic_proof_checking/.depend.opt
index 06b9188a0..84367a6e9 100644
--- a/helm/software/components/cic_proof_checking/.depend.opt
+++ b/helm/software/components/cic_proof_checking/.depend.opt
@@ -22,3 +22,5 @@ freshNamesGenerator.cmo: cicTypeChecker.cmi cicSubstitution.cmi \
     freshNamesGenerator.cmi 
 freshNamesGenerator.cmx: cicTypeChecker.cmx cicSubstitution.cmx \
     freshNamesGenerator.cmi 
+cicDischarge.cmo: cicEnvironment.cmi cicDischarge.cmi 
+cicDischarge.cmx: cicEnvironment.cmx cicDischarge.cmi 
diff --git a/helm/software/components/cic_proof_checking/Makefile b/helm/software/components/cic_proof_checking/Makefile
index b2ee8993f..a5f97bc1d 100644
--- a/helm/software/components/cic_proof_checking/Makefile
+++ b/helm/software/components/cic_proof_checking/Makefile
@@ -14,6 +14,7 @@ INTERFACE_FILES = \
 	cicReduction.mli \
 	cicTypeChecker.mli \
         freshNamesGenerator.mli \
+        cicDischarge.mli        \
 	$(NULL)
 IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
 
diff --git a/helm/software/components/cic_proof_checking/cicDischarge.ml b/helm/software/components/cic_proof_checking/cicDischarge.ml
new file mode 100644
index 000000000..49d6da890
--- /dev/null
+++ b/helm/software/components/cic_proof_checking/cicDischarge.ml
@@ -0,0 +1,247 @@
+(* Copyright (C) 2003-2005, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+module UM = UriManager
+module C  = Cic
+module Un = CicUniv
+module E  = CicEnvironment
+
+let hashtbl_size = 11
+
+let not_implemented =
+   "discharge of current proofs is not implemented yet"
+
+(* helper functions *********************************************************)
+
+let list_pos found l =
+   let rec aux n = function
+      | []       -> raise Not_found
+      | hd :: tl -> if found hd then n else aux (succ n) tl
+   in 
+   aux 0 l
+
+let sh a b = if a == b then a else b
+
+let rec list_map_sh map l = match l with
+   | []       -> l
+   | hd :: tl ->
+      let hd', tl' = map hd, list_map_sh map tl in
+      if hd' == hd && tl' == tl then l else
+      sh hd hd' :: sh tl tl'
+
+let flatten = function
+   | C.Appl vs :: tl -> vs @ tl
+   | ts              -> ts
+
+let vars_of_uri uri =
+   let obj, _ = E.get_obj Un.default_ugraph uri in
+   match obj with
+      | C.Constant (_, _, _, vars, _)
+      | C.Variable (_, _, _, vars, _)
+      | C.InductiveDefinition (_, vars, _, _)
+      | C.CurrentProof (_, _, _, _, vars, _)  -> vars
+
+let mk_arg s u =
+   try List.assq u s
+   with Not_found -> C.Var (u, [])
+
+(* main functions ***********************************************************)
+
+type status = {
+   du: UM.uri -> UM.uri;                (* uri discharge map               *)
+   c : C.context;                       (* var context of this object      *)
+   ls: (UM.uri, UM.uri list) Hashtbl.t; (* var lists of subobjects         *)
+   rl: UM.uri list;                     (* reverse var list of this object *)
+   h : int                              (* relocation index                *)
+}
+
+let add st k = {st with h = st.h + k}
+
+let discharge st u = st.h + list_pos (UM.eq u) st.rl
+
+let get_args st u =
+   try Hashtbl.find st.ls u
+   with Not_found -> 
+      let args = vars_of_uri u in
+      Hashtbl.add st.ls u args; args
+
+let rec discharge_term st t = match t with
+   | C.Implicit _
+   | C.Sort _
+   | C.Rel _                      -> t
+   | C.Const (u, s)               ->
+      let args = get_args st u in
+      if args = [] then t else
+      let s = List.map (mk_arg s) args in
+      C.Appl (C.Const (st.du u, []) :: discharge_nsubst st s)
+   | C.MutInd (u, m, s)           ->
+      let args = get_args st u in
+      if args = [] then t else
+      let s = List.map (mk_arg s) args in
+      C.Appl (C.MutInd (st.du u, m, []) :: discharge_nsubst st s)
+   | C.MutConstruct (u, m, n, s)  ->
+      let args = get_args st u in
+      if args = [] then t else
+      let s = List.map (mk_arg s) args in
+      C.Appl (C.MutConstruct (st.du u, m, n, []) :: discharge_nsubst st s)
+   | C.Var (u, s)                 ->
+      let args = get_args st u in
+      if args = [] then C.Rel (discharge st u) else
+      let s = List.map (mk_arg s) args in
+      C.Appl (C.Rel (discharge st u) :: discharge_nsubst st s)
+   | C.Meta (i, s)                ->
+      let s' = list_map_sh (discharge_usubst st) s in
+      if s' == s then t else C.Meta (i, s')
+   | C.Appl vs                    ->
+      let vs' = list_map_sh (discharge_term st) vs in
+      if vs' == vs then t else C.Appl (flatten vs')
+   | C.Cast (v, w)                ->
+      let v', w' = discharge_term st v, discharge_term st w in
+      if v' = v && w' = w then t else
+      C.Cast (sh v v', sh w w')
+   | C.MutCase (u, m, w, v, vs)   ->
+      let w', v', vs' = 
+         discharge_term st w, discharge_term st v,
+	 list_map_sh (discharge_term st) vs
+      in
+      if w' = w && v' = v && vs' == vs then t else
+      C.MutCase (st.du u, m, sh w w', sh v v', sh vs vs')
+   | C.Prod (b, w, v)             ->
+      let w', v' = discharge_term st w, discharge_term (add st 1) v in
+      if w' = w && v' = v then t else
+      C.Prod (b, sh w w', sh v v')
+   | C.Lambda (b, w, v)           ->
+      let w', v' = discharge_term st w, discharge_term (add st 1) v in
+      if w' = w && v' = v then t else
+      C.Lambda (b, sh w w', sh v v')
+   | C.LetIn (b, y, w, v)   ->
+      let y', w', v' = 
+         discharge_term st y, discharge_term st w, discharge_term (add st 1) v
+      in
+      if y' = y && w' = w && v' == v then t else
+      C.LetIn (b, sh y y', sh w w', sh v v')
+   | C.CoFix (i, s)         ->
+      let no = List.length s in
+      let s' = list_map_sh (discharge_cofun st no) s in
+      if s' == s then t else C.CoFix (i, s')
+   | C.Fix (i, s)         ->
+      let no = List.length s in
+      let s' = list_map_sh (discharge_fun st no) s in
+      if s' == s then t else C.Fix (i, s')
+
+and discharge_nsubst st s =
+   List.map (discharge_term st) s
+
+and discharge_usubst st s = match s with
+   | None   -> s
+   | Some t ->
+      let t' = discharge_term st t in
+      if t' == t then s else Some t'
+
+and discharge_cofun st no f =
+   let b, w, v = f in
+   let w', v' = discharge_term st w, discharge_term (add st no) v in
+   if w' = w && v' = v then f else
+   b, sh w w', sh v v'
+
+and discharge_fun st no f =
+   let b, i, w, v = f in
+   let w', v' = discharge_term st w, discharge_term (add st no) v in
+   if w' = w && v' = v then f else
+   b, i, sh w w', sh v v'
+
+let close is_type st t = 
+   let map t = function
+      | Some (b, C.Def (v, w)) -> C.LetIn (b, v, w, t)
+      | Some (b, C.Decl w)     ->
+         if is_type then C.Prod (b, w, t) else C.Lambda (b, w, t)
+      | None                   -> assert false
+   in   
+   List.fold_left map t st.c
+
+let discharge_con st con =
+   let b, v = con in
+   let v' = discharge_term st v in
+   if v' == v && st.rl = [] then con else b, close true st (sh v v')
+
+let discharge_type st ind_type =
+   let b, ind, w, cons = ind_type in
+   let w', cons' = discharge_term st w, list_map_sh (discharge_con st) cons in
+   if w' == w && cons' == cons && st.rl = [] then ind_type else
+   let w'' = close true st (sh w w') in
+   b, ind, w'', sh cons cons'
+
+let rec discharge_object du obj = 
+   let ls = Hashtbl.create hashtbl_size in match obj with
+   | C.Variable (b, None, w, vars, attrs)              ->
+      let st = init_status du ls vars in
+      let w' = discharge_term st w in
+      if w' = w && vars = [] then obj else
+      let w'' = close true st (sh w w') in
+      C.Variable (b, None, w'', [], attrs)
+   | C.Variable (b, Some v, w, vars, attrs)            ->
+      let st = init_status du ls vars in
+      let w', v' = discharge_term st w, discharge_term st v in
+      if w' = w && v' = v && vars = [] then obj else
+      let w'', v'' = close true st (sh w w'), close false st (sh v v') in
+      C.Variable (b, Some v'', w'', [], attrs)
+   | C.Constant (b, None, w, vars, attrs)              ->
+      let st = init_status du ls vars in
+      let w' = discharge_term st w in
+      if w' = w && vars = [] then obj else
+      let w'' = close true st (sh w w') in
+      C.Constant (b, None, w'', [], attrs)
+   | C.Constant (b, Some v, w, vars, attrs)            ->
+      let st = init_status du ls vars in
+      let w', v' = discharge_term st w, discharge_term st v in
+      if w' = w && v' = v && vars = [] then obj else
+      let w'', v'' = close true st (sh w w'), close false st (sh v v') in
+      C.Constant (b, Some v'', w'', [], attrs)
+   | C.InductiveDefinition (types, vars, lpsno, attrs) ->
+      let st = init_status du ls vars in
+      let types' = list_map_sh (discharge_type st) types in
+      if types' == types && vars = [] then obj else
+      let lpsno' = lpsno + List.length vars in
+      C.InductiveDefinition (sh types types', [], lpsno', attrs)
+   | C.CurrentProof _                                  ->
+      HLog.warn not_implemented; obj
+
+and discharge_uri du uri =
+   let obj, _ = E.get_obj Un.default_ugraph uri in
+   let obj' = discharge_object du obj in
+   obj', obj' == obj
+
+and discharge_vars du vars =
+   let map u =
+      match discharge_uri du u with
+         | C.Variable (b, None, w, _, _), _   -> Some (C.Name b, C.Decl w)
+         | C.Variable (b, Some v, w, _, _), _ -> Some (C.Name b, C.Def (v, w))
+	 | _                                  -> None
+   in
+   List.rev_map map vars
+
+and init_status du ls vars =
+   let c, rl = discharge_vars du vars, List.rev vars in
+   {du = du; c = c; ls = ls; rl = rl; h = 1} 
diff --git a/helm/software/components/cic_proof_checking/cicDischarge.mli b/helm/software/components/cic_proof_checking/cicDischarge.mli
new file mode 100644
index 000000000..447e2a344
--- /dev/null
+++ b/helm/software/components/cic_proof_checking/cicDischarge.mli
@@ -0,0 +1,34 @@
+(* Copyright (C) 2003-2005, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* discharges the explicit variables of the given object (with sharing)    *)
+(* the first argument is a map for relocating the uris of the dependencdes *)
+val discharge_object:
+   (UriManager.uri -> UriManager.uri) -> Cic.obj -> Cic.obj
+
+(* applies the previous function to the object at the given uri *)
+(* returns true if the object does not need discharging         *)
+val discharge_uri:
+   (UriManager.uri -> UriManager.uri) -> UriManager.uri -> Cic.obj * bool
diff --git a/helm/software/components/content_pres/.depend b/helm/software/components/content_pres/.depend
index 5ab78a89e..6dd0e78a1 100644
--- a/helm/software/components/content_pres/.depend
+++ b/helm/software/components/content_pres/.depend
@@ -23,9 +23,9 @@ boxPp.cmo: renderingAttrs.cmi mpresentation.cmi cicNotationPres.cmi box.cmi \
     boxPp.cmi 
 boxPp.cmx: renderingAttrs.cmx mpresentation.cmx cicNotationPres.cmx box.cmx \
     boxPp.cmi 
-cicNotationPres.cmo: renderingAttrs.cmi mpresentation.cmi boxPp.cmi box.cmi \
+cicNotationPres.cmo: renderingAttrs.cmi mpresentation.cmi box.cmi \
     cicNotationPres.cmi 
-cicNotationPres.cmx: renderingAttrs.cmx mpresentation.cmx boxPp.cmx box.cmx \
+cicNotationPres.cmx: renderingAttrs.cmx mpresentation.cmx box.cmx \
     cicNotationPres.cmi 
 content2pres.cmo: termContentPres.cmi renderingAttrs.cmi mpresentation.cmi \
     cicNotationPres.cmi box.cmi content2pres.cmi 
diff --git a/helm/software/components/content_pres/.depend.opt b/helm/software/components/content_pres/.depend.opt
index 2c5d65140..6dd0e78a1 100644
--- a/helm/software/components/content_pres/.depend.opt
+++ b/helm/software/components/content_pres/.depend.opt
@@ -1,5 +1,6 @@
-cicNotationPres.cmi: mpresentation.cmi box.cmi 
+termContentPres.cmi: cicNotationParser.cmi 
 boxPp.cmi: mpresentation.cmi cicNotationPres.cmi box.cmi 
+cicNotationPres.cmi: mpresentation.cmi box.cmi 
 content2pres.cmi: cicNotationPres.cmi 
 sequent2pres.cmi: cicNotationPres.cmi 
 renderingAttrs.cmo: renderingAttrs.cmi 
@@ -15,17 +16,17 @@ box.cmx: renderingAttrs.cmx box.cmi
 content2presMatcher.cmo: content2presMatcher.cmi 
 content2presMatcher.cmx: content2presMatcher.cmi 
 termContentPres.cmo: renderingAttrs.cmi content2presMatcher.cmi \
-    termContentPres.cmi 
+    cicNotationParser.cmi termContentPres.cmi 
 termContentPres.cmx: renderingAttrs.cmx content2presMatcher.cmx \
-    termContentPres.cmi 
-cicNotationPres.cmo: renderingAttrs.cmi mpresentation.cmi box.cmi \
-    cicNotationPres.cmi 
-cicNotationPres.cmx: renderingAttrs.cmx mpresentation.cmx box.cmx \
-    cicNotationPres.cmi 
+    cicNotationParser.cmx termContentPres.cmi 
 boxPp.cmo: renderingAttrs.cmi mpresentation.cmi cicNotationPres.cmi box.cmi \
     boxPp.cmi 
 boxPp.cmx: renderingAttrs.cmx mpresentation.cmx cicNotationPres.cmx box.cmx \
     boxPp.cmi 
+cicNotationPres.cmo: renderingAttrs.cmi mpresentation.cmi box.cmi \
+    cicNotationPres.cmi 
+cicNotationPres.cmx: renderingAttrs.cmx mpresentation.cmx box.cmx \
+    cicNotationPres.cmi 
 content2pres.cmo: termContentPres.cmi renderingAttrs.cmi mpresentation.cmi \
     cicNotationPres.cmi box.cmi content2pres.cmi 
 content2pres.cmx: termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \
diff --git a/helm/software/components/tactics/.depend b/helm/software/components/tactics/.depend
index 579ab17cc..94235e520 100644
--- a/helm/software/components/tactics/.depend
+++ b/helm/software/components/tactics/.depend
@@ -30,8 +30,8 @@ setoids.cmi: proofEngineTypes.cmi
 fourierR.cmi: proofEngineTypes.cmi 
 fwdSimplTactic.cmi: proofEngineTypes.cmi 
 statefulProofEngine.cmi: proofEngineTypes.cmi 
-tactics.cmi: universe.cmi tacticals.cmi proofEngineTypes.cmi 
-declarative.cmi: universe.cmi proofEngineTypes.cmi 
+tactics.cmi: universe.cmi tacticals.cmi proofEngineTypes.cmi auto.cmi 
+declarative.cmi: universe.cmi proofEngineTypes.cmi auto.cmi 
 proofEngineTypes.cmo: proofEngineTypes.cmi 
 proofEngineTypes.cmx: proofEngineTypes.cmi 
 proofEngineHelpers.cmo: proofEngineTypes.cmi proofEngineHelpers.cmi 
@@ -53,9 +53,11 @@ proofEngineStructuralRules.cmo: proofEngineTypes.cmi \
 proofEngineStructuralRules.cmx: proofEngineTypes.cmx \
     proofEngineStructuralRules.cmi 
 primitiveTactics.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \
-    proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi 
+    proofEngineStructuralRules.cmi proofEngineReduction.cmi \
+    proofEngineHelpers.cmi primitiveTactics.cmi 
 primitiveTactics.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \
-    proofEngineReduction.cmx proofEngineHelpers.cmx primitiveTactics.cmi 
+    proofEngineStructuralRules.cmx proofEngineReduction.cmx \
+    proofEngineHelpers.cmx primitiveTactics.cmi 
 hashtbl_equiv.cmo: hashtbl_equiv.cmi 
 hashtbl_equiv.cmx: hashtbl_equiv.cmi 
 metadataQuery.cmo: proofEngineTypes.cmi primitiveTactics.cmi \
@@ -104,16 +106,14 @@ paramodulation/saturation.cmx: paramodulation/utils.cmx \
     paramodulation/subst.cmx proofEngineTypes.cmx proofEngineHelpers.cmx \
     paramodulation/indexing.cmx paramodulation/founif.cmx \
     paramodulation/equality.cmx paramodulation/saturation.cmi 
-variousTactics.cmo: tacticals.cmi proofEngineTypes.cmi \
-    proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \
+variousTactics.cmo: proofEngineTypes.cmi primitiveTactics.cmi \
     variousTactics.cmi 
-variousTactics.cmx: tacticals.cmx proofEngineTypes.cmx \
-    proofEngineReduction.cmx proofEngineHelpers.cmx primitiveTactics.cmx \
+variousTactics.cmx: proofEngineTypes.cmx primitiveTactics.cmx \
     variousTactics.cmi 
-compose.cmo: variousTactics.cmi proofEngineTypes.cmi primitiveTactics.cmi \
-    closeCoercionGraph.cmi compose.cmi 
-compose.cmx: variousTactics.cmx proofEngineTypes.cmx primitiveTactics.cmx \
-    closeCoercionGraph.cmx compose.cmi 
+compose.cmo: proofEngineTypes.cmi primitiveTactics.cmi closeCoercionGraph.cmi \
+    compose.cmi 
+compose.cmx: proofEngineTypes.cmx primitiveTactics.cmx closeCoercionGraph.cmx \
+    compose.cmi 
 introductionTactics.cmo: proofEngineTypes.cmi primitiveTactics.cmi \
     introductionTactics.cmi 
 introductionTactics.cmx: proofEngineTypes.cmx primitiveTactics.cmx \
@@ -136,16 +136,16 @@ equalityTactics.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \
     proofEngineStructuralRules.cmx proofEngineReduction.cmx \
     proofEngineHelpers.cmx primitiveTactics.cmx introductionTactics.cmx \
     equalityTactics.cmi 
-auto.cmo: paramodulation/utils.cmi universe.cmi paramodulation/subst.cmi \
-    paramodulation/saturation.cmi proofEngineTypes.cmi \
-    proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \
-    metadataQuery.cmi paramodulation/indexing.cmi equalityTactics.cmi \
-    paramodulation/equality.cmi autoTypes.cmi autoCache.cmi auto.cmi 
-auto.cmx: paramodulation/utils.cmx universe.cmx paramodulation/subst.cmx \
-    paramodulation/saturation.cmx proofEngineTypes.cmx \
-    proofEngineReduction.cmx proofEngineHelpers.cmx primitiveTactics.cmx \
-    metadataQuery.cmx paramodulation/indexing.cmx equalityTactics.cmx \
-    paramodulation/equality.cmx autoTypes.cmx autoCache.cmx auto.cmi 
+auto.cmo: paramodulation/utils.cmi universe.cmi paramodulation/saturation.cmi \
+    proofEngineTypes.cmi proofEngineReduction.cmi proofEngineHelpers.cmi \
+    primitiveTactics.cmi metadataQuery.cmi paramodulation/indexing.cmi \
+    equalityTactics.cmi paramodulation/equality.cmi autoTypes.cmi \
+    autoCache.cmi auto.cmi 
+auto.cmx: paramodulation/utils.cmx universe.cmx paramodulation/saturation.cmx \
+    proofEngineTypes.cmx proofEngineReduction.cmx proofEngineHelpers.cmx \
+    primitiveTactics.cmx metadataQuery.cmx paramodulation/indexing.cmx \
+    equalityTactics.cmx paramodulation/equality.cmx autoTypes.cmx \
+    autoCache.cmx auto.cmi 
 destructTactic.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \
     proofEngineStructuralRules.cmi proofEngineHelpers.cmi \
     primitiveTactics.cmi introductionTactics.cmi equalityTactics.cmi \
@@ -204,7 +204,7 @@ tactics.cmx: variousTactics.cmx tacticals.cmx setoids.cmx ring.cmx \
     fwdSimplTactic.cmx fourierR.cmx equalityTactics.cmx \
     eliminationTactics.cmx destructTactic.cmx compose.cmx \
     closeCoercionGraph.cmx auto.cmx tactics.cmi 
-declarative.cmo: universe.cmi tactics.cmi tacticals.cmi proofEngineTypes.cmi \
+declarative.cmo: tactics.cmi tacticals.cmi proofEngineTypes.cmi auto.cmi \
     declarative.cmi 
-declarative.cmx: universe.cmx tactics.cmx tacticals.cmx proofEngineTypes.cmx \
+declarative.cmx: tactics.cmx tacticals.cmx proofEngineTypes.cmx auto.cmx \
     declarative.cmi 
diff --git a/helm/software/components/tactics/.depend.opt b/helm/software/components/tactics/.depend.opt
index 579ab17cc..94235e520 100644
--- a/helm/software/components/tactics/.depend.opt
+++ b/helm/software/components/tactics/.depend.opt
@@ -30,8 +30,8 @@ setoids.cmi: proofEngineTypes.cmi
 fourierR.cmi: proofEngineTypes.cmi 
 fwdSimplTactic.cmi: proofEngineTypes.cmi 
 statefulProofEngine.cmi: proofEngineTypes.cmi 
-tactics.cmi: universe.cmi tacticals.cmi proofEngineTypes.cmi 
-declarative.cmi: universe.cmi proofEngineTypes.cmi 
+tactics.cmi: universe.cmi tacticals.cmi proofEngineTypes.cmi auto.cmi 
+declarative.cmi: universe.cmi proofEngineTypes.cmi auto.cmi 
 proofEngineTypes.cmo: proofEngineTypes.cmi 
 proofEngineTypes.cmx: proofEngineTypes.cmi 
 proofEngineHelpers.cmo: proofEngineTypes.cmi proofEngineHelpers.cmi 
@@ -53,9 +53,11 @@ proofEngineStructuralRules.cmo: proofEngineTypes.cmi \
 proofEngineStructuralRules.cmx: proofEngineTypes.cmx \
     proofEngineStructuralRules.cmi 
 primitiveTactics.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \
-    proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi 
+    proofEngineStructuralRules.cmi proofEngineReduction.cmi \
+    proofEngineHelpers.cmi primitiveTactics.cmi 
 primitiveTactics.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \
-    proofEngineReduction.cmx proofEngineHelpers.cmx primitiveTactics.cmi 
+    proofEngineStructuralRules.cmx proofEngineReduction.cmx \
+    proofEngineHelpers.cmx primitiveTactics.cmi 
 hashtbl_equiv.cmo: hashtbl_equiv.cmi 
 hashtbl_equiv.cmx: hashtbl_equiv.cmi 
 metadataQuery.cmo: proofEngineTypes.cmi primitiveTactics.cmi \
@@ -104,16 +106,14 @@ paramodulation/saturation.cmx: paramodulation/utils.cmx \
     paramodulation/subst.cmx proofEngineTypes.cmx proofEngineHelpers.cmx \
     paramodulation/indexing.cmx paramodulation/founif.cmx \
     paramodulation/equality.cmx paramodulation/saturation.cmi 
-variousTactics.cmo: tacticals.cmi proofEngineTypes.cmi \
-    proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \
+variousTactics.cmo: proofEngineTypes.cmi primitiveTactics.cmi \
     variousTactics.cmi 
-variousTactics.cmx: tacticals.cmx proofEngineTypes.cmx \
-    proofEngineReduction.cmx proofEngineHelpers.cmx primitiveTactics.cmx \
+variousTactics.cmx: proofEngineTypes.cmx primitiveTactics.cmx \
     variousTactics.cmi 
-compose.cmo: variousTactics.cmi proofEngineTypes.cmi primitiveTactics.cmi \
-    closeCoercionGraph.cmi compose.cmi 
-compose.cmx: variousTactics.cmx proofEngineTypes.cmx primitiveTactics.cmx \
-    closeCoercionGraph.cmx compose.cmi 
+compose.cmo: proofEngineTypes.cmi primitiveTactics.cmi closeCoercionGraph.cmi \
+    compose.cmi 
+compose.cmx: proofEngineTypes.cmx primitiveTactics.cmx closeCoercionGraph.cmx \
+    compose.cmi 
 introductionTactics.cmo: proofEngineTypes.cmi primitiveTactics.cmi \
     introductionTactics.cmi 
 introductionTactics.cmx: proofEngineTypes.cmx primitiveTactics.cmx \
@@ -136,16 +136,16 @@ equalityTactics.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \
     proofEngineStructuralRules.cmx proofEngineReduction.cmx \
     proofEngineHelpers.cmx primitiveTactics.cmx introductionTactics.cmx \
     equalityTactics.cmi 
-auto.cmo: paramodulation/utils.cmi universe.cmi paramodulation/subst.cmi \
-    paramodulation/saturation.cmi proofEngineTypes.cmi \
-    proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \
-    metadataQuery.cmi paramodulation/indexing.cmi equalityTactics.cmi \
-    paramodulation/equality.cmi autoTypes.cmi autoCache.cmi auto.cmi 
-auto.cmx: paramodulation/utils.cmx universe.cmx paramodulation/subst.cmx \
-    paramodulation/saturation.cmx proofEngineTypes.cmx \
-    proofEngineReduction.cmx proofEngineHelpers.cmx primitiveTactics.cmx \
-    metadataQuery.cmx paramodulation/indexing.cmx equalityTactics.cmx \
-    paramodulation/equality.cmx autoTypes.cmx autoCache.cmx auto.cmi 
+auto.cmo: paramodulation/utils.cmi universe.cmi paramodulation/saturation.cmi \
+    proofEngineTypes.cmi proofEngineReduction.cmi proofEngineHelpers.cmi \
+    primitiveTactics.cmi metadataQuery.cmi paramodulation/indexing.cmi \
+    equalityTactics.cmi paramodulation/equality.cmi autoTypes.cmi \
+    autoCache.cmi auto.cmi 
+auto.cmx: paramodulation/utils.cmx universe.cmx paramodulation/saturation.cmx \
+    proofEngineTypes.cmx proofEngineReduction.cmx proofEngineHelpers.cmx \
+    primitiveTactics.cmx metadataQuery.cmx paramodulation/indexing.cmx \
+    equalityTactics.cmx paramodulation/equality.cmx autoTypes.cmx \
+    autoCache.cmx auto.cmi 
 destructTactic.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \
     proofEngineStructuralRules.cmi proofEngineHelpers.cmi \
     primitiveTactics.cmi introductionTactics.cmi equalityTactics.cmi \
@@ -204,7 +204,7 @@ tactics.cmx: variousTactics.cmx tacticals.cmx setoids.cmx ring.cmx \
     fwdSimplTactic.cmx fourierR.cmx equalityTactics.cmx \
     eliminationTactics.cmx destructTactic.cmx compose.cmx \
     closeCoercionGraph.cmx auto.cmx tactics.cmi 
-declarative.cmo: universe.cmi tactics.cmi tacticals.cmi proofEngineTypes.cmi \
+declarative.cmo: tactics.cmi tacticals.cmi proofEngineTypes.cmi auto.cmi \
     declarative.cmi 
-declarative.cmx: universe.cmx tactics.cmx tacticals.cmx proofEngineTypes.cmx \
+declarative.cmx: tactics.cmx tacticals.cmx proofEngineTypes.cmx auto.cmx \
     declarative.cmi 
-- 
2.39.2