From 9db61bd8a7975fe37dda80e0fb7cf5809b69f987 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sat, 16 Sep 2023 16:48:11 +0200
Subject: [PATCH] adding parameters to auto to tune some builtin constants

+ a not working "Filename.chop_extension" removed. It does not understand our uri fragments
+ the "debug" flag enables auto debug_print that produces stack overflow sometimes :(
---
 .gitignore                                   |   2 +
 components/grafite_parser/grafiteParser.ml   | 150 +--
 components/ng_kernel/nUri.ml                 |   2 +-
 components/ng_paramodulation/nCicParamod.ml  | 105 ++-
 components/ng_paramodulation/nCicParamod.mli |  43 +-
 components/ng_paramodulation/paramod.ml      | 269 +++---
 components/ng_paramodulation/paramod.mli     |   2 +
 components/ng_paramodulation/pp.ml           |   2 +-
 components/ng_tactics/nnAuto.ml              | 902 ++++++++++---------
 9 files changed, 756 insertions(+), 721 deletions(-)

diff --git a/.gitignore b/.gitignore
index 884112d77..200dc04ce 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1,5 @@
+*.exe
+_build
 matita/broken_contribs/lambdadelta/bin/*/_build
 matita/broken_contribs/lambdadelta/.depend
 matita/broken_contribs/lambdadelta/bin/recomm/srcs
diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 26ec12af2..6656e6bde 100644
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -1,14 +1,14 @@
 (* Copyright (C) 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
@@ -18,7 +18,7 @@
  * 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://helm.cs.unibo.it/
  *)
@@ -36,10 +36,10 @@ let exc_located_wrapper f =
   | Ploc.Exc (floc, Stream.Error msg) ->
       raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
   | Ploc.Exc (floc, HExtlib.Localized(_,exn)) ->
-      raise (HExtlib.Localized 
+      raise (HExtlib.Localized
         (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
   | Ploc.Exc (floc, exn) ->
-      raise (HExtlib.Localized 
+      raise (HExtlib.Localized
         (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
 
 type parsable = Grammar.parsable * Sedlexing.lexbuf
@@ -57,12 +57,12 @@ let strm_of_parsable (_,buf) = buf
 let add_raw_attribute ~text t = N.AttributedTerm (`Raw text, t)
 
 let default_associativity = Gramext.NonA
-        
-let mk_rec_corec src flavour ind_kind defs loc = 
+
+let mk_rec_corec src flavour ind_kind defs loc =
  let attrs = src, flavour, `Regular in
   (loc, N.LetRec (ind_kind, defs, attrs))
 
-let nmk_rec_corec src flavour ind_kind defs loc index = 
+let nmk_rec_corec src flavour ind_kind defs loc index =
  let loc,t = mk_rec_corec src flavour ind_kind defs loc in
   G.NObj (loc,t,index)
 
@@ -70,7 +70,7 @@ let shift_vars binder (vars, ty) bo =
    let map var bo = N.Binder (binder, (var, ty), bo) in
    List.fold_right map vars bo
 
-let shift_params binder params bo = 
+let shift_params binder params bo =
    List.fold_right (shift_vars binder) params bo
 (*
 let nnon_punct_of_punct = function
@@ -146,15 +146,15 @@ EXTEND
          None -> None,[],Some N.UserInput
        | Some ps -> ps]
   ];
-  inverter_param_list: [ 
-    [ params = tactic_term -> 
+  inverter_param_list: [
+    [ params = tactic_term ->
       let deannotate = function
         | N.AttributedTerm (_,t) | t -> t
       in match deannotate params with
       | N.Implicit _ -> [false]
       | N.UserInput -> [true]
-      | N.Appl l -> 
-         List.map (fun x -> match deannotate x with  
+      | N.Appl l ->
+         List.map (fun x -> match deannotate x with
            | N.Implicit _ -> false
            | N.UserInput -> true
            | _ -> raise (Invalid_argument "malformed target parameter list 1")) l
@@ -181,12 +181,12 @@ EXTEND
         SYMBOL <:unicode<vdash>>;
         concl = tactic_term -> (List.rev hyps,concl) ] ->
          G.NTactic(loc,[G.NAssert (loc, seqs)])
-    | SYMBOL "/"; num = OPT NUMBER ; 
+    | SYMBOL "/"; num = OPT NUMBER ;
        just_and_params = auto_params; SYMBOL "/" ->
        let just,params = just_and_params in
        let depth = match num with Some n -> n | None -> "1" in
        (match just with
-       | None -> 
+       | None ->
 	         G.NTactic(loc,
             [G.NAuto(loc,(None,["depth",depth]@params))])
        | Some (`Univ univ) ->
@@ -197,16 +197,16 @@ EXTEND
              G.NAutoInteractive (loc, (None,["depth",depth]@params))))
     | SYMBOL "#"; SYMBOL "#" -> G.NMacro (loc, G.NIntroGuess loc)
     | IDENT "check"; t = tactic_term -> G.NMacro(loc,G.NCheck (loc,t))
-    | IDENT "screenshot"; fname = QSTRING -> 
+    | IDENT "screenshot"; fname = QSTRING ->
         G.NMacro(loc,G.Screenshot (loc, fname))
     | IDENT "cases"; what = tactic_term ; where = pattern_spec ->
         G.NTactic(loc,[G.NCases (loc, what, where)])
-    | IDENT "change";  "with"; with_what = tactic_term; what = pattern_spec -> 
+    | IDENT "change";  "with"; with_what = tactic_term; what = pattern_spec ->
         G.NTactic(loc,[G.NChange (loc, what, with_what)])
     | SYMBOL "-"; id = IDENT ->
         G.NTactic(loc,[G.NClear (loc, [id])])
-    | PLACEHOLDER; num = OPT NUMBER; 
-	l = OPT [ SYMBOL "{"; l = LIST1 tactic_term; SYMBOL "}" -> l ] -> 
+    | PLACEHOLDER; num = OPT NUMBER;
+	l = OPT [ SYMBOL "{"; l = LIST1 tactic_term; SYMBOL "}" -> l ] ->
         G.NTactic(loc,[G.NConstructor (loc, (match num with None -> None | Some x -> Some (int_of_string x)),match l with None -> [] | Some l -> l)])
     | IDENT "cut"; t = tactic_term -> G.NTactic(loc,[G.NCut (loc, t)])
     | IDENT "destruct"; just = OPT [ dom = ident_list1 -> dom ];
@@ -227,15 +227,15 @@ EXTEND
         G.NTactic(loc,[G.NReduce (loc, kind, p)])
     | dir = direction; what = tactic_term ; where = pattern_spec ->	
         G.NTactic(loc,[G.NRewrite (loc, dir, what, where)])
-    | IDENT "try"; tac = SELF -> 
+    | IDENT "try"; tac = SELF ->
         let tac = match tac with G.NTactic(_,[t]) -> t | _ -> assert false in
         G.NTactic(loc,[ G.NTry (loc,tac)])
-    | IDENT "repeat"; tac = SELF -> 
+    | IDENT "repeat"; tac = SELF ->
         let tac = match tac with G.NTactic(_,[t]) -> t | _ -> assert false in
         G.NTactic(loc,[ G.NRepeat (loc,tac)])
-    | LPAREN; l = LIST1 SELF; RPAREN -> 
-        let l = 
-          List.flatten 
+    | LPAREN; l = LIST1 SELF; RPAREN ->
+        let l =
+          List.flatten
             (List.map (function G.NTactic(_,t) -> t | _ -> assert false) l) in
         G.NTactic(loc,[G.NBlock (loc,l)])
     | IDENT "assumption" -> G.NTactic(loc,[ G.NAssumption loc])
@@ -249,10 +249,10 @@ EXTEND
         G.NTactic(loc,[G.NLetIn (loc,(None,[],Some N.UserInput),t,name)])
     | just =
        [ IDENT "using"; t=tactic_term -> `Term t
-       | params = auto_params -> 
+       | params = auto_params ->
             let just,params = params in
             `Auto
-            (match just with 
+            (match just with
              | None -> (None,params)
              | Some (`Univ univ) -> (Some univ,params)
              (* `Trace behaves exaclty like None for the moment being *)
@@ -273,9 +273,9 @@ EXTEND
         G.NTactic (loc,[G.We_need_to_prove (loc, t, id)])
     | IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t = tactic_term -> G.NTactic(loc,[G.BetaRewritingStep (loc,t)])
     | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t1=tactic_term -> G.NTactic (loc,[G.Thesisbecomes(loc,t1)])
-    | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->  
+    | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
         G.NTactic (loc,[G.We_proceed_by_cases_on (loc, t, t1)])
-    | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->  
+    | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
         G.NTactic (loc,[G.We_proceed_by_induction_on (loc, t, t1)])
     | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
         G.NTactic (loc,[G.Byinduction(loc, t, id)])
@@ -285,7 +285,7 @@ EXTEND
     | IDENT "print_stack" -> G.NTactic (loc,[G.PrintStack loc])
     (* DO NOT FACTORIZE with the two following, camlp5 sucks*)
 (*
-    | IDENT "conclude";  
+    | IDENT "conclude";
       termine = tactic_term;
       SYMBOL "=" ;
       t1=tactic_term ;
@@ -293,10 +293,10 @@ EXTEND
        [ IDENT "using"; t=tactic_term -> `Term t
        | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
        | IDENT "proof" -> `Proof
-       | params = auto_params -> `Auto 
+       | params = auto_params -> `Auto
             (
                let just,params = params in
-               match just with 
+               match just with
                  | None -> (None,params)
                  | Some (`Univ univ) -> (Some univ,params)
                  (* `Trace behaves exaclty like None for the moment being *)
@@ -313,10 +313,10 @@ EXTEND
        [ IDENT "using"; t=tactic_term -> `Term t
        | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
        | IDENT "proof" -> `Proof
-       | params = auto_params -> `Auto 
+       | params = auto_params -> `Auto
             (
                let just,params = params in
-               match just with 
+               match just with
                  | None -> (None,params)
                  | Some (`Univ univ) -> (Some univ,params)
                  (* `Trace behaves exaclty like None for the moment being *)
@@ -337,10 +337,10 @@ EXTEND
        [ IDENT "using"; t=tactic_term -> `Term t
        | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
        | IDENT "proof" -> `Proof
-       | params = auto_params -> `Auto 
+       | params = auto_params -> `Auto
             (
                let just,params = params in
-               match just with 
+               match just with
                  | None -> (None,params)
                  | Some (`Univ univ) -> (Some univ,params)
                  (* `Trace behaves exaclty like None for the moment being *)
@@ -358,16 +358,18 @@ EXTEND
    | IDENT "width"
    | IDENT "size"
    | IDENT "nohyps"
-(*   | IDENT "timeout" *)
+   | IDENT "time"
+   | IDENT "debug"
+   | IDENT "steps"
    ]
 ];
   auto_params: [
-    [ params = 
+    [ params =
       LIST0 [
          i = auto_fixed_param -> i,""
        | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
-              string_of_int v | v = IDENT -> v ] -> i,v ]; 
-      just = OPT [ IDENT "by"; by = 
+              string_of_int v | v = IDENT -> v ] -> i,v ];
+      just = OPT [ IDENT "by"; by =
         [ univ = LIST0 tactic_term SEP SYMBOL "," -> `Univ univ
         | SYMBOL "_" -> `Trace ] -> by ] -> just,params
    ]
@@ -377,7 +379,7 @@ EXTEND
     [ WEPROVED; ty = tactic_term ; id = OPT [ LPAREN ; id = IDENT ; RPAREN -> id] -> BYC_weproved (ty,id)
     | "done" -> BYC_done
     | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
-      IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ; 
+      IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
       id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,t2,id2)
     | WEHAVE; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
               BYC_wehaveand (id1,t1,id2,t2)
@@ -454,7 +456,7 @@ EXTEND
     ]
   ];
   inductive_spec: [ [
-    fst_name = IDENT; 
+    fst_name = IDENT;
       params = LIST0 protected_binder_vars;
     SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
     fst_constructors = LIST0 constructor SEP SYMBOL "|";
@@ -475,23 +477,23 @@ EXTEND
         let ind_types = fst_ind_type :: tl_ind_types in
         (params, ind_types)
     ] ];
-    
+
     record_spec: [ [
-      name = IDENT; 
+      name = IDENT;
       params = LIST0 protected_binder_vars;
-       SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ; 
-       fields = LIST0 [ 
+       SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
+       fields = LIST0 [
          name = IDENT ;
          params = LIST0 protected_binder_vars; (* FG: params added *)
-         coercion = [ 
-             SYMBOL ":" -> false,0 
+         coercion = [
+             SYMBOL ":" -> false,0
            | SYMBOL ":"; SYMBOL ">" -> true,0
            | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
-         ]; 
-         ty = term -> 
+         ];
+         ty = term ->
            let b,n = coercion in
-           (name, shift_params `Forall params ty, b, n) 
-       ] SEP SYMBOL ";"; SYMBOL "}" -> 
+           (name, shift_params `Forall params ty, b, n)
+       ] SEP SYMBOL ";"; SYMBOL "}" ->
         let params =
           List.fold_right
             (fun (names, typ) acc ->
@@ -555,7 +557,7 @@ EXTEND
       [ dir = OPT direction; s = QSTRING;
         assoc = OPT associativity; prec = precedence;
         IDENT "for";
-        p2 = 
+        p2 =
           [ blob = UNPARSED_AST ->
               add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
                 (CicNotationParser.parse_level2_ast lstatus
@@ -594,13 +596,13 @@ EXTEND
           (s, args, t)
       ]
     ];
-    
+
     include_command: [ [
-        IDENT "include" ; path = QSTRING -> 
+        IDENT "include" ; path = QSTRING ->
           loc,path,G.WithPreferences
-      | IDENT "include" ; IDENT "alias"; path = QSTRING -> 
+      | IDENT "include" ; IDENT "alias"; path = QSTRING ->
           loc,path,G.OnlyPreferences
-      | IDENT "include'" ; path = QSTRING -> 
+      | IDENT "include'" ; path = QSTRING ->
           loc,path,G.WithoutPreferences
      ]];
 
@@ -630,7 +632,7 @@ EXTEND
       body = term ->
         let body = shift_params `Lambda params body in
         let attrs = src, nflavour, `Regular in
-        G.NObj (loc, 
+        G.NObj (loc,
           N.Theorem(name, N.Implicit `JustOne, Some body, attrs),
           true)
     | src = source; IDENT "axiom"; i = index; name = IDENT;
@@ -651,24 +653,24 @@ EXTEND
     | src = source; IDENT "record" ; (params,name,ty,fields) = record_spec ->
         G.NObj (loc, N.Record (params,name,ty,fields,src),true)
 (* FG: new syntax for inductive/coinductive definitions and statements *)
-    | src = source; IDENT "rec"; nflavour = ntheorem_flavour; defs = let_defs -> 
+    | src = source; IDENT "rec"; nflavour = ntheorem_flavour; defs = let_defs ->
         nmk_rec_corec src nflavour `Inductive defs loc true
     | src = source; IDENT "corec"; nflavour = ntheorem_flavour; defs = let_codefs ->
         nmk_rec_corec src nflavour `CoInductive defs loc true
 (**)
-    | LETCOREC ; defs = let_codefs -> 
+    | LETCOREC ; defs = let_codefs ->
         nmk_rec_corec `Provided `Definition `CoInductive defs loc true
-    | LETREC ; defs = let_defs -> 
+    | LETREC ; defs = let_defs ->
         nmk_rec_corec `Provided `Definition `Inductive defs loc true
     | IDENT "discriminator" ; indty = tactic_term -> G.NDiscriminator (loc,indty)
     | IDENT "inverter"; name = IDENT; IDENT "for" ; indty = tactic_term ;
-      paramspec = OPT inverter_param_list ; 
-      outsort = OPT [ SYMBOL ":" ; outsort = term -> outsort ] -> 
+      paramspec = OPT inverter_param_list ;
+      outsort = OPT [ SYMBOL ":" ; outsort = term -> outsort ] ->
         G.NInverter (loc,name,indty,paramspec,outsort)
-    | IDENT "universe"; cyclic = OPT [ IDENT "cyclic" -> () ] ; IDENT "constraint"; u1 = tactic_term; 
+    | IDENT "universe"; cyclic = OPT [ IDENT "cyclic" -> () ] ; IDENT "constraint"; u1 = tactic_term;
         SYMBOL <:unicode<lt>> ; u2 = tactic_term ->
         let acyclic = match cyclic with None -> true | Some () -> false in
-        let urify = function 
+        let urify = function
           | NotationPt.AttributedTerm (_, NotationPt.Sort (`NType i)) ->
               NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
           | _ -> raise (Failure "only a Type[…] sort can be constrained")
@@ -680,13 +682,13 @@ EXTEND
         G.UnificationHint (loc, t, n)
     | IDENT "coercion"; name = IDENT;
         compose = OPT [ IDENT "nocomposites" -> () ];
-        spec = OPT [ SYMBOL ":"; ty = term; 
-        SYMBOL <:unicode<def>>; t = term; "on"; 
+        spec = OPT [ SYMBOL ":"; ty = term;
+        SYMBOL <:unicode<def>>; t = term; "on";
         id = [ IDENT | PIDENT ]; SYMBOL ":"; source = term;
         "to"; target = term -> t,ty,(id,source),target ] ->
           let compose = compose = None in
           G.NCoercion(loc,name,compose,spec)
-    | IDENT "copy" ; s = IDENT; IDENT "from"; u = URI; "with"; 
+    | IDENT "copy" ; s = IDENT; IDENT "from"; u = URI; "with";
       m = LIST0 [ u1 = URI; SYMBOL <:unicode<mapsto>>; u2 = URI -> u1,u2 ] ->
         G.NCopy (loc,s,NUri.uri_of_string u,
           List.map (fun a,b -> NUri.uri_of_string a, NUri.uri_of_string b) m)
@@ -707,18 +709,18 @@ EXTEND
     | tac = nnon_punctuation_tactical(*; punct = npunctuation_tactical*) ->
           G.NTactic (loc, [tac])
     | tac = ntactic (*; punct = npunctuation_tactical*) ->
-         tac 
+         tac
 (*
-    | tac = nnon_punctuation_tactical; 
+    | tac = nnon_punctuation_tactical;
         punct = npunctuation_tactical ->
           G.NTactic (loc, [tac; punct])
 *)
     ]
   ];
   comment: [
-    [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT -> 
+    [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
        G.Code (loc, ex)
-    | str = NOTE -> 
+    | str = NOTE ->
        G.Note (loc, str)
     ]
   ];
@@ -757,7 +759,7 @@ class virtual status =
    db <- Some (mk_parser (Grammar.Entry.create grammar "statement") self)
  end
 
-let extend status l1 action = 
+let extend status l1 action =
   let status = CicNotationParser.extend status l1 action in
   let grammar = CicNotationParser.level2_ast_grammar status in
   status#set_parser_db
@@ -765,7 +767,7 @@ let extend status l1 action =
 ;;
 
 
-let parse_statement status = 
+let parse_statement status =
   parse_statement status#parser_db
 
 (* vim:set foldmethod=marker: *)
diff --git a/components/ng_kernel/nUri.ml b/components/ng_kernel/nUri.ml
index ba87b2e28..62403c72e 100644
--- a/components/ng_kernel/nUri.ml
+++ b/components/ng_kernel/nUri.ml
@@ -47,7 +47,7 @@ fun s ->
 ;;
 
 let eq = (==);;
-let compare (n1,_) (n2,_) = n2 - n1;;
+let compare (n1,_) (n2,_) = n2 - n1;; (* we compare by age *)
 let hash (n,_) = n;;
 
 module HT = struct
diff --git a/components/ng_paramodulation/nCicParamod.ml b/components/ng_paramodulation/nCicParamod.ml
index 702cd8c16..912cffd70 100644
--- a/components/ng_paramodulation/nCicParamod.ml
+++ b/components/ng_paramodulation/nCicParamod.ml
@@ -1,12 +1,12 @@
 (*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic        
-    ||A||  Library of Mathematics, developed at the Computer Science     
-    ||T||  Department, University of Bologna, Italy.                     
-    ||I||                                                                
-    ||T||  HELM is free software; you can redistribute it and/or         
-    ||A||  modify it under the terms of the GNU General Public License   
-    \   /  version 2 or (at your option) any later version.      
-     \ /   This software is distributed as is, NO WARRANTY.     
+    ||M||  This file is part of HELM, an Hypertextual, Electronic
+    ||A||  Library of Mathematics, developed at the Computer Science
+    ||T||  Department, University of Bologna, Italy.
+    ||I||
+    ||T||  HELM is free software; you can redistribute it and/or
+    ||A||  modify it under the terms of the GNU General Public License
+    \   /  version 2 or (at your option) any later version.
+     \ /   This software is distributed as is, NO WARRANTY.
       V_______________________________________________________________ *)
 
 (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
@@ -16,12 +16,14 @@ NCicBlob.set_default_eqP()
 NCicProof.set_default_sig()
 ;;
 
+let time = ref 300.0
+
 let noprint _ = ();;
-let print s = prerr_endline (Lazy.force s);; 
-let debug = noprint;; 
+let print s = prerr_endline (Lazy.force s);;
+let debug = noprint;;
 
-module B(C : NCicBlob.NCicContext): Orderings.Blob 
-  with type t = NCic.term and type input = NCic.term 
+module B(C : NCicBlob.NCicContext): Orderings.Blob
+  with type t = NCic.term and type input = NCic.term
   = Orderings.LPO(NCicBlob.NCicBlob(C))
 
 module NCicParamod(C : NCicBlob.NCicContext) = Paramod.Paramod(B(C))
@@ -30,22 +32,22 @@ let readback status ?(demod=false) metasenv subst context (bag,i,fo_subst,l) =
 (*
   List.iter (fun x ->
      print_endline (Pp.pp_unit_clause ~margin:max_int
-     (fst(Terms.M.find x bag)))) l; 
+     (fst(Terms.M.find x bag)))) l;
 *)
   (* let stamp = Unix.gettimeofday () in *)
   let proofterm,prooftype = NCicProof.mk_proof status ~demod bag i fo_subst l in
   (* debug (lazy (Printf.sprintf "Got proof term in %fs"
 		     (Unix.gettimeofday() -. stamp))); *)
 (*
-  let metasenv, proofterm = 
+  let metasenv, proofterm =
     let rec aux k metasenv = function
       | NCic.Meta _ as t -> metasenv, t
-      | NCic.Implicit _ -> 
+      | NCic.Implicit _ ->
           let metasenv, i, _, _ =
-            NCicMetaSubst.mk_meta metasenv context `IsTerm 
+            NCicMetaSubst.mk_meta metasenv context `IsTerm
           in
             metasenv, NCic.Meta (i,(k,NCic.Irl (List.length context)))
-      | t -> NCicUntrusted.map_term_fold_a 
+      | t -> NCicUntrusted.map_term_fold_a
           (fun _ k -> k+1) k aux metasenv t
     in
       aux 0 metasenv proofterm
@@ -53,9 +55,9 @@ let readback status ?(demod=false) metasenv subst context (bag,i,fo_subst,l) =
   debug (lazy (status#ppterm ~metasenv ~subst ~context proofterm));
 (*
   let stamp = Unix.gettimeofday () in
-  let metasenv, subst, proofterm, _prooftype = 
-    NCicRefiner.typeof 
-      (status#set_coerc_db NCicCoercion.empty_db) 
+  let metasenv, subst, proofterm, _prooftype =
+    NCicRefiner.typeof
+      (status#set_coerc_db NCicCoercion.empty_db)
       metasenv subst context proofterm None
   in
     print (lazy (Printf.sprintf "Refined in %fs"
@@ -65,32 +67,32 @@ let readback status ?(demod=false) metasenv subst context (bag,i,fo_subst,l) =
 
 let nparamod status metasenv subst context t table =
   let module C =
-    struct 
+    struct
       let metasenv = metasenv
       let subst = subst
-      let context = context 
-    end 
+      let context = context
+    end
   in
   (*let module B = B(C) in*)
   let module P = NCicParamod(C) in
   (*let module Pp = Pp.Pp(B) in*)
   let bag, maxvar = Terms.empty_bag, 0 in
-  let (bag,maxvar), goals = 
+  let (bag,maxvar), goals =
     HExtlib.list_mapi_acc (fun x _ a -> P.mk_goal a x) (bag,maxvar) [t]
   in
-  let (bag,maxvar), passives = 
+  let (bag,maxvar), passives =
     HExtlib.list_mapi_acc (fun x _ a -> P.mk_passive a x) (bag,maxvar) table
   in
-  match 
-    P.paramod ~useage:true ~max_steps:max_int ~timeout:(Unix.gettimeofday () +. 300.0) 
-      ~g_passives:goals ~passives (bag,maxvar) 
-  with 
+  match
+    P.paramod ~useage:true ~max_steps:max_int ~timeout:(Unix.gettimeofday () +. !time)
+      ~g_passives:goals ~passives (bag,maxvar)
+  with
   | P.Error _ | P.GaveUp | P.Timeout _ -> []
-  | P.Unsatisfiable solutions -> 
+  | P.Unsatisfiable solutions ->
       List.map (readback status metasenv subst context) solutions
 ;;
-  
-module EmptyC = 
+
+module EmptyC =
   struct
     let metasenv = []
     let subst = []
@@ -103,7 +105,17 @@ module P = NCicParamod(EmptyC)
 type state = P.state
 let empty_state = P.empty_state
 
-exception NotEmbeddable 
+let pp_state s =
+  let module Pp = Pp.Pp(CB) in
+  let str () =
+    let bag, _ = P.bag_of_state s in
+    Pp.pp_bag bag
+  in
+  debug (lazy "EQ CACHE BEGINS");
+  debug (lazy (str ()));
+  debug (lazy "EQ CACHE ENDS")
+
+exception NotEmbeddable
 
 let not_embeddable status subst context ty =
   let rec aux = function
@@ -112,12 +124,12 @@ let not_embeddable status subst context ty =
     | NCic.Rel _
     | NCic.Sort _ -> ()
     | NCic.Appl l -> List.iter aux l
-    | t -> 
+    | t ->
         (* cannot embed a blob term containing metas *)
         if (NCicUntrusted.metas_of_term status subst context t = [])
-        then () 
+        then ()
         else raise NotEmbeddable
-  in 
+  in
   try aux ty; noprint (lazy ("Embeddable")); false
   with NotEmbeddable -> debug (lazy ("Not embeddable")); true
 ;;
@@ -130,12 +142,12 @@ let tooflex (_,l,_,_) =
        | _, (Terms.Var _ | Terms.Node (Terms.Var _::_)),(Terms.Incomparable | Terms.Invertible) -> true
        | _ -> false)
     | _ -> false
-;;  
+;;
 
 let forward_infer_step0 status metasenv subst context s t ty =
   let bag = P.bag_of_state s in
   let not_embed =
-    let sty,_,_ = 
+    let sty,_,_ =
       NCicMetaSubst.saturate status ~delta:0  metasenv subst context ty 0 in
       not_embeddable status subst context sty in
   if not_embed then (debug (lazy "theorem not embeddable"); s,None)
@@ -171,7 +183,7 @@ let demod status metasenv subst context s goal =
   (* let stamp = Unix.gettimeofday () in *)
   match P.demod s goal with
     | P.Error _ | P.GaveUp | P.Timeout _ -> []
-    | P.Unsatisfiable solutions -> 
+    | P.Unsatisfiable solutions ->
       (* print (lazy (Printf.sprintf "Got solutions in %fs"
 		     (Unix.gettimeofday() -. stamp))); *)
       List.map (readback ~demod:true status metasenv subst context) solutions
@@ -180,30 +192,31 @@ let demod status metasenv subst context s goal =
 let paramod status metasenv subst context s goal =
   if not_embeddable status subst context (snd goal) then [] else
   (* let stamp = Unix.gettimeofday () in *)
-  match P.nparamod ~useage:true ~max_steps:max_int 
-    ~timeout:(Unix.gettimeofday () +. 300.0) s goal with
+  match P.nparamod ~useage:true ~max_steps:max_int
+    ~timeout:(Unix.gettimeofday () +. !time) s goal with
   | P.Error _ | P.GaveUp | P.Timeout _ -> []
-  | P.Unsatisfiable solutions -> 
+  | P.Unsatisfiable solutions ->
       (* print (lazy (Printf.sprintf "Got solutions in %fs"
 		     (Unix.gettimeofday() -. stamp))); *)
       List.map (readback status metasenv subst context) solutions
 ;;
 
 let fast_eq_check status metasenv subst context s goal =
+  pp_state s;
   if not_embeddable status subst context (snd goal) then [] else
   (* let stamp = Unix.gettimeofday () in *)
   match P.fast_eq_check s goal with
   | P.Error _ | P.GaveUp | P.Timeout _ -> []
-  | P.Unsatisfiable solutions -> 
+  | P.Unsatisfiable solutions ->
       (* print (lazy (Printf.sprintf "Got solutions in %fs"
 		     (Unix.gettimeofday() -. stamp))); *)
       List.map (readback status metasenv subst context) solutions
 ;;
 
 let is_equation status metasenv subst context ty =
-  let hty, _, _ = 
+  let hty, _, _ =
     NCicMetaSubst.saturate status ~delta:0 metasenv subst context
-      ty 0 
+      ty 0
   in match hty with
     | NCic.Appl (eq ::_) when eq = CB.eqP -> true
     | _ -> false
@@ -214,7 +227,7 @@ let demodulate status metasenv subst context s goal =
   (* let stamp = Unix.gettimeofday () in *)
   match P.fast_eq_check s goal with
   | P.Error _ | P.GaveUp | P.Timeout _ -> []
-  | P.Unsatisfiable solutions -> 
+  | P.Unsatisfiable solutions ->
       (* print (lazy (Printf.sprintf "Got solutions in %fs"
 		     (Unix.gettimeofday() -. stamp))); *)
       List.map (readback status metasenv subst context) solutions
diff --git a/components/ng_paramodulation/nCicParamod.mli b/components/ng_paramodulation/nCicParamod.mli
index b4cb209fb..9af1006ad 100644
--- a/components/ng_paramodulation/nCicParamod.mli
+++ b/components/ng_paramodulation/nCicParamod.mli
@@ -1,25 +1,28 @@
 (*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic        
-    ||A||  Library of Mathematics, developed at the Computer Science     
-    ||T||  Department, University of Bologna, Italy.                     
-    ||I||                                                                
-    ||T||  HELM is free software; you can redistribute it and/or         
-    ||A||  modify it under the terms of the GNU General Public License   
-    \   /  version 2 or (at your option) any later version.      
-     \ /   This software is distributed as is, NO WARRANTY.     
+    ||M||  This file is part of HELM, an Hypertextual, Electronic
+    ||A||  Library of Mathematics, developed at the Computer Science
+    ||T||  Department, University of Bologna, Italy.
+    ||I||
+    ||T||  HELM is free software; you can redistribute it and/or
+    ||A||  modify it under the terms of the GNU General Public License
+    \   /  version 2 or (at your option) any later version.
+     \ /   This software is distributed as is, NO WARRANTY.
       V_______________________________________________________________ *)
 
 (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
 
+(* FG: this was 300.0 hard coded *)
+val time: float ref
+
 val nparamod :
   #NCicCoercion.status ->
-  NCic.metasenv -> NCic.substitution -> NCic.context -> 
+  NCic.metasenv -> NCic.substitution -> NCic.context ->
     (NCic.term * NCic.term) -> (NCic.term * NCic.term) list ->
      (NCic.term * NCic.term * NCic.metasenv * NCic.substitution) list
 
-type state 
+type state
 val empty_state: state
-val forward_infer_step: 
+val forward_infer_step:
   #NCic.status -> NCic.metasenv -> NCic.substitution -> NCic.context ->
   state -> NCic.term -> NCic.term -> state
 val index_obj:
@@ -27,21 +30,21 @@ val index_obj:
 val is_equation:
  #NCic.status -> NCic.metasenv -> NCic.substitution -> NCic.context ->
   NCic.term -> bool
-val paramod : 
+val paramod :
   #NCicCoercion.status ->
   NCic.metasenv -> NCic.substitution -> NCic.context ->
-  state -> 
-  (NCic.term * NCic.term) -> 
+  state ->
+  (NCic.term * NCic.term) ->
   (NCic.term * NCic.term * NCic.metasenv * NCic.substitution) list
-val fast_eq_check : 
+val fast_eq_check :
   #NCicCoercion.status ->
   NCic.metasenv -> NCic.substitution -> NCic.context ->
-  state -> 
-  (NCic.term * NCic.term) -> 
+  state ->
+  (NCic.term * NCic.term) ->
   (NCic.term * NCic.term * NCic.metasenv * NCic.substitution) list
-val demod : 
+val demod :
   #NCicCoercion.status ->
   NCic.metasenv -> NCic.substitution -> NCic.context ->
-  state -> 
-  (NCic.term * NCic.term) -> 
+  state ->
+  (NCic.term * NCic.term) ->
   (NCic.term * NCic.term * NCic.metasenv * NCic.substitution) list
diff --git a/components/ng_paramodulation/paramod.ml b/components/ng_paramodulation/paramod.ml
index e38179c77..236251e46 100644
--- a/components/ng_paramodulation/paramod.ml
+++ b/components/ng_paramodulation/paramod.ml
@@ -1,31 +1,33 @@
 (*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic        
-    ||A||  Library of Mathematics, developed at the Computer Science     
-    ||T||  Department, University of Bologna, Italy.                     
-    ||I||                                                                
-    ||T||  HELM is free software; you can redistribute it and/or         
-    ||A||  modify it under the terms of the GNU General Public License   
-    \   /  version 2 or (at your option) any later version.      
-     \ /   This software is distributed as is, NO WARRANTY.     
+    ||M||  This file is part of HELM, an Hypertextual, Electronic
+    ||A||  Library of Mathematics, developed at the Computer Science
+    ||T||  Department, University of Bologna, Italy.
+    ||I||
+    ||T||  HELM is free software; you can redistribute it and/or
+    ||A||  modify it under the terms of the GNU General Public License
+    \   /  version 2 or (at your option) any later version.
+     \ /   This software is distributed as is, NO WARRANTY.
       V_______________________________________________________________ *)
 
 (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
 
-let print s = prerr_endline (Lazy.force s) ;; 
-let noprint _s = ();;  
+let print s = prerr_endline (Lazy.force s) ;;
+let noprint _s = ();;
 let debug = noprint;;
 
+let max_steps = ref 2
+
 let monster = 100;;
-    
+
 module type Paramod =
   sig
     type t
     type input
-    type szsontology = 
-      | Unsatisfiable of 
+    type szsontology =
+      | Unsatisfiable of
 	  (t Terms.bag * int * t Terms.substitution * int list) list
-      | GaveUp 
-      | Error of string 
+      | GaveUp
+      | Error of string
       | Timeout of int * t Terms.bag
     type bag = t Terms.bag * int
     type state
@@ -34,13 +36,13 @@ module type Paramod =
     val replace_bag: state -> bag -> state
     val mk_passive : bag -> input * input -> bag * t Terms.unit_clause
     val mk_goal : bag -> input * input -> bag * t Terms.unit_clause
-    val forward_infer_step : 
+    val forward_infer_step :
       state ->
       t Terms.unit_clause ->
       int ->
       state
-    val goal_narrowing : 
-      int 
+    val goal_narrowing :
+      int
       -> int
       -> float option
       -> state
@@ -49,8 +51,8 @@ module type Paramod =
       useage:bool ->
       max_steps:int ->
       ?timeout:float ->
-      bag -> 
-      g_passives:t Terms.unit_clause list -> 
+      bag ->
+      g_passives:t Terms.unit_clause list ->
       passives:t Terms.unit_clause list -> szsontology
     val demod :
       state -> input* input -> szsontology
@@ -64,11 +66,11 @@ module type Paramod =
   end
 
 module Paramod (B : Orderings.Blob) = struct
-  module Pp = Pp.Pp (B) 
+  module Pp = Pp.Pp (B)
   (*module FU = FoUnif.Founif(B)*)
-  module IDX = Index.Index(B) 
-  module Sup = Superposition.Superposition(B) 
-  module Utils = FoUtils.Utils(B) 
+  module IDX = Index.Index(B)
+  module Sup = Superposition.Superposition(B)
+  module Utils = FoUtils.Utils(B)
   module Order = B
   module WeightOrderedPassives =
       struct
@@ -81,29 +83,29 @@ module Paramod (B : Orderings.Blob) = struct
         type t = B.t Terms.passive_clause
         let compare = Utils.compare_passive_clauses_age
       end
-  
+
   module WeightPassiveSet = Set.Make(WeightOrderedPassives)
   module AgePassiveSet = Set.Make(AgeOrderedPassives)
 
   type t = B.t
   type input = B.input
-  type bag = B.t Terms.bag * int 
-  type szsontology = 
-    | Unsatisfiable of 
+  type bag = B.t Terms.bag * int
+  type szsontology =
+    | Unsatisfiable of
 	(B.t Terms.bag * int * B.t Terms.substitution * int list) list
-    | GaveUp 
-    | Error of string 
+    | GaveUp
+    | Error of string
     | Timeout of int * B.t Terms.bag
   exception Stop of szsontology
-  type state = 
-      t Terms.bag 
+  type state =
+      t Terms.bag
       * int
-      * Index.Index(B).active_set 
-      * (IDX.DT.t * WeightPassiveSet.t * AgePassiveSet.t) 
-      * B.t Terms.unit_clause list 
+      * Index.Index(B).active_set
+      * (IDX.DT.t * WeightPassiveSet.t * AgePassiveSet.t)
+      * B.t Terms.unit_clause list
       * (WeightPassiveSet.t * AgePassiveSet.t)
 
-  let empty_state = 
+  let empty_state =
     Terms.empty_bag,
     0,
     ([],IDX.DT.empty),
@@ -114,7 +116,7 @@ module Paramod (B : Orderings.Blob) = struct
 
   let bag_of_state (bag,n,_,_,_,_) = bag,n
   ;;
-  
+
   let replace_bag (_,_,a,b,c,d) (bag,n) = bag,n,a,b,c,d
   ;;
 
@@ -123,7 +125,7 @@ module Paramod (B : Orderings.Blob) = struct
     let pcl = if no_weight then (0,cl)
     else Utils.mk_passive_clause cl in
     IDX.index_unit_clause passive_t cl,
-    WeightPassiveSet.add pcl passives_w, 
+    WeightPassiveSet.add pcl passives_w,
     AgePassiveSet.add pcl passives_a
   ;;
 
@@ -176,11 +178,11 @@ module Paramod (B : Orderings.Blob) = struct
     end
   ;;
 
-  let passive_set_cardinal (_,passives_w,_) 
+  let passive_set_cardinal (_,passives_w,_)
       = WeightPassiveSet.cardinal passives_w
   ;;
 
-  let g_passive_set_cardinal (passives_w,_) 
+  let g_passive_set_cardinal (passives_w,_)
       = WeightPassiveSet.cardinal passives_w
   ;;
 
@@ -214,19 +216,19 @@ module Paramod (B : Orderings.Blob) = struct
     let bag, c = Terms.add_to_bag c bag in
     (bag, maxvar), c
   ;;
-  
+
   let mk_passive (bag,maxvar) = mk_clause bag maxvar;;
 
   let mk_goal (bag,maxvar) = mk_clause bag maxvar;;
 
-  let initialize_goal (bag,maxvar,actives,passives,_,_) t = 
+  let initialize_goal (bag,maxvar,actives,passives,_,_) t =
     let (bag,maxvar), g = mk_unit_clause bag maxvar t in
     let g_passives = g_passive_empty_set in
     (* if the goal is not an equation we returns an empty
        passive set *)
     let g_passives =
       if Terms.is_eq_clause g then add_passive_goal g_passives g
-      else g_passives 
+      else g_passives
     in
       (bag,maxvar,actives,passives,[],g_passives)
 
@@ -259,8 +261,8 @@ module Paramod (B : Orderings.Blob) = struct
                           g_actives g_passives g_current iterno =
     (* superposition left, simplifications on goals *)
       debug (lazy "infer_left step...");
-      let bag, maxvar, new_goals = 
-        Sup.infer_left bag maxvar g_current actives 
+      let bag, maxvar, new_goals =
+        Sup.infer_left bag maxvar g_current actives
       in
         debug (lazy "Performed infer_left step");
 	let bag = Terms.replace_in_bag (g_current,false,iterno) bag in
@@ -272,19 +274,22 @@ module Paramod (B : Orderings.Blob) = struct
     let actives_l, _ = actives in
     let passive_t,_,_ = passives in
     let wset = IDX.elems passive_t in
-      ("Actives :" ^ (String.concat ";\n" 
+      ("Actives :" ^ (String.concat ";\n"
 	(List.map Pp.pp_unit_clause actives_l)))
-      ^ 
-      ("Passives:" ^(String.concat ";\n" 
+      ^
+      ("Passives:" ^(String.concat ";\n"
         (List.map (fun (_,cl) -> Pp.pp_unit_clause cl)
 	       (IDX.ClauseSet.elements wset))))
   ;;
 
-  let forward_infer_step 
-      ((bag,maxvar,actives,passives,g_actives,g_passives) as s)  
+  let pp_bag_length bag =
+    Printf.eprintf "Bag length: %u\n%!" (fst bag)
+
+  let forward_infer_step
+      ((bag,maxvar,actives,passives,g_actives,g_passives) as s)
       current iterno =
     (* forward step *)
-    
+
     (* e = select P           *
      * e' = demod A e         *
      * A' = demod [e'] A      *
@@ -297,47 +302,49 @@ module Paramod (B : Orderings.Blob) = struct
     debug (lazy("Number of actives : " ^ (string_of_int (List.length (fst actives)))));
     noprint (lazy (pp_clauses actives passives));
     let _ = noprint
-      (lazy 
-	 ("Actives before simplification:" ^ (String.concat ";\n" 
-	    (List.map Pp.pp_unit_clause (fst actives))))) in 
+      (lazy
+	 ("Actives before simplification:" ^ (String.concat ";\n"
+	    (List.map Pp.pp_unit_clause (fst actives))))) in
+(*    pp_bag_length bag; *)
     match Sup.keep_simplified current actives bag maxvar
     with
       | _,None -> debug(lazy("None")); s
       | bag,Some (current,actives) ->
     debug (lazy ("simplified to " ^ (Pp.pp_unit_clause current)));
     let _ = noprint
-      (lazy 
-	 ("Actives after simplification:" ^ (String.concat ";\n" 
-	    (List.map Pp.pp_unit_clause (fst actives))))) in 
-    let bag, maxvar, actives, new_clauses = 
-      Sup.infer_right bag maxvar current actives 
+      (lazy
+	 ("Actives after simplification:" ^ (String.concat ";\n"
+	    (List.map Pp.pp_unit_clause (fst actives))))) in
+    let bag, maxvar, actives, new_clauses =
+      Sup.infer_right bag maxvar current actives
     in
       debug
-	(lazy 
-	 ("New clauses :" ^ (String.concat ";\n" 
-	    (List.map Pp.pp_unit_clause new_clauses)))); 
+	(lazy
+	 ("New clauses :" ^ (String.concat ";\n"
+	    (List.map Pp.pp_unit_clause new_clauses))));
       debug (lazy "Demodulating goals with actives...");
       (* keep goals demodulated w.r.t. actives and check if solved *)
-      let bag, g_actives = 
-        List.fold_left 
-          (fun (bag,acc) c -> 
-             match 
+      let bag, g_actives =
+        List.fold_left
+          (fun (bag,acc) c ->
+             match
                Sup.simplify_goal ~no_demod:false maxvar (snd actives) bag acc c
              with
                | None -> bag, acc
                | Some (bag,c1) -> bag,if c==c1 then c::acc else c::c1::acc)
-          (bag,[]) g_actives 
+          (bag,[]) g_actives
       in
       let ctable = IDX.index_unit_clause IDX.DT.empty current in
-      let bag, maxvar, new_goals = 
-        List.fold_left 
-          (fun (bag,m,acc) g -> 
+      let bag, maxvar, new_goals =
+        List.fold_left
+          (fun (bag,m,acc) g ->
              let bag, m, ng = Sup.infer_left bag m g ([current],ctable) in
-               bag,m,ng@acc) 
-          (bag,maxvar,[]) g_actives 
+               bag,m,ng@acc)
+          (bag,maxvar,[]) g_actives
       in
       let bag = Terms.replace_in_bag (current,false,iterno) bag in
-	(* prerr_endline (Pp.pp_bag bag); *)
+(*      pp_bag_length bag; *)
+(*      prerr_endline (Pp.pp_bag bag); *)
     bag, maxvar, actives,
     add_passive_clauses passives new_clauses, g_actives,
     add_passive_goals g_passives new_goals
@@ -349,7 +356,7 @@ module Paramod (B : Orderings.Blob) = struct
           (List.length g_actives)) ^
        (Printf.sprintf "Number of passive goals : %d\n"
           (g_passive_set_cardinal g_passives)) ^
-       (Printf.sprintf "Number of actives : %d\n" 
+       (Printf.sprintf "Number of actives : %d\n"
 	  (List.length (fst actives))) ^
        (Printf.sprintf "Number of passives : %d\n"
          (passive_set_cardinal passives)))
@@ -358,62 +365,62 @@ module Paramod (B : Orderings.Blob) = struct
 
   (* we just check if any of the active goals is subsumed by a
      passive clause, or if any of the passive goal is subsumed
-     by an active or passive clause *) 
+     by an active or passive clause *)
   let last_chance (bag,maxvar,actives,passives,g_actives,g_passives) =
     debug (lazy("Last chance " ^ string_of_float
 		  (Unix.gettimeofday())));
     let actives_l, active_t = actives in
     let passive_t,_wset,_ = passives in
     let _ = noprint
-      (lazy 
-	 ("Actives :" ^ (String.concat ";\n" 
-	    (List.map Pp.pp_unit_clause actives_l)))) in 
+      (lazy
+	 ("Actives :" ^ (String.concat ";\n"
+	    (List.map Pp.pp_unit_clause actives_l)))) in
     let wset = IDX.elems passive_t in
     let _ = noprint
-      (lazy 
-	 ("Passives:" ^(String.concat ";\n" 
+      (lazy
+	 ("Passives:" ^(String.concat ";\n"
 	    (List.map (fun (_,cl) -> Pp.pp_unit_clause cl)
-	       (IDX.ClauseSet.elements wset))))) in 
-    let g_passives = 
-      WeightPassiveSet.fold 
+	       (IDX.ClauseSet.elements wset))))) in
+    let g_passives =
+      WeightPassiveSet.fold
 	(fun (_,x) acc ->
 	  if List.exists (Sup.are_alpha_eq x) g_actives then acc
           else x::acc)
 	  (fst g_passives) []
-    in 
+    in
       ignore
       (List.iter
-	(fun x -> 
-	    ignore 
+	(fun x ->
+	    ignore
 	     (debug (lazy("ckecking goal vs a: " ^ Pp.pp_unit_clause x));
                Sup.simplify_goal ~no_demod:true maxvar active_t bag [] x))
-       g_passives); 
+       g_passives);
       ignore
       (List.iter
-	 (fun x -> 
-	    ignore 
+	 (fun x ->
+	    ignore
 	      (debug (lazy("ckecking goal vs p: " ^ Pp.pp_unit_clause x));
 	Sup.simplify_goal ~no_demod:true maxvar passive_t bag [] x))
-        (g_actives@g_passives)); 
+        (g_actives@g_passives));
     raise (Stop (Timeout (maxvar,bag)))
 
   let check_timeout = function
     | None -> false
     | Some timeout -> Unix.gettimeofday () > timeout
- 
+
   let rec given_clause ~useage
-    bag maxvar iterno weight_picks max_steps timeout 
-    actives passives g_actives g_passives 
+    bag maxvar iterno weight_picks max_steps timeout
+    actives passives g_actives g_passives
   =
     let iterno = iterno + 1 in
     if iterno = max_steps || check_timeout timeout then
       last_chance (bag,maxvar,actives,passives,g_actives,g_passives)
-    else 
+    else
     let use_age = useage && (weight_picks = (iterno / 6 + 1)) in
     let weight_picks = if use_age then 0 else weight_picks+1
     in
 
-    let rec aux_select bag 
+    let rec aux_select bag
 	(passives:IDX.DT.t * WeightPassiveSet.t * AgePassiveSet.t)
 	g_passives =
       let backward,(weight,current),passives,g_passives =
@@ -429,16 +436,16 @@ module Paramod (B : Orderings.Blob) = struct
 	  let bag = Terms.replace_in_bag (current,false,iterno) bag in
         if backward then
           let _ = debug (lazy("Selected goal : " ^ Pp.pp_unit_clause current)) in
-         match 
-           Sup.simplify_goal 
-             ~no_demod:false maxvar (snd actives) bag g_actives current 
+         match
+           Sup.simplify_goal
+             ~no_demod:false maxvar (snd actives) bag g_actives current
          with
            | None -> aux_select bag passives g_passives
            | Some (bag,g_current) ->
                backward_infer_step bag maxvar actives passives
                  g_actives g_passives g_current iterno
         else
-          let _ = debug (lazy("Selected fact : " ^ Pp.pp_unit_clause current)) 
+          let _ = debug (lazy("Selected fact : " ^ Pp.pp_unit_clause current))
 	  in
             if Sup.orphan_murder bag (fst actives) current then
 	      let _ = debug (lazy "Orphan murdered") in
@@ -447,58 +454,58 @@ module Paramod (B : Orderings.Blob) = struct
             else
 	      let s = bag,maxvar,actives,passives,g_actives,g_passives in
               let s1 = forward_infer_step s current iterno
-	      in 
-		if s == s1 then aux_select bag passives g_passives  
+	      in
+		if s == s1 then aux_select bag passives g_passives
 		else s1
     in
-      (*prerr_endline "Active table :"; 
+      (*prerr_endline "Active table :";
        (List.iter (fun x -> prerr_endline (Pp.pp_unit_clause x))
           (fst actives)); *)
 
-    let (bag,maxvar,actives,passives,g_actives,g_passives) as status  =      
+    let (bag,maxvar,actives,passives,g_actives,g_passives) as status  =
       aux_select bag passives g_passives
     in
-      debug (debug_status status);       
+      debug (debug_status status);
       given_clause ~useage
-        bag maxvar iterno weight_picks max_steps timeout 
+        bag maxvar iterno weight_picks max_steps timeout
         actives passives g_actives g_passives
   ;;
 
   let check_and_infer ~no_demod iterno status current =
     let bag,maxvar,actives,passives,g_actives,g_passives = status in
-    match 
-      Sup.simplify_goal 
-        ~no_demod maxvar (snd actives) bag g_actives current 
+    match
+      Sup.simplify_goal
+        ~no_demod maxvar (snd actives) bag g_actives current
     with
       | None -> debug (lazy "None"); status
-      | Some (bag,g_current) -> 
-	  let _ = 
-	    debug (lazy("Infer on goal : " 
-			^ Pp.pp_unit_clause g_current)) 
+      | Some (bag,g_current) ->
+	  let _ =
+	    debug (lazy("Infer on goal : "
+			^ Pp.pp_unit_clause g_current))
 	  in
 	    backward_infer_step bag maxvar actives passives
               g_actives g_passives g_current iterno
 
-  (* similar to given_clause, but it merely works on goals, 
+  (* similar to given_clause, but it merely works on goals,
      in parallel, at each iteration *)
   let rec goal_narrowing iterno max_steps timeout status
-  = 
+  =
     debug (debug_status status);
     let iterno = iterno + 1 in
     if iterno = max_steps || check_timeout timeout then
       last_chance status
-    else 
-    let _,_,_,_,_,g_passives = status in 
+    else
+    let _,_,_,_,_,g_passives = status in
     let passive_goals = WeightPassiveSet.elements (fst g_passives) in
-    let newstatus = 
+    let newstatus =
       List.fold_left
 	(fun acc g ->
 	   let _bag,_maxvar,_actives,_passives,_g_actives,g_passives = acc in
 	   let _g_passives =
 	     remove_passive_goal g_passives g in
 	   let current = snd g in
-	   let _ = 
-	     debug (lazy("Selected goal gn: " ^ Pp.pp_unit_clause current)) 
+	   let _ =
+	     debug (lazy("Selected goal gn: " ^ Pp.pp_unit_clause current))
 	   in
 	     (* we work both on the original goal and the demodulated one*)
 	   let acc = check_and_infer ~no_demod:false iterno acc current
@@ -517,7 +524,7 @@ module Paramod (B : Orderings.Blob) = struct
             | (_,_,_,Terms.Step (_,i1,i2,_,_,_)),_,_ ->
                 if (not ongoal) && (List.mem i acce) then accg,acce
                 else
-                  let accg,acce = 
+                  let accg,acce =
                     traverse false (traverse ongoal (accg,acce) i1) i2
                   in
                     if ongoal then i::accg,acce else accg,i::acce
@@ -526,8 +533,8 @@ module Paramod (B : Orderings.Blob) = struct
           (List.rev esteps)@gsteps
       in
       debug (lazy ("steps: " ^ (string_of_int (List.length l))));
-      let max_w = 
-	List.fold_left 
+      let max_w =
+	List.fold_left
 	  (fun acc i ->
 	     let (cl,_,_) = Terms.get_from_bag i bag in
 	       max acc (Order.compute_unit_clause_weight cl)) 0 l in
@@ -537,16 +544,16 @@ module Paramod (B : Orderings.Blob) = struct
 	      if d then
 		prerr_endline
 		(Printf.sprintf "Id : %d, selected at %d, weight %d,disc, by %s"
-		   id it (Order.compute_unit_clause_weight cl) 
+		   id it (Order.compute_unit_clause_weight cl)
 		   (Pp.pp_proof_step proof))
 	      else
 	       prerr_endline
 		(Printf.sprintf "Id : %d, selected at %d, weight %d by %s"
-		   id it (Order.compute_unit_clause_weight cl) 
+		   id it (Order.compute_unit_clause_weight cl)
 		   (Pp.pp_proof_step proof))) l;*)
         debug (lazy ("Proof:" ^
-          (String.concat "\n" 
-	     (List.map 
+          (String.concat "\n"
+	     (List.map
 		(fun x ->
 		   let cl,_,_ = Terms.get_from_bag x bag in
 		     Pp.pp_unit_clause cl) l))));
@@ -562,10 +569,10 @@ module Paramod (B : Orderings.Blob) = struct
     in
     let g_actives = [] in
     let actives = [], IDX.DT.empty in
-    try 
+    try
      given_clause ~useage ~noinfer:false
       bag maxvar 0  0 max_steps timeout actives passives g_actives g_passives
-    with 
+    with
     | Sup.Success (bag, _, (i,_,_,_),subst) ->
 	compute_result bag i subst
     | Stop (Unsatisfiable _) -> Error "solution found!"
@@ -578,7 +585,7 @@ let demod s goal =
   let bag, ((i,_,_,_) as g1) = Sup.demodulate bag g (snd actives) in
     if g1 = g then GaveUp else compute_result bag i []
 (*
-  if Terms.is_eq_clause g then 
+  if Terms.is_eq_clause g then
 
   else GaveUp *)
 
@@ -586,8 +593,8 @@ let fast_eq_check s goal =
   let (_,_,_,_,_,g_passives) as s = initialize_goal s goal in
   if is_passive_g_set_empty g_passives then (Error "not an equation" : szsontology)
   else
-  try 
-    goal_narrowing 0 2 None s
+  try
+    goal_narrowing 0 !max_steps None s
   with
     | Sup.Success (bag, _, (i,_,_,_),subst) ->
 	compute_result bag i subst
diff --git a/components/ng_paramodulation/paramod.mli b/components/ng_paramodulation/paramod.mli
index 367d79394..9eb8e41eb 100644
--- a/components/ng_paramodulation/paramod.mli
+++ b/components/ng_paramodulation/paramod.mli
@@ -11,6 +11,8 @@
 
 (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
 
+val max_steps: int ref
+
 module type Paramod =
   sig
     type t
diff --git a/components/ng_paramodulation/pp.ml b/components/ng_paramodulation/pp.ml
index 3f2a5cecc..e10e48c9a 100644
--- a/components/ng_paramodulation/pp.ml
+++ b/components/ng_paramodulation/pp.ml
@@ -121,7 +121,7 @@ let pp_unit_clause ~formatter:f c =
           Format.fprintf f "@]"
 ;;
 
-let pp_bag ~formatter:f (_,bag) = 
+let pp_bag ~formatter:f (_,bag) =
   Format.fprintf f "@[<v>";
   Terms.M.iter 
   (fun _ (c,d,_) -> pp_unit_clause ~formatter:f c;
diff --git a/components/ng_tactics/nnAuto.ml b/components/ng_tactics/nnAuto.ml
index 92682c8ad..e5d904eed 100644
--- a/components/ng_tactics/nnAuto.ml
+++ b/components/ng_tactics/nnAuto.ml
@@ -1,20 +1,20 @@
 (*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic        
-    ||A||  Library of Mathematics, developed at the Computer Science     
-    ||T||  Department, University of Bologna, Italy.                     
-    ||I||                                                                 
-    ||T||  HELM is free software; you can redistribute it and/or         
-    ||A||  modify it under the terms of the GNU General Public License   
-    \   /  version 2 or (at your option) any later version.      
-     \ /   This software is distributed as is, NO WARRANTY.     
+    ||M||  This file is part of HELM, an Hypertextual, Electronic
+    ||A||  Library of Mathematics, developed at the Computer Science
+    ||T||  Department, University of Bologna, Italy.
+    ||I||
+    ||T||  HELM is free software; you can redistribute it and/or
+    ||A||  modify it under the terms of the GNU General Public License
+    \   /  version 2 or (at your option) any later version.
+     \ /   This software is distributed as is, NO WARRANTY.
       V_______________________________________________________________ *)
 
 open Printf
 
-let print ?(depth=0) s = 
-  prerr_endline (String.make (2*depth) ' '^Lazy.force s) 
-let noprint ?depth:(_=0) _ = () 
-let debug_print = noprint
+let print ?(depth=0) s =
+  prerr_endline (String.make (2*depth) ' '^Lazy.force s)
+let noprint ?depth:(_depth=0) _s = ()
+let debug_print = ref noprint
 
 open Continuationals.Stack
 open NTacStatus
@@ -53,7 +53,7 @@ let incr_uses tbl item =
 
 let toref f tbl t =
   match t with
-    | Ast.NRef n -> 
+    | Ast.NRef n ->
         f tbl n
     | Ast.NCic _  (* local candidate *)
     | _  ->  ()
@@ -72,8 +72,8 @@ let print_stat _status tbl =
   let vcompare (_,v1) (_,v2) =
     Stdlib.compare (relevance v1) (relevance v2) in
   let l = List.sort vcompare l in
-  let short_name r = 
-    Filename.chop_extension 
+  let short_name r =
+(*    Filename.chop_extension *) (* FG: This causes an error because of the uri fragment *)
       (Filename.basename (NReference.string_of_reference r))
   in
   let vstring (a,v)=
@@ -82,7 +82,7 @@ let print_stat _status tbl =
       "; uses = " ^ (string_of_int !(v.uses)) ^
       "; nom = " ^ (string_of_int !(v.nominations)) in
   lazy ("\n\nSTATISTICS:\n" ^
-          String.concat "\n" (List.map vstring l)) 
+          String.concat "\n" (List.map vstring l))
 
 (* ======================= utility functions ========================= *)
 module IntSet = Set.Make(struct type t = int let compare = compare end)
@@ -104,7 +104,7 @@ let deps status g =
   metas_of_term status gty
 ;;
 
-let menv_closure status gl = 
+let menv_closure status gl =
   let rec closure acc = function
     | [] -> acc
     | x::l when IntSet.mem x acc -> closure acc l
@@ -112,29 +112,29 @@ let menv_closure status gl =
   in closure IntSet.empty gl
 ;;
 
-(* we call a "fact" an object whose hypothesis occur in the goal 
+(* we call a "fact" an object whose hypothesis occur in the goal
    or in types of goal-variables *)
-let branch status ty =  
+let branch status ty =
   let status, ty, metas = saturate ~delta:0 status ty in
   noprint (lazy ("saturated ty :" ^ (ppterm status ty)));
   let g_metas = metas_of_term status ty in
   let clos = menv_closure status g_metas in
   (* let _,_,metasenv,_,_ = status#obj in *)
-  let menv = 
+  let menv =
     List.fold_left
       (fun acc m ->
          let _, m = term_of_cic_term status m (ctx_of m) in
-         match m with 
+         match m with
          | NCic.Meta(i,_) -> IntSet.add i acc
          | _ -> assert false)
       IntSet.empty metas
-  in 
+  in
   (* IntSet.subset menv clos *)
   IntSet.cardinal(IntSet.diff menv clos)
 
 let is_a_fact status ty = branch status ty = 0
 
-let is_a_fact_obj s uri = 
+let is_a_fact_obj s uri =
   let obj = NCicEnvironment.get_checked_obj s uri in
   match obj with
     | (_,_,[],[],NCic.Constant(_,_,_,ty,_)) ->
@@ -142,15 +142,15 @@ let is_a_fact_obj s uri =
 (* aggiungere i costruttori *)
     | _ -> false
 
-let is_a_fact_ast status subst metasenv ctx cand = 
- noprint ~depth:0 
-   (lazy ("checking facts " ^ NotationPp.pp_term status cand)); 
+let is_a_fact_ast status subst metasenv ctx cand =
+ noprint ~depth:0
+   (lazy ("checking facts " ^ NotationPp.pp_term status cand));
  let status, t = disambiguate status ctx ("",0,cand) `XTNone in
  let status,t = term_of_cic_term status t ctx in
  let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
    is_a_fact status (mk_cic_term ctx ty)
 
-let current_goal status = 
+let current_goal status =
   let open_goals = head_goals status#stack in
   assert (List.length open_goals  = 1);
   let open_goal = List.hd open_goals in
@@ -158,16 +158,16 @@ let current_goal status =
   let ctx = ctx_of gty in
     open_goal, ctx, gty
 
-let height_of_ref status (NReference.Ref (uri, x)) = 
+let height_of_ref status (NReference.Ref (uri, x)) =
   match x with
-  | NReference.Decl 
-  | NReference.Ind _ 
+  | NReference.Decl
+  | NReference.Ind _
   | NReference.Con _
-  | NReference.CoFix _ -> 
+  | NReference.CoFix _ ->
       let _,height,_,_,_ = NCicEnvironment.get_checked_obj status uri in
-      height 
-  | NReference.Def h -> h 
-  | NReference.Fix (_,_,h) -> h 
+      height
+  | NReference.Def h -> h
+  | NReference.Fix (_,_,h) -> h
 ;;
 
 (*************************** height functions ********************************)
@@ -180,10 +180,10 @@ let fast_height_of_term status t =
    | NCic.Rel _
    | NCic.Sort _ -> ()
    | NCic.Implicit _ -> assert false
-   | NCic.Const nref -> 
+   | NCic.Const nref ->
 (*
                    prerr_endline (status#ppterm ~metasenv:[] ~subst:[]
-                   ~context:[] t ^ ":" ^ string_of_int (height_of_ref status nref));            
+                   ~context:[] t ^ ":" ^ string_of_int (height_of_ref status nref));
 *)
        h := max !h (height_of_ref status nref)
    | NCic.Prod (_,t1,t2)
@@ -195,27 +195,27 @@ let fast_height_of_term status t =
   aux t; !h
 ;;
 
-let height_of_goal g status = 
+let height_of_goal g status =
   let ty = get_goalty status g in
   let context = ctx_of ty in
   let _, ty = term_of_cic_term status ty (ctx_of ty) in
   let h = ref (fast_height_of_term status ty) in
-  List.iter 
-    (function 
+  List.iter
+    (function
        | _, NCic.Decl ty -> h := max !h (fast_height_of_term status ty)
-       | _, NCic.Def (bo,ty) -> 
+       | _, NCic.Def (bo,ty) ->
            h := max !h (fast_height_of_term status ty);
            h := max !h (fast_height_of_term status bo);
     )
     context;
   !h
-;;      
+;;
 
-let height_of_goals status = 
+let height_of_goals status =
   let open_goals = head_goals status#stack in
   assert (List.length open_goals > 0);
   let h = ref 1 in
-  List.iter 
+  List.iter
     (fun open_goal ->
        h := max !h (height_of_goal open_goal status))
      open_goals;
@@ -226,7 +226,7 @@ let height_of_goals status =
 (* =============================== paramod =========================== *)
 let solve f status eq_cache goal =
 (*
-  let f = 
+  let f =
     if fast then NCicParamod.fast_eq_check
     else NCicParamod.paramod in
 *)
@@ -235,37 +235,37 @@ let solve f status eq_cache goal =
   let gty = NCicUntrusted.apply_subst status subst ctx gty in
   let build_status (pt, _, metasenv, subst) =
     try
-      debug_print (lazy ("refining: "^(status#ppterm ctx subst metasenv pt)));
-      let stamp = Unix.gettimeofday () in 
+      !debug_print (lazy ("refining: "^(status#ppterm ctx subst metasenv pt)));
+      let stamp = Unix.gettimeofday () in
       let metasenv, subst, pt, pty =
         (* NCicRefiner.typeof status
           (* (status#set_coerc_db NCicCoercion.empty_db) *)
           metasenv subst ctx pt None in
-          debug_print (lazy ("refined: "^(status#ppterm ctx subst metasenv pt)));
+          !debug_print (lazy ("refined: "^(status#ppterm ctx subst metasenv pt)));
           noprint (lazy ("synt: "^(status#ppterm ctx subst metasenv pty)));
           let metasenv, subst =
             NCicUnification.unify status metasenv subst ctx gty pty *)
-        NCicRefiner.typeof 
-          (status#set_coerc_db NCicCoercion.empty_db) 
-          metasenv subst ctx pt (`XTSome gty) 
-        in 
+        NCicRefiner.typeof
+          (status#set_coerc_db NCicCoercion.empty_db)
+          metasenv subst ctx pt (`XTSome gty)
+        in
           noprint (lazy (Printf.sprintf "Refined in %fs"
-                     (Unix.gettimeofday() -. stamp))); 
+                     (Unix.gettimeofday() -. stamp)));
           let status = status#set_obj (n,h,metasenv,subst,o) in
           let metasenv = List.filter (fun (j,_) -> j <> goal) metasenv in
           let subst = (goal,(gname,ctx,pt,pty)) :: subst in
             Some (status#set_obj (n,h,metasenv,subst,o))
-    with 
-        NCicRefiner.RefineFailure msg 
+    with
+        NCicRefiner.RefineFailure msg
       | NCicRefiner.Uncertain msg ->
-          debug_print (lazy ("WARNING U: refining in fast_eq_check failed\n" ^
-                        snd (Lazy.force msg) ^        
-                        "\n in the environment\n" ^ 
+          !debug_print (lazy ("WARNING U: refining in fast_eq_check failed\n" ^
+                        snd (Lazy.force msg) ^
+                        "\n in the environment\n" ^
                         status#ppmetasenv subst metasenv)); None
-      | NCicRefiner.AssertFailure msg -> 
-          debug_print (lazy ("WARNING F: refining in fast_eq_check failed" ^
+      | NCicRefiner.AssertFailure msg ->
+          !debug_print (lazy ("WARNING F: refining in fast_eq_check failed" ^
                         Lazy.force msg ^
-                        "\n in the environment\n" ^ 
+                        "\n in the environment\n" ^
                         status#ppmetasenv subst metasenv)); None
       | Sys.Break as e -> raise e
       | _ -> None
@@ -276,20 +276,20 @@ let solve f status eq_cache goal =
 
 let fast_eq_check eq_cache status (goal:int) =
   match solve NCicParamod.fast_eq_check status eq_cache goal with
-  | [] -> raise (Error (lazy "no proof found",None))
+  | [] -> raise (Error (lazy "fast_eq_check: no proof found",None))
   | s::_ -> s
 ;;
 
-let dist_fast_eq_check eq_cache s = 
+let dist_fast_eq_check eq_cache s =
   NTactics.distribute_tac (fast_eq_check eq_cache) s
 ;;
 
 let auto_eq_check eq_cache status =
-  try 
+  try
     let s = dist_fast_eq_check eq_cache status in
       [s]
   with
-    | Error _ -> debug_print (lazy ("no paramod proof found"));[]
+    | Error _ -> !debug_print (lazy ("no paramod proof found"));[]
 ;;
 
 let index_local_equations eq_cache ?(flag=false) status =
@@ -303,21 +303,21 @@ let index_local_equations eq_cache ?(flag=false) status =
   let _,_,metasenv,subst,_ = status#obj in
   let ctx = apply_subst_context ~fix_projections:true status (ctx_of ngty) in
   let c = ref 0 in
-  List.fold_left 
+  List.fold_left
     (fun eq_cache _ ->
        c:= !c+1;
        let t = NCic.Rel !c in
          try
            let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
            if is_a_fact status (mk_cic_term ctx ty) then
-             (debug_print(lazy("eq indexing " ^ (status#ppterm ctx subst metasenv ty)));
+             (!debug_print(lazy("eq indexing " ^ (status#ppterm ctx subst metasenv ty)));
               NCicParamod.forward_infer_step status metasenv subst ctx eq_cache t ty)
-           else 
+           else
              (noprint (lazy ("not a fact: " ^ (status#ppterm ctx subst metasenv ty)));
               eq_cache)
-         with 
+         with
            | NCicTypeChecker.TypeCheckerFailure _
-           | NCicTypeChecker.AssertFailure _ -> eq_cache) 
+           | NCicTypeChecker.AssertFailure _ -> eq_cache)
     eq_cache ctx
  end
 ;;
@@ -344,35 +344,35 @@ let index_local_equations2 eq_cache status open_goal lemmas ?flag:(_=false) nohy
     List.map (fun i -> NCic.Rel (i + 1))
      (HExtlib.list_seq 1 (List.length ctx)) in
   let lemmas = lemmas @ local_equations in
-  List.fold_left 
+  List.fold_left
     (fun eq_cache t ->
          try
            let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
            if is_a_fact status (mk_cic_term ctx ty) then
-             (debug_print(lazy("eq indexing " ^ (status#ppterm ctx subst metasenv ty)));
+             (!debug_print(lazy("eq indexing " ^ (status#ppterm ctx subst metasenv ty)));
               NCicParamod.forward_infer_step status metasenv subst ctx eq_cache t ty)
-           else 
+           else
              (noprint (lazy ("not a fact: " ^ (status#ppterm ctx subst metasenv ty)));
               eq_cache)
-         with 
+         with
            | NCicTypeChecker.TypeCheckerFailure _
            | NCicTypeChecker.AssertFailure _ -> eq_cache)
     eq_cache lemmas
 ;;
 
-let fast_eq_check_tac ~params:_ s = 
-  let unit_eq = index_local_equations s#eq_cache s in   
+let fast_eq_check_tac ~params:_ s =
+  let unit_eq = index_local_equations s#eq_cache s in
   dist_fast_eq_check unit_eq s
 ;;
 
 let paramod eq_cache status goal =
   match solve NCicParamod.paramod status eq_cache goal with
-  | [] -> raise (Error (lazy "no proof found",None))
+  | [] -> raise (Error (lazy "paramod: no proof found",None))
   | s::_ -> s
 ;;
 
-let paramod_tac ~params:_ s = 
-  let unit_eq = index_local_equations s#eq_cache s in   
+let paramod_tac ~params:_ s =
+  let unit_eq = index_local_equations s#eq_cache s in
   NTactics.distribute_tac (paramod unit_eq) s
 ;;
 
@@ -382,21 +382,21 @@ let demod eq_cache status goal =
   | s::_ -> s
 ;;
 
-let demod_tac ~params s = 
+let demod_tac ~params s =
   let unit_eq s i =
    index_local_equations2 s#eq_cache s i (fst params)
     (List.mem_assoc "nohyps" (snd params))
-  in   
+  in
    NTactics.distribute_tac (fun s i -> demod (unit_eq s i) s i) s
 ;;
 
 (*
-let fast_eq_check_tac_all  ~params eq_cache status = 
+let fast_eq_check_tac_all  ~params eq_cache status =
   let g,_,_ = current_goal status in
   let allstates = fast_eq_check_all status eq_cache g in
   let pseudo_low_tac s _ _ = s in
-  let pseudo_low_tactics = 
-    List.map pseudo_low_tac allstates 
+  let pseudo_low_tactics =
+    List.map pseudo_low_tac allstates
   in
     List.map (fun f -> NTactics.distribute_tac f status) pseudo_low_tactics
 ;;
@@ -408,26 +408,26 @@ let demod status eq_cache goal =
   let gname, ctx, gty = List.assoc goal metasenv in
   let gty = NCicUntrusted.apply_subst subst ctx gty in
 
-let demod_tac ~params s = 
-  let unit_eq = index_local_equations s#eq_cache s in   
+let demod_tac ~params s =
+  let unit_eq = index_local_equations s#eq_cache s in
   dist_fast_eq_check unit_eq s
 *)
 
 (*************** subsumption ****************)
 
 let close_wrt_context status =
-  List.fold_left 
-    (fun ty ctx_entry -> 
-        match ctx_entry with 
+  List.fold_left
+    (fun ty ctx_entry ->
+        match ctx_entry with
        | name, NCic.Decl t -> NCic.Prod(name,t,ty)
        | _name, NCic.Def(bo, _) -> NCicSubstitution.subst status bo ty)
 ;;
 
 let args_for_context ?(k=1) ctx =
   let _,args =
-    List.fold_left 
-      (fun (n,l) ctx_entry -> 
-         match ctx_entry with 
+    List.fold_left
+      (fun (n,l) ctx_entry ->
+         match ctx_entry with
            | _name, NCic.Decl _t -> n+1,NCic.Rel(n)::l
            | _name, NCic.Def(_bo, _) -> n+1,l)
       (k,[]) ctx in
@@ -445,38 +445,38 @@ let constant_for_meta status ctx ty i =
 
 (* not used *)
 let refresh metasenv =
-  List.fold_left 
+  List.fold_left
     (fun (metasenv,subst) (i,(iattr,ctx,ty)) ->
        let ikind = NCicUntrusted.kind_of_meta iattr in
-       let metasenv,_j,instance,ty = 
-         NCicMetaSubst.mk_meta ~attrs:iattr 
+       let metasenv,_j,instance,ty =
+         NCicMetaSubst.mk_meta ~attrs:iattr
            metasenv ctx ~with_type:ty ikind in
        let s_entry = i,(iattr, ctx, instance, ty) in
        let metasenv = List.filter (fun (x,_) -> i <> x) metasenv in
-         metasenv,s_entry::subst) 
+         metasenv,s_entry::subst)
       (metasenv,[]) metasenv
 
 (* close metasenv returns a ground instance of all the metas in the
 metasenv, insantiatied with axioms, and the list of these axioms *)
-let close_metasenv status metasenv subst = 
+let close_metasenv status metasenv subst =
   (*
   let metasenv = NCicUntrusted.apply_subst_metasenv subst metasenv in
   *)
-  let metasenv = NCicUntrusted.sort_metasenv status subst metasenv in 
-    List.fold_left 
+  let metasenv = NCicUntrusted.sort_metasenv status subst metasenv in
+    List.fold_left
       (fun (subst,objs) (i,(_iattr,ctx,ty)) ->
          let ty = NCicUntrusted.apply_subst status subst ctx ty in
-         let ctx = 
-           NCicUntrusted.apply_subst_context status ~fix_projections:true 
+         let ctx =
+           NCicUntrusted.apply_subst_context status ~fix_projections:true
              subst ctx in
-         let (uri,_,_,_,_obj) as okind = 
+         let (uri,_,_,_,_obj) as okind =
            constant_for_meta status ctx ty i in
          try
            NCicEnvironment.check_and_add_obj status okind;
            let iref = NReference.reference_of_spec uri NReference.Decl in
            let iterm =
              let args = args_for_context ctx in
-               if args = [] then NCic.Const iref 
+               if args = [] then NCic.Const iref
                else NCic.Appl(NCic.Const iref::args)
            in
            (* prerr_endline (status#ppterm ctx [] [] iterm); *)
@@ -498,27 +498,27 @@ let ground_instances status gl =
   let subst, objs = close_metasenv status submenv subst in
   try
     List.iter
-      (fun i -> 
+      (fun i ->
          let (_, ctx, t, _) = List.assoc i subst in
            noprint (lazy (status#ppterm ctx [] [] t));
-           List.iter 
-             (fun ((uri,_,_,_,_) as obj) -> 
-                NCicEnvironment.invalidate_item (`Obj (uri, obj))) 
+           List.iter
+             (fun ((uri,_,_,_,_) as obj) ->
+                NCicEnvironment.invalidate_item (`Obj (uri, obj)))
              objs;
            ())
       gl
   with
-      Not_found -> assert false 
+      Not_found -> assert false
   (* (ctx,t) *)
 ;;
 
-let replace_meta status i args target = 
+let replace_meta status i args target =
   let rec aux k = function
     (* TODO: local context *)
     | NCic.Meta (j,lc) when i = j ->
         (match args with
            | [] -> NCic.Rel 1
-           | _ -> let args = 
+           | _ -> let args =
                List.map (NCicSubstitution.subst_meta status lc) args in
                NCic.Appl(NCic.Rel k::args))
     | NCic.Meta (_j,lc) as m ->
@@ -535,11 +535,11 @@ let replace_meta status i args target =
 ;;
 
 let close_wrt_metasenv status subst =
-  List.fold_left 
+  List.fold_left
     (fun ty (i,(_iattr,ctx,mty)) ->
        let mty = NCicUntrusted.apply_subst status subst ctx mty in
-       let ctx = 
-         NCicUntrusted.apply_subst_context status ~fix_projections:true 
+       let ctx =
+         NCicUntrusted.apply_subst_context status ~fix_projections:true
            subst ctx in
        let cty = close_wrt_context status mty ctx in
        let name = "foo"^(string_of_int i) in
@@ -555,14 +555,14 @@ let close status g =
   let _,_,metasenv,subst,_ = status#obj in
   let subset = menv_closure status [g] in
   let subset = IntSet.remove g subset in
-  let elems = IntSet.elements subset in 
+  let elems = IntSet.elements subset in
   let _, ctx, ty = NCicUtils.lookup_meta g metasenv in
   let ty = NCicUntrusted.apply_subst status subst ctx ty in
   noprint (lazy ("metas in " ^ (status#ppterm ctx [] metasenv ty)));
   noprint (lazy (String.concat ", " (List.map string_of_int elems)));
   let submenv = List.filter (fun (x,_) -> IntSet.mem x subset) metasenv in
-  let submenv = List.rev (NCicUntrusted.sort_metasenv status subst submenv) in 
-(*  
+  let submenv = List.rev (NCicUntrusted.sort_metasenv status subst submenv) in
+(*
     let submenv = metasenv in
 *)
   let ty = close_wrt_metasenv status subst ty submenv in
@@ -574,23 +574,23 @@ let close status g =
 
 let saturate_to_ref status metasenv subst ctx nref ty =
   let height = height_of_ref status nref in
-  let rec aux metasenv ty args = 
-    let ty,metasenv,moreargs =  
-      NCicMetaSubst.saturate status ~delta:height metasenv subst ctx ty 0 in 
+  let rec aux metasenv ty args =
+    let ty,metasenv,moreargs =
+      NCicMetaSubst.saturate status ~delta:height metasenv subst ctx ty 0 in
     match ty with
-      | NCic.Const(NReference.Ref (_,NReference.Def _) as nre) 
+      | NCic.Const(NReference.Ref (_,NReference.Def _) as nre)
           when nre<>nref ->
-          let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def status nre in 
+          let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def status nre in
             aux metasenv bo (args@moreargs)
-      | NCic.Appl(NCic.Const(NReference.Ref (_,NReference.Def _) as nre)::tl) 
+      | NCic.Appl(NCic.Const(NReference.Ref (_,NReference.Def _) as nre)::tl)
           when nre<>nref ->
           let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def status nre in
-            aux metasenv (NCic.Appl(bo::tl)) (args@moreargs) 
+            aux metasenv (NCic.Appl(bo::tl)) (args@moreargs)
     | _ -> ty,metasenv,(args@moreargs)
   in
     aux metasenv ty []
 
-let smart_apply t unit_eq status g = 
+let smart_apply t unit_eq status g =
   let n,h,metasenv,_subst,o = status#obj in
   let _gname, ctx, gty = List.assoc g metasenv in
   (* let ggty = mk_cic_term context gty in *)
@@ -598,70 +598,70 @@ let smart_apply t unit_eq status g =
   let status,t = term_of_cic_term status t ctx in
   let _,_,metasenv,subst,_ = status#obj in
   let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
-  let ty,metasenv,args = 
+  let ty,metasenv,args =
     match gty with
       | NCic.Const(nref)
-      | NCic.Appl(NCic.Const(nref)::_) -> 
+      | NCic.Appl(NCic.Const(nref)::_) ->
           saturate_to_ref status metasenv subst ctx nref ty
-      | _ -> 
+      | _ ->
           NCicMetaSubst.saturate status metasenv subst ctx ty 0 in
   let metasenv,j,inst,_ = NCicMetaSubst.mk_meta metasenv ctx `IsTerm in
   let status = status#set_obj (n,h,metasenv,subst,o) in
-  let pterm = if args=[] then t else 
+  let pterm = if args=[] then t else
     match t with
-      | NCic.Appl l -> NCic.Appl(l@args) 
-      | _ -> NCic.Appl(t::args) 
+      | NCic.Appl l -> NCic.Appl(l@args)
+      | _ -> NCic.Appl(t::args)
   in
   noprint(lazy("pterm " ^ (status#ppterm ctx [] [] pterm)));
   noprint(lazy("pty " ^ (status#ppterm ctx [] [] ty)));
-  let eq_coerc =       
-    let uri = 
+  let eq_coerc =
+    let uri =
       NUri.uri_of_string "cic:/matita/basics/logic/eq_coerc.con" in
     let ref = NReference.reference_of_spec uri (NReference.Def(2)) in
       NCic.Const ref
   in
-  let smart = 
+  let smart =
     NCic.Appl[eq_coerc;ty;NCic.Implicit `Type;pterm;inst] in
-  let smart = mk_cic_term ctx smart in 
+  let smart = mk_cic_term ctx smart in
     try
       let status = instantiate status g smart in
       let _,_,metasenv,subst,_ = status#obj in
       let _,ctx,jty = List.assoc j metasenv in
       let jty = NCicUntrusted.apply_subst status subst ctx jty in
-        debug_print(lazy("goal " ^ (status#ppterm ctx [] [] jty)));
+        !debug_print(lazy("goal " ^ (status#ppterm ctx [] [] jty)));
         let res = fast_eq_check unit_eq status j in
-        debug_print(lazy("ritorno da fast_eq_check"));
+        !debug_print(lazy("ritorno da fast_eq_check"));
         res
     with
       | NCicEnvironment.ObjectNotFound _s as e ->
           raise (Error (lazy "eq_coerc non yet defined",Some e))
-      | Error _ as e -> debug_print (lazy "error"); raise e
-(* FG: for now we catch TypeCheckerFailure; to be understood *)  
+      | Error _ as e -> !debug_print (lazy "error"); raise e
+(* FG: for now we catch TypeCheckerFailure; to be understood *)
       | NCicTypeChecker.TypeCheckerFailure _ ->
-          debug_print (lazy "TypeCheckerFailure");
-          raise (Error (lazy "no proof found",None))
+          !debug_print (lazy "TypeCheckerFailure");
+          raise (Error (lazy "smart_apply: no proof found",None))
 ;;
 
 let compare_statuses ~past ~present =
- let _,_,past,_,_ = past#obj in 
- let _,_,present,_,_ = present#obj in 
+ let _,_,past,_,_ = past#obj in
+ let _,_,present,_,_ = present#obj in
  List.map fst (List.filter (fun (i,_) -> not(List.mem_assoc i past)) present),
  List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i present)) past)
 ;;
 
 (* paramodulation has only an implicit knoweledge of the symmetry of equality;
-   hence it is in trouble in proving (a = b) = (b = a) *) 
+   hence it is in trouble in proving (a = b) = (b = a) *)
 let try_sym tac status g =
   let sym_eq = Ast.Appl [Ast.Ident("sym_eq",None); Ast.Implicit `Vector] in
   let _,_,metasenv,subst,_ = status#obj in
   let _, context, gty = List.assoc g metasenv in
-  let is_eq = 
-    NCicParamod.is_equation status metasenv subst context gty 
+  let is_eq =
+    NCicParamod.is_equation status metasenv subst context gty
   in
   if is_eq then
     try tac status g
     with Error _ ->
-      let new_status = instantiate_with_ast status g ("",0,sym_eq) in 
+      let new_status = instantiate_with_ast status g ("",0,sym_eq) in
       let go, _ = compare_statuses ~past:status ~present:new_status in
       assert (List.length go  = 1);
       let ng = List.hd go in
@@ -670,12 +670,12 @@ let try_sym tac status g =
 ;;
 
 let smart_apply_tac t s =
-  let unit_eq = index_local_equations s#eq_cache s in   
-  NTactics.distribute_tac (try_sym (smart_apply t unit_eq)) s 
+  let unit_eq = index_local_equations s#eq_cache s in
+  NTactics.distribute_tac (try_sym (smart_apply t unit_eq)) s
   (* NTactics.distribute_tac (smart_apply t unit_eq) s *)
 
 let smart_apply_auto t eq_cache =
-  NTactics.distribute_tac (try_sym (smart_apply t eq_cache)) 
+  NTactics.distribute_tac (try_sym (smart_apply t eq_cache))
   (* NTactics.distribute_tac (smart_apply t eq_cache) *)
 
 
@@ -773,11 +773,11 @@ let keys_of_type status orig_ty =
 *)
    [ty] in
 (*CSC: strange: we keep ty, ty normalized and ty ~delta:(h-1) *)
-  let keys = 
+  let keys =
     let _, ty = term_of_cic_term status ty (ctx_of ty) in
     match ty with
-    | NCic.Const (NReference.Ref (_,(NReference.Def h | NReference.Fix (_,_,h)))) 
-    | NCic.Appl (NCic.Const(NReference.Ref(_,(NReference.Def h | NReference.Fix (_,_,h))))::_) 
+    | NCic.Const (NReference.Ref (_,(NReference.Def h | NReference.Fix (_,_,h))))
+    | NCic.Appl (NCic.Const(NReference.Ref(_,(NReference.Def h | NReference.Fix (_,_,h))))::_)
        when h > 0 ->
          let _,ty,_= saturate status ~delta:(h-1) orig_ty in
          ty::keys
@@ -796,8 +796,8 @@ let keys_of_term status t =
     keys_of_type status orig_ty
 ;;
 
-let mk_th_cache status gl = 
-  List.fold_left 
+let mk_th_cache status gl =
+  List.fold_left
     (fun (status, acc) g ->
        let gty = get_goalty status g in
        let ctx = ctx_of gty in
@@ -805,14 +805,14 @@ let mk_th_cache status gl =
        noprint(lazy("th cache in: "^ppcontext status ctx));
        if List.mem_assq ctx acc then status, acc else
          let idx = InvRelDiscriminationTree.empty in
-         let status,_,idx = 
-           List.fold_left 
-             (fun (status, i, idx) _ -> 
+         let status,_,idx =
+           List.fold_left
+             (fun (status, i, idx) _ ->
                 let t = mk_cic_term ctx (NCic.Rel i) in
                 let status, keys = keys_of_term status t in
                 noprint(lazy("indexing: "^ppterm status t ^ ": " ^ string_of_int (List.length keys)));
                 let idx =
-                  List.fold_left (fun idx k -> 
+                  List.fold_left (fun idx k ->
                     InvRelDiscriminationTree.index idx k t) idx keys
                 in
                 status, i+1, idx)
@@ -826,35 +826,35 @@ let all_elements ctx cache =
   let dummy = mk_cic_term ctx (NCic.Meta (0,(0, (NCic.Irl 0)))) in
     try
       let idx = List.assq ctx cache in
-      Ncic_termSet.elements 
+      Ncic_termSet.elements
         (InvRelDiscriminationTree.retrieve_unifiables idx dummy)
     with Not_found -> []
 
-let add_to_th t c ty = 
+let add_to_th t c ty =
   let key_c = ctx_of t in
   if not (List.mem_assq key_c c) then
-      (key_c ,InvRelDiscriminationTree.index 
-               InvRelDiscriminationTree.empty ty t ) :: c 
+      (key_c ,InvRelDiscriminationTree.index
+               InvRelDiscriminationTree.empty ty t ) :: c
   else
     let rec replace = function
       | [] -> []
-      | (x, idx) :: tl when x == key_c -> 
+      | (x, idx) :: tl when x == key_c ->
           (x, InvRelDiscriminationTree.index idx ty t) :: tl
       | x :: tl -> x :: replace tl
-    in 
+    in
       replace c
 ;;
 
-let rm_from_th t c ty = 
+let rm_from_th t c ty =
   let key_c = ctx_of t in
   if not (List.mem_assq key_c c) then assert false
   else
     let rec replace = function
       | [] -> []
-      | (x, idx) :: tl when x == key_c -> 
+      | (x, idx) :: tl when x == key_c ->
           (x, InvRelDiscriminationTree.remove_index idx ty t) :: tl
       | x :: tl -> x :: replace tl
-    in 
+    in
       replace c
 ;;
 
@@ -862,13 +862,13 @@ let pp_idx status idx =
    InvRelDiscriminationTree.iter idx
       (fun k set ->
          noprint(lazy("K: " ^ NCicInverseRelIndexable.string_of_path k));
-         Ncic_termSet.iter 
-           (fun t -> debug_print(lazy("\t"^ppterm status t))) 
+         Ncic_termSet.iter
+           (fun t -> !debug_print(lazy("\t"^ppterm status t)))
            set)
 ;;
 
-let pp_th (status: #NTacStatus.pstatus) = 
-  List.iter 
+let pp_th (status: #NTacStatus.pstatus) =
+  List.iter
     (fun (ctx, idx) ->
        noprint(lazy( "-----------------------------------------------"));
        noprint(lazy( (status#ppcontext ~metasenv:[] ~subst:[] ctx)));
@@ -876,14 +876,14 @@ let pp_th (status: #NTacStatus.pstatus) =
        pp_idx status idx)
 ;;
 
-let search_in_th gty th = 
+let search_in_th gty th =
   let c = ctx_of gty in
   let rec aux acc = function
    | [] -> (* Ncic_termSet.elements *) acc
    | (_::tl) as k ->
-       try 
+       try
          let idx = List.assoc(*q*) k th in
-         let acc = Ncic_termSet.union acc 
+         let acc = Ncic_termSet.union acc
            (InvRelDiscriminationTree.retrieve_unifiables idx gty)
          in
          aux acc tl
@@ -912,20 +912,20 @@ type cache =
 
 let add_to_trace status ~depth cache t =
   match t with
-    | Ast.NRef _ -> 
-        debug_print ~depth (lazy ("Adding to trace: " ^ NotationPp.pp_term status t));
+    | Ast.NRef _ ->
+        !debug_print ~depth (lazy ("Adding to trace: " ^ NotationPp.pp_term status t));
         {cache with trace = t::cache.trace}
     | Ast.NCic _  (* local candidate *)
-    | _  -> (*not an application *) cache 
+    | _  -> (*not an application *) cache
 
-let pptrace status tr = 
-  (lazy ("Proof Trace: " ^ (String.concat ";" 
+let pptrace status tr =
+  (lazy ("Proof Trace: " ^ (String.concat ";"
                               (List.map (NotationPp.pp_term status) tr))))
 (* not used
 let remove_from_trace cache t =
   match t with
-    | Ast.NRef _ -> 
-        (match cache.trace with 
+    | Ast.NRef _ ->
+        (match cache.trace with
            |  _::tl -> {cache with trace = tl}
            | _ -> assert false)
     | Ast.NCic _  (* local candidate *)
@@ -948,9 +948,9 @@ exception Proved of NTacStatus.tac_status * Ast.term list
 
 let init_cache ?(facts=[]) ?(under_inspection=[],[])
     ?(failures=[])
-    ?(unit_eq=NCicParamod.empty_state) 
-    ?(trace=[]) 
-    _ = 
+    ?(unit_eq=NCicParamod.empty_state)
+    ?(trace=[])
+    _ =
     {facts = facts;
      failures = failures;
      under_inspection = under_inspection;
@@ -960,7 +960,7 @@ let init_cache ?(facts=[]) ?(under_inspection=[],[])
 let only _signature _context _candidate = true
 (*
         (* TASSI: nel trie ci mettiamo solo il body, non il ty *)
-  let candidate_ty = 
+  let candidate_ty =
    NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] candidate
   in
   let height = fast_height_of_term status candidate_ty in
@@ -968,12 +968,12 @@ let only _signature _context _candidate = true
   if rc = false then
     noprint (lazy ("Filtro: " ^ status#ppterm ~context:[] ~subst:[]
           ~metasenv:[] candidate ^ ": " ^ string_of_int height))
-  else 
+  else
     noprint (lazy ("Tengo: " ^ status#ppterm ~context:[] ~subst:[]
           ~metasenv:[] candidate ^ ": " ^ string_of_int height));
 
   rc *)
-;; 
+;;
 
 let candidate_no = ref 0;;
 
@@ -986,26 +986,26 @@ let sort_candidates status ctx candidates =
     let status,t = term_of_cic_term status ct ctx in
     let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
     let res = branch status (mk_cic_term ctx ty) in
-    noprint (lazy ("branch factor for: " ^ (ppterm status ct) ^ " = " 
+    noprint (lazy ("branch factor for: " ^ (ppterm status ct) ^ " = "
                       ^ (string_of_int res)));
       res
-  in 
+  in
   let candidates = List.map (fun t -> branch t,t) candidates in
-  let candidates = 
-     List.sort (fun (a,_) (b,_) -> a - b) candidates in 
+  let candidates =
+     List.sort (fun (a,_) (b,_) -> a - b) candidates in
   let candidates = List.map snd candidates in
-    noprint (lazy ("candidates =\n" ^ (String.concat "\n" 
+    noprint (lazy ("candidates =\n" ^ (String.concat "\n"
         (List.map (NotationPp.pp_term status) candidates))));
     candidates
 
 let sort_new_elems l =
   List.sort (fun (_,s1) (_,s2) -> openg_no s1 - openg_no s2) l
 
-let rec stack_goals level gs = 
+let rec stack_goals level gs =
   if level = 0 then []
-  else match gs with 
+  else match gs with
     | [] -> assert false
-    | (g,_,_,_,_)::s -> 
+    | (g,_,_,_,_)::s ->
         let is_open = function
           | (_,Continuationals.Stack.Open i) -> Some i
           | (_,Continuationals.Stack.Closed _) -> None
@@ -1019,16 +1019,16 @@ let open_goals level status = stack_goals level status#stack
 let try_candidate ?(smart=0) _flags depth status eq_cache _ctx t =
   try
     (*let old_og_no = List.length (open_goals (depth+1) status) in*)
-    debug_print ~depth (lazy ("try " ^ (string_of_int smart) ^ " : "
+    !debug_print ~depth (lazy ("try " ^ (string_of_int smart) ^ " : "
       ^ (NotationPp.pp_term status) t));
-    let status = 
+    let status =
       if smart = 0 then NTactics.apply_tac ("",0,t) status
-      else if smart = 1 then  
-        smart_apply_auto ("",0,t) eq_cache status 
+      else if smart = 1 then
+        smart_apply_auto ("",0,t) eq_cache status
       else (* smart = 2: both *)
         try NTactics.apply_tac ("",0,t) status
-        with Error _ -> 
-          smart_apply_auto ("",0,t) eq_cache status 
+        with Error _ ->
+          smart_apply_auto ("",0,t) eq_cache status
     in
 (* FG: this optimization rules out some applications of
  * lift_bind (from contribs/lambda_delta/Basic_2/substitution/lift.ma)
@@ -1036,7 +1036,7 @@ let try_candidate ?(smart=0) _flags depth status eq_cache _ctx t =
     (* we compare the expected branching with the actual one and
        prune the candidate when the latter is larger. The optimization
        is meant to rule out stange applications of flexible terms,
-       such as the application of eq_f that always succeeds.  
+       such as the application of eq_f that always succeeds.
        There is some gain but less than expected *)
     let og_no = List.length (open_goals (depth+1) status) in
     let status, cict = disambiguate status ctx ("",0,t) None in
@@ -1045,16 +1045,16 @@ let try_candidate ?(smart=0) _flags depth status eq_cache _ctx t =
     let ty = NCicTypeChecker.typeof status subst metasenv ctx ct in
     let res = branch status (mk_cic_term ctx ty) in
     let diff = og_no - old_og_no in
-    debug_print (lazy ("expected branching: " ^ (string_of_int res)));
-    debug_print (lazy ("actual: branching" ^ (string_of_int diff))); 
+    !debug_print (lazy ("expected branching: " ^ (string_of_int res)));
+    !debug_print (lazy ("actual: branching" ^ (string_of_int diff)));
     (* some flexibility *)
-    if og_no - old_og_no > res then 
-      (debug_print (lazy ("branch factor for: " ^ (ppterm status cict) ^ " = " 
+    if og_no - old_og_no > res then
+      (!debug_print (lazy ("branch factor for: " ^ (ppterm status cict) ^ " = "
                     ^ (string_of_int res) ^ " vs. " ^ (string_of_int og_no)));
-       debug_print ~depth (lazy "strange application"); None)
-    else 
+       !debug_print ~depth (lazy "strange application"); None)
+    else
 *)      (incr candidate_no; Some ((!candidate_no,t),status))
-   with Error _ -> debug_print ~depth (lazy "failed"); None
+   with Error _ -> !debug_print ~depth (lazy "failed"); None
 ;;
 
 let sort_of status subst metasenv ctx t =
@@ -1063,7 +1063,7 @@ let sort_of status subst metasenv ctx t =
    assert (metasenv = metasenv');
    NCicTypeChecker.typeof status subst metasenv ctx ty
 ;;
-  
+
 let type0= NUri.uri_of_string ("cic:/matita/pts/Type0.univ")
 ;;
 
@@ -1079,7 +1079,7 @@ let perforate_small status subst metasenv context t =
         in
           NCic.Appl (hd::List.map map tl)
     | t -> t
-  in 
+  in
     aux t
 ;;
 
@@ -1105,24 +1105,24 @@ let get_candidates ?(smart=true) ~pfailed depth flags status cache _signature gt
   let _,_,metasenv,subst,_ = status#obj in
   let context = ctx_of gty in
   let _, raw_gty = term_of_cic_term status gty context in
-  let is_prod, _is_eq =   
-    let status, t = term_of_cic_term status gty context  in 
+  let is_prod, _is_eq =
+    let status, t = term_of_cic_term status gty context  in
     let t = NCicReduction.whd status subst context t in
       match t with
         | NCic.Prod _ -> true, false
-        | _ -> false, NCicParamod.is_equation status metasenv subst context t 
+        | _ -> false, NCicParamod.is_equation status metasenv subst context t
   in
-  debug_print ~depth (lazy ("gty:" ^ NTacStatus.ppterm status gty));
-  let is_eq = 
-    NCicParamod.is_equation status metasenv subst context raw_gty 
+  !debug_print ~depth (lazy ("gty:" ^ NTacStatus.ppterm status gty));
+  let is_eq =
+    NCicParamod.is_equation status metasenv subst context raw_gty
   in
   let raw_weak_gty, weak_gty  =
     if smart then
       match raw_gty with
-        | NCic.Appl _ 
-        | NCic.Const _ 
-        | NCic.Rel _ -> 
-            let raw_weak = 
+        | NCic.Appl _
+        | NCic.Const _
+        | NCic.Rel _ ->
+            let raw_weak =
               perforate_small status subst metasenv context raw_gty in
             let weak = mk_cic_term context raw_weak in
             noprint ~depth (lazy ("weak_gty:" ^ NTacStatus.ppterm status weak));
@@ -1132,23 +1132,23 @@ let get_candidates ?(smart=true) ~pfailed depth flags status cache _signature gt
   in
   (* we now compute global candidates *)
   let global_cands, smart_global_cands =
-  let mapf s = 
-    let to_ast = function 
-      | NCic.Const r when true 
+  let mapf s =
+    let to_ast = function
+      | NCic.Const r when true
            (*is_relevant statistics r*) -> Some (Ast.NRef r)
    (* | NCic.Const _ -> None  *)
       | _ -> assert false in
-        HExtlib.filter_map 
+        HExtlib.filter_map
           to_ast (NDiscriminationTree.TermSet.elements s) in
-    let g,l = 
+    let g,l =
       get_cands
         (NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe)
-        NDiscriminationTree.TermSet.diff 
+        NDiscriminationTree.TermSet.diff
         NDiscriminationTree.TermSet.empty
         raw_gty raw_weak_gty in
     mapf g, mapf l
-  in 
-  let global_cands,smart_global_cands = 
+  in
+  let global_cands,smart_global_cands =
       if flags.local_candidates then global_cands,smart_global_cands
       else let filter = List.filter (function Ast.NRef NReference.Ref (uri,_) -> is_a_needed_uri
                                                                                    (NUri.string_of_uri
@@ -1156,19 +1156,19 @@ let get_candidates ?(smart=true) ~pfailed depth flags status cache _signature gt
         in filter global_cands,filter smart_global_cands
   in
   (* we now compute local candidates *)
-  let local_cands,smart_local_cands = 
-    let mapf s = 
+  let local_cands,smart_local_cands =
+    let mapf s =
       let to_ast t =
-        let _status, t = term_of_cic_term status t context 
+        let _status, t = term_of_cic_term status t context
         in Ast.NCic t in
         List.map to_ast (Ncic_termSet.elements s) in
-    let g,l = 
+    let g,l =
       get_cands
         (fun ty -> search_in_th ty cache)
         Ncic_termSet.diff  Ncic_termSet.empty gty weak_gty in
       mapf g, mapf l
   in
-  let local_cands,smart_local_cands = 
+  let local_cands,smart_local_cands =
    if flags.local_candidates then local_cands,smart_local_cands
    else let filter = List.filter (function Ast.NRef NReference.Ref (uri,_) -> is_a_needed_uri
                                                                                 (NUri.string_of_uri
@@ -1189,25 +1189,25 @@ let get_candidates ?(smart=true) ~pfailed depth flags status cache _signature gt
     (* if the goal is an equation and paramodulation did not fail
      we avoid to apply unit equalities; refl is an
      exception since it prompts for convertibility *)
-    let l1 = if is_eq && (not pfailed) 
-      then [Ast.Ident("refl",None)] else gl1@ll1 in 
-    let l2 = 
+    let l1 = if is_eq && (not pfailed)
+      then [Ast.Ident("refl",None)] else gl1@ll1 in
+    let l2 =
       (* if smart given candidates are applied in smart mode *)
       if by && smart then ll2
-      else if by then given_candidates@ll2 
+      else if by then given_candidates@ll2
       else gl2@ll2
     in l1,l2
   in
   (* we now compute candidates to be applied in smart mode, splitted in
-     facts and not facts *) 
+     facts and not facts *)
   let smart_candidates_facts, smart_candidates_other =
-    if is_prod || not(smart) then [],[] 
-    else 
+    if is_prod || not(smart) then [],[]
+    else
     let sgl1,sgl2 = List.partition test smart_global_cands in
     let sll1,sll2 = List.partition test smart_local_cands in
     let l1 = if is_eq then [] else sgl1@sll1 in
-    let l2 = 
-      if by && smart then given_candidates@sll2 
+    let l2 =
+      if by && smart then given_candidates@sll2
       else if by then sll2
       else sgl2@sll2
     in l1,l2
@@ -1219,49 +1219,49 @@ let get_candidates ?(smart=true) ~pfailed depth flags status cache _signature gt
 ;;
 
 let applicative_case ~pfailed depth signature status flags gty cache =
-  app_counter:= !app_counter+1; 
+  app_counter:= !app_counter+1;
   let _,_,metasenv,subst,_ = status#obj in
   let context = ctx_of gty in
   let tcache = cache.facts in
-  let is_prod, is_eq =   
-    let status, t = term_of_cic_term status gty context  in 
+  let is_prod, is_eq =
+    let status, t = term_of_cic_term status gty context  in
     let t = NCicReduction.whd status subst context t in
       match t with
         | NCic.Prod _ -> true, false
-        | _ -> false, NCicParamod.is_equation status metasenv subst context t 
+        | _ -> false, NCicParamod.is_equation status metasenv subst context t
   in
-  debug_print ~depth (lazy (string_of_bool is_eq)); 
+  !debug_print ~depth (lazy (string_of_bool is_eq));
   (* new *)
-  let candidates_facts, smart_candidates_facts, 
-      candidates_other, smart_candidates_other = 
-    get_candidates ~smart:true ~pfailed depth 
-      flags status tcache signature gty 
+  let candidates_facts, smart_candidates_facts,
+      candidates_other, smart_candidates_other =
+    get_candidates ~smart:true ~pfailed depth
+      flags status tcache signature gty
   in
   let sm = if is_eq || is_prod then 0 else 2 in
   (*let sm1 = if flags.last then 2 else 0 in *)
-  let maxd = (depth + 1 = flags.maxdepth) in 
+  let maxd = (depth + 1 = flags.maxdepth) in
   let try_candidates only_one sm acc candidates =
-    List.fold_left 
+    List.fold_left
       (fun elems cand ->
-         if (only_one && (elems <> [])) then elems 
+         if (only_one && (elems <> [])) then elems
          else
            match try_candidate ~smart:sm
              flags depth status cache.unit_eq context cand with
                | None -> elems
                | Some x -> x::elems)
       acc candidates
-  in 
+  in
   (* if the goal is the last one we stop at the first fact *)
   let elems = try_candidates flags.last sm [] candidates_facts in
   (* now we add smart_facts *)
   let elems = try_candidates flags.last sm elems smart_candidates_facts in
-  (* if we are at maxdepth and the goal is not a product we are done 
+  (* if we are at maxdepth and the goal is not a product we are done
      similarly, if the goal is the last one and we already found a
      solution *)
   if (maxd && not(is_prod)) || (flags.last && elems<>[]) then elems
   else
     let elems = try_candidates false 2 elems candidates_other in
-    debug_print ~depth (lazy ("not facts: try smart application"));
+    !debug_print ~depth (lazy ("not facts: try smart application"));
     try_candidates false 2 elems smart_candidates_other
 ;;
 
@@ -1271,93 +1271,93 @@ exception Found
 (* gty is supposed to be meta-closed *)
 let is_subsumed depth filter_depth status gty cache =
   if cache=[] then false else (
-  debug_print ~depth (lazy("Subsuming " ^ (ppterm status gty))); 
+  !debug_print ~depth (lazy("Subsuming " ^ (ppterm status gty)));
   let n,h,metasenv,subst,obj = status#obj in
   let ctx = ctx_of gty in
   let _ , raw_gty = term_of_cic_term status gty ctx in
-  let target = NCicSubstitution.lift status 1 raw_gty in 
+  let target = NCicSubstitution.lift status 1 raw_gty in
   (* we compute candidates using the perforated type *)
   let weak_gty  =
     match target with
-      | NCic.Appl _ 
-      | NCic.Const _ 
-      | NCic.Rel _ -> 
-          let raw_weak = 
+      | NCic.Appl _
+      | NCic.Const _
+      | NCic.Rel _ ->
+          let raw_weak =
             perforate_small status subst metasenv ctx raw_gty in
           let weak = mk_cic_term ctx raw_weak in
-          debug_print ~depth (lazy ("weak_gty:" ^ NTacStatus.ppterm status weak));
+          !debug_print ~depth (lazy ("weak_gty:" ^ NTacStatus.ppterm status weak));
           Some (weak)
       | _ -> None
   in
   (* candidates must only be searched w.r.t the given context *)
-  let candidates = 
+  let candidates =
     try
     let idx = List.assq ctx cache in
     match weak_gty with
       | Some weak ->
-          Ncic_termSet.elements 
+          Ncic_termSet.elements
             (InvRelDiscriminationTree.retrieve_unifiables idx weak)
       |None -> []
     with Not_found -> []
   in
   (* this is a dirty trick: the first argument of an application is used
      to remember at which depth a goal failed *)
-  let filter t = 
-    let ctx = ctx_of t in 
-    let _, src = term_of_cic_term status t ctx in 
-    match src with 
-     | NCic.Appl [NCic.Implicit (`Typeof d); t] 
+  let filter t =
+    let ctx = ctx_of t in
+    let _, src = term_of_cic_term status t ctx in
+    match src with
+     | NCic.Appl [NCic.Implicit (`Typeof d); t]
        when d <= depth -> Some (mk_cic_term ctx t)
      | _ -> None in
-  let candidates = 
-    if filter_depth then HExtlib.filter_map filter candidates else candidates in  
-  debug_print ~depth
+  let candidates =
+    if filter_depth then HExtlib.filter_map filter candidates else candidates in
+  !debug_print ~depth
     (lazy ("failure candidates: " ^ string_of_int (List.length candidates)));
     try
       List.iter
         (fun t ->
            let _ , source = term_of_cic_term status t ctx in
-           let implication = 
+           let implication =
              NCic.Prod("foo",source,target) in
-           let metasenv,j,_,_ = 
-             NCicMetaSubst.mk_meta  
+           let metasenv,j,_,_ =
+             NCicMetaSubst.mk_meta
                metasenv ctx ~with_type:implication `IsType in
            let status = status#set_obj (n,h,metasenv,subst,obj) in
-           let status = status#set_stack [([1,Open j],[],[],`NoTag,[])] in 
+           let status = status#set_stack [([1,Open j],[],[],`NoTag,[])] in
            try
              let status = NTactics.intro_tac "foo" status in
              let status =
                NTactics.apply_tac ("",0,Ast.NCic (NCic.Rel 1)) status
-             in 
+             in
                if (head_goals status#stack = []) then raise Found
                else ()
            with
              | Error _ -> ())
         candidates;false
-    with Found -> debug_print ~depth (lazy "success");true)
+    with Found -> !debug_print ~depth (lazy "success");true)
 ;;
 
-let rec guess_name name ctx = 
+let rec guess_name name ctx =
   if name = "_" then guess_name "auto" ctx else
   if not (List.mem_assoc name ctx) then name else
   guess_name (name^"'") ctx
 ;;
 
-let is_prod status = 
+let is_prod status =
   let _, ctx, gty = current_goal status in
   let status, gty = apply_subst status ctx gty in
   let _, raw_gty = term_of_cic_term status gty ctx in
   match raw_gty with
     | NCic.Prod (name,src,_) ->
-        let status, src = whd status ~delta:0 ctx (mk_cic_term ctx src) in 
+        let status, src = whd status ~delta:0 ctx (mk_cic_term ctx src) in
         (match snd (term_of_cic_term status src ctx) with
-        | NCic.Const(NReference.Ref (_,NReference.Ind _) as r) 
+        | NCic.Const(NReference.Ref (_,NReference.Ind _) as r)
         | NCic.Appl (NCic.Const(NReference.Ref (_,NReference.Ind _) as r)::_) ->
             let _,_,itys,_,_ = NCicEnvironment.get_checked_indtys status r in
             (match itys with
             (* | [_,_,_,[_;_]]  con nat va, ovviamente, in loop *)
-            | [_,_,_,[_]] 
-            | [_,_,_,[]] -> `Inductive (guess_name name ctx)         
+            | [_,_,_,[_]]
+            | [_,_,_,[]] -> `Inductive (guess_name name ctx)
             | _ -> `Some (guess_name name ctx))
         | _ -> `Some (guess_name name ctx))
     | _ -> `None
@@ -1368,7 +1368,7 @@ let intro ~depth status facts name =
   let t = mk_cic_term ctx (NCic.Rel 1) in
   let status, keys = keys_of_term status t in
   let facts = List.fold_left (add_to_th t) facts keys in
-    debug_print ~depth (lazy ("intro: "^ name));
+    !debug_print ~depth (lazy ("intro: "^ name));
   (* unprovability is not stable w.r.t introduction *)
   status, facts
 ;;
@@ -1376,7 +1376,7 @@ let intro ~depth status facts name =
 let rec intros_facts ~depth status facts =
   if List.length (head_goals status#stack) <> 1 then status, facts else
   match is_prod status with
-    | `Inductive name 
+    | `Inductive name
     | `Some(name) ->
         let status,facts =
           intro ~depth status facts name
@@ -1385,7 +1385,7 @@ let rec intros_facts ~depth status facts =
           let status = NTactics.case1_tac name status in
           intros_facts ~depth status facts *)
     | _ -> status, facts
-;; 
+;;
 
 let intros ~depth status ?(use_given_only=false) cache =
     match is_prod status with
@@ -1393,22 +1393,22 @@ let intros ~depth status ?(use_given_only=false) cache =
       | `Some _ ->
           let trace = cache.trace in
           let status,facts =
-            intros_facts ~depth status cache.facts 
-          in 
-          if head_goals status#stack = [] then 
+            intros_facts ~depth status cache.facts
+          in
+          if head_goals status#stack = [] then
             let status = NTactics.merge_tac status in
             [(0,Ast.Ident("__intros",None)),status], cache
           else
             (* we reindex the equation from scratch *)
             let unit_eq = index_local_equations status#eq_cache status ~flag:use_given_only in
             let status = NTactics.merge_tac status in
-            [(0,Ast.Ident("__intros",None)),status], 
+            [(0,Ast.Ident("__intros",None)),status],
             init_cache ~facts ~unit_eq () ~trace
       | _ -> [],cache
 ;;
 
-let reduce ~whd ~depth status g = 
-  let n,h,metasenv,subst,o = status#obj in 
+let reduce ~whd ~depth status g =
+  let n,h,metasenv,subst,o = status#obj in
   let attr, ctx, ty = NCicUtils.lookup_meta g metasenv in
   let ty = NCicUntrusted.apply_subst status subst ctx ty in
   let ty' =
@@ -1416,10 +1416,10 @@ let reduce ~whd ~depth status g =
   in
   if ty = ty' then []
   else
-    (debug_print ~depth 
+    (!debug_print ~depth
       (lazy ("reduced to: "^ status#ppterm ctx subst metasenv ty'));
-    let metasenv = 
-      (g,(attr,ctx,ty'))::(List.filter (fun (i,_) -> i<>g) metasenv) 
+    let metasenv =
+      (g,(attr,ctx,ty'))::(List.filter (fun (i,_) -> i<>g) metasenv)
     in
     let status = status#set_obj (n,h,metasenv,subst,o) in
     (* we merge to gain a depth level; the previous goal level should
@@ -1433,7 +1433,7 @@ let is_meta status gty =
   let _, ty = term_of_cic_term status gty (ctx_of gty) in
   match ty with
   | NCic.Meta _ -> true
-  | _ -> false 
+  | _ -> false
 ;;
 
 let do_something signature flags status g depth gty ?(use_given_only=false) cache =
@@ -1441,10 +1441,10 @@ let do_something signature flags status g depth gty ?(use_given_only=false) cach
     thanks to the toplogical sorting of goals. *)
   if is_meta status gty then
     let t = Ast.Ident("I",None) in
-    debug_print (lazy ("using default term" ^ (NotationPp.pp_term status) t));
+    !debug_print (lazy ("using default term" ^ (NotationPp.pp_term status) t));
     let s = NTactics.apply_tac ("",0,t) status in
     [(0,t),s], cache
-  else 
+  else
   let l0, cache = intros ~depth status cache ~use_given_only in
   if l0 <> [] then l0, cache
   else
@@ -1452,43 +1452,43 @@ let do_something signature flags status g depth gty ?(use_given_only=false) cach
   let l = reduce ~whd:true ~depth status g in
   (* if l <> [] then l,cache else *)
   (* backward aplications *)
-  let l1 = 
-    List.map 
+  let l1 =
+    List.map
       (fun s ->
          incr candidate_no;
          ((!candidate_no,Ast.Ident("__paramod",None)),s))
-      (auto_eq_check cache.unit_eq status) 
+      (auto_eq_check cache.unit_eq status)
   in
-  let l2 = 
+  let l2 =
     if ((l1 <> []) && flags.last) then [] else
-    applicative_case ~pfailed:(l1=[]) depth signature status flags gty cache 
+    applicative_case ~pfailed:(l1=[]) depth signature status flags gty cache
   in
   (* statistics *)
-  List.iter 
+  List.iter
     (fun ((_,t),_) -> toref incr_nominations statistics t) l2;
   (* states in l1 have have an empty set of subgoals: no point to sort them *)
-  debug_print ~depth 
+  !debug_print ~depth
     (lazy ("alternatives = " ^ (string_of_int (List.length (l1@l@l2)))));
     (* we order alternatives w.r.t the number of subgoals they open *)
-    l1 @ (sort_new_elems l2) @ l, cache 
+    l1 @ (sort_new_elems l2) @ l, cache
 ;;
 
 let pp_goal = function
-  | (_,Continuationals.Stack.Open i) 
-  | (_,Continuationals.Stack.Closed i) -> string_of_int i 
+  | (_,Continuationals.Stack.Open i)
+  | (_,Continuationals.Stack.Closed i) -> string_of_int i
 ;;
 
 let pp_goals status l =
-  String.concat ", " 
-    (List.map 
-       (fun i -> 
+  String.concat ", "
+    (List.map
+       (fun i ->
           let gty = get_goalty status i in
             NTacStatus.ppterm status gty)
        l)
 ;;
 
-module M = 
-  struct 
+module M =
+  struct
     type t = int
     let compare = Stdlib.compare
   end
@@ -1498,31 +1498,31 @@ module MS = HTopoSort.Make(M)
 ;;
 
 let sort_tac status =
-  let gstatus = 
+  let gstatus =
     match status#stack with
     | [] -> assert false
     | (goals, t, k, tag, p) :: s ->
         let g = head_goals status#stack in
-        let sortedg = 
+        let sortedg =
           (List.rev (MS.topological_sort g (deps status))) in
-          noprint (lazy ("old g = " ^ 
+          noprint (lazy ("old g = " ^
             String.concat "," (List.map string_of_int g)));
-          noprint (lazy ("sorted goals = " ^ 
+          noprint (lazy ("sorted goals = " ^
             String.concat "," (List.map string_of_int sortedg)));
           let is_it i = function
-            | (_,Continuationals.Stack.Open j ) 
+            | (_,Continuationals.Stack.Open j )
             | (_,Continuationals.Stack.Closed j ) -> i = j
-          in 
-          let sorted_goals = 
+          in
+          let sorted_goals =
             List.map (fun i -> List.find (is_it i) goals) sortedg
           in
             (sorted_goals, t, k, tag, p) :: s
   in
    status#set_stack gstatus
 ;;
-  
+
 let clean_up_tac status =
-  let gstatus = 
+  let gstatus =
     match status#stack with
     | [] -> assert false
     | (g, t, k, tag, p) :: s ->
@@ -1537,12 +1537,12 @@ let clean_up_tac status =
 ;;
 
 let focus_tac focus status =
-  let gstatus = 
+  let gstatus =
     match status#stack with
     | [] -> assert false
     | (g, t, k, tag) :: s ->
         let in_focus = function
-          | (_,Continuationals.Stack.Open i) 
+          | (_,Continuationals.Stack.Open i)
           | (_,Continuationals.Stack.Closed i) -> List.mem i focus
         in
         let focus,others = List.partition in_focus g
@@ -1555,20 +1555,20 @@ let focus_tac focus status =
 
 let deep_focus_tac level focus status =
   let in_focus = function
-    | (_,Continuationals.Stack.Open i) 
+    | (_,Continuationals.Stack.Open i)
     | (_,Continuationals.Stack.Closed i) -> List.mem i focus
   in
-  let rec slice level gs = 
+  let rec slice level gs =
     if level = 0 then [],[],gs else
-      match gs with 
+      match gs with
         | [] -> assert false
         | (g, t, k, tag,p) :: s ->
-            let f,o,gs = slice (level-1) s in           
+            let f,o,gs = slice (level-1) s in
             let f1,o1 = List.partition in_focus g
             in
             (f1,[],[],`BranchTag, [])::f, (o1, t, k, tag, p)::o, gs
   in
-  let gstatus = 
+  let gstatus =
     let f,o,s = slice level status#stack in f@o@s
   in
    status#set_stack gstatus
@@ -1581,89 +1581,89 @@ match status#stack with
       let is_open = function
           | (_,Continuationals.Stack.Open i) -> Some i
           | (_,Continuationals.Stack.Closed _) -> None
-        in 
+        in
       let others = menv_closure status (stack_goals (level-1) tl) in
-      List.for_all (fun i -> IntSet.mem i others) 
+      List.for_all (fun i -> IntSet.mem i others)
         (HExtlib.filter_map is_open g)
 
 let top_cache ~depth:_ top status ?(use_given_only=false) cache =
   if top then
-    let unit_eq = index_local_equations status#eq_cache status ~flag:use_given_only in 
+    let unit_eq = index_local_equations status#eq_cache status ~flag:use_given_only in
     {cache with unit_eq = unit_eq}
   else cache
 
 let rec auto_clusters ?(top=false) flags signature cache depth ?(use_given_only=false) status : unit =
-  debug_print ~depth (lazy ("entering auto clusters at depth " ^
+  !debug_print ~depth (lazy ("entering auto clusters at depth " ^
                            (string_of_int depth)));
-  debug_print ~depth (pptrace status cache.trace);
+  !debug_print ~depth (pptrace status cache.trace);
   (* ignore(Unix.select [] [] [] 0.01); *)
   let status = clean_up_tac status in
   let goals = head_goals status#stack in
-  if goals = [] then 
+  if goals = [] then
     if depth = 0 then raise (Proved (status, cache.trace))
-    else 
+    else
       let status = NTactics.merge_tac status in
         let cache =
         let l,tree = cache.under_inspection in
-            match l with 
+            match l with
             | [] -> cache (* possible because of intros that cleans the cache *)
             | a::tl -> let tree = rm_from_th a tree a in
-              {cache with under_inspection = tl,tree} 
-        in 
+              {cache with under_inspection = tl,tree}
+        in
          auto_clusters flags signature cache (depth-1) status ~use_given_only
   else if List.length goals < 2 then
     let cache = top_cache ~depth top status cache ~use_given_only in
     auto_main flags signature cache depth status ~use_given_only
   else
     let all_goals = open_goals (depth+1) status in
-    debug_print ~depth (lazy ("goals = " ^ 
+    !debug_print ~depth (lazy ("goals = " ^
       String.concat "," (List.map string_of_int all_goals)));
     let classes = HExtlib.clusters (deps status) all_goals in
     (* if any of the classes exceed maxwidth we fail *)
     List.iter
       (fun gl ->
-         if List.length gl > flags.maxwidth then 
+         if List.length gl > flags.maxwidth then
            begin
-             debug_print ~depth (lazy "FAIL GLOBAL WIDTH"); 
+             !debug_print ~depth (lazy "FAIL GLOBAL WIDTH");
              HLog.warn (sprintf "global width (%u) exceeded: %u"
                flags.maxwidth (List.length gl));
              raise (Gaveup cache.failures)
            end else ()) classes;
     if List.length classes = 1 then
-      let flags = 
-        {flags with last = (List.length all_goals = 1)} in 
+      let flags =
+        {flags with last = (List.length all_goals = 1)} in
         (* no need to cluster *)
       let cache = top_cache ~depth top status cache ~use_given_only in
         auto_main flags signature cache depth status ~use_given_only
     else
       let classes = if top then List.rev classes else classes in
-      debug_print ~depth
-        (lazy 
-           (String.concat "\n" 
+      !debug_print ~depth
+        (lazy
+           (String.concat "\n"
            (List.map
-             (fun l -> 
+             (fun l ->
                ("cluster:" ^ String.concat "," (List.map string_of_int l)))
            classes)));
       (* we now process each cluster *)
-      let status,cache,b = 
+      let status,cache,b =
         List.fold_left
           (fun (status,cache,b) gl ->
-             let flags = 
-               {flags with last = (List.length gl = 1)} in 
-             let lold = List.length status#stack in 
-              debug_print ~depth (lazy ("stack length = " ^ 
+             let flags =
+               {flags with last = (List.length gl = 1)} in
+             let lold = List.length status#stack in
+              !debug_print ~depth (lazy ("stack length = " ^
                         (string_of_int lold)));
              let fstatus = deep_focus_tac (depth+1) gl status in
              let cache = top_cache ~depth top fstatus cache ~use_given_only in
-             try 
-               debug_print ~depth (lazy ("focusing on" ^ 
+             try
+               !debug_print ~depth (lazy ("focusing on" ^
                               String.concat "," (List.map string_of_int gl)));
                auto_main flags signature cache depth fstatus ~use_given_only; assert false
-             with 
-               | Proved(status,trace) -> 
+             with
+               | Proved(status,trace) ->
                    let status = NTactics.merge_tac status in
                    let cache = {cache with trace = trace} in
-                   let lnew = List.length status#stack in 
+                   let lnew = List.length status#stack in
                      assert (lold = lnew);
                    (status,cache,true)
                | Gaveup failures when top ->
@@ -1674,63 +1674,63 @@ let rec auto_clusters ?(top=false) flags signature cache depth ?(use_given_only=
       in
       let rec final_merge n s =
         if n = 0 then s else final_merge (n-1) (NTactics.merge_tac s)
-      in let status = final_merge depth status 
+      in let status = final_merge depth status
       in if b then raise (Proved(status,cache.trace)) else raise (Gaveup cache.failures)
 
 and
-        
-(* BRAND NEW VERSION *)         
+
+(* BRAND NEW VERSION *)
 auto_main flags signature cache depth ?(use_given_only=false) status: unit=
-  debug_print ~depth (lazy "entering auto main");
-  debug_print ~depth (pptrace status cache.trace);
-  debug_print ~depth (lazy ("stack length = " ^ 
+  !debug_print ~depth (lazy "entering auto main");
+  !debug_print ~depth (pptrace status cache.trace);
+  !debug_print ~depth (lazy ("stack length = " ^
                         (string_of_int (List.length status#stack))));
   (* ignore(Unix.select [] [] [] 0.01); *)
   let status = sort_tac (clean_up_tac status) in
   let goals = head_goals status#stack in
   match goals with
     | [] when depth = 0 -> raise (Proved (status,cache.trace))
-    | []  -> 
+    | []  ->
 	let status = NTactics.merge_tac status in
 	let cache =
 	  let l,tree = cache.under_inspection in
-	    match l with 
+	    match l with
 	      | [] -> cache (* possible because of intros that cleans the cache *)
 	      | a::tl -> let tree = rm_from_th a tree a in
-		  {cache with under_inspection = tl,tree} 
-	in 
+		  {cache with under_inspection = tl,tree}
+	in
 	  auto_clusters flags signature cache (depth-1) status ~use_given_only
     | _orig::_ ->
 	if depth > 0 && move_to_side depth status
-	then 
+	then
 	  let status = NTactics.merge_tac status in
 	  let cache =
 	    let l,tree = cache.under_inspection in
-	      match l with 
+	      match l with
 	        | [] -> cache (* possible because of intros that cleans the cache*)
 	        | a::tl -> let tree = rm_from_th a tree a in
-		    {cache with under_inspection = tl,tree} 
-	  in 
+		    {cache with under_inspection = tl,tree}
+	  in
 	    auto_clusters flags signature cache (depth-1) status ~use_given_only
 	else
         let ng = List.length goals in
         (* moved inside auto_clusters *)
-        if ng > flags.maxwidth then begin 
-          debug_print ~depth (lazy "FAIL LOCAL WIDTH");
+        if ng > flags.maxwidth then begin
+          !debug_print ~depth (lazy "FAIL LOCAL WIDTH");
           HLog.warn (sprintf "local width (%u) exceeded: %u"
              flags.maxwidth ng);
           raise (Gaveup cache.failures)
         end else if depth = flags.maxdepth then
           raise (Gaveup cache.failures)
-        else 
+        else
         let status = NTactics.branch_tac ~force:true status in
         let g,gctx, gty = current_goal status in
         let ctx,ty = close status g in
         let closegty = mk_cic_term ctx ty in
         let status, gty = apply_subst status gctx gty in
-        debug_print ~depth (lazy("Attacking goal " ^ 
+        !debug_print ~depth (lazy("Attacking goal " ^
           string_of_int g ^ " : "^ppterm status gty));
-        debug_print ~depth (lazy ("current failures: " ^ 
+        !debug_print ~depth (lazy ("current failures: " ^
           string_of_int (List.length (all_elements ctx cache.failures))));
         let is_eq =
            let _,_,metasenv,subst,_ = status#obj in
@@ -1740,65 +1740,65 @@ auto_main flags signature cache depth ?(use_given_only=false) status: unit=
         if (not flags.last && is_eq && (depth < (flags.maxdepth -2))) then
         (* for efficiency reasons, in this case we severely cripple the
            search depth *)
-          (debug_print ~depth (lazy ("RAISING DEPTH TO " ^ string_of_int (depth+1)));
+          (!debug_print ~depth (lazy ("RAISING DEPTH TO " ^ string_of_int (depth+1)));
            auto_main flags signature cache (depth+1) status ~use_given_only)
         (* check for loops *)
-        else if is_subsumed depth false status closegty (snd cache.under_inspection) then 
-          (debug_print ~depth (lazy "SUBSUMED");
+        else if is_subsumed depth false status closegty (snd cache.under_inspection) then
+          (!debug_print ~depth (lazy "SUBSUMED");
            raise (Gaveup cache.failures))
         (* check for failures *)
-        else if is_subsumed depth true status closegty cache.failures then 
-          (debug_print ~depth (lazy "ALREADY MET");
+        else if is_subsumed depth true status closegty cache.failures then
+          (!debug_print ~depth (lazy "ALREADY MET");
            raise (Gaveup cache.failures))
         else
         let new_sig = height_of_goal g status in
-        if new_sig < signature then 
-          (debug_print  ~depth (lazy ("news = " ^ (string_of_int new_sig)));
-           debug_print  ~depth (lazy ("olds = " ^ (string_of_int signature)))); 
-        let alternatives, cache = 
+        if new_sig < signature then
+          (!debug_print  ~depth (lazy ("news = " ^ (string_of_int new_sig)));
+           !debug_print  ~depth (lazy ("olds = " ^ (string_of_int signature))));
+        let alternatives, cache =
           do_something signature flags status g depth gty cache ~use_given_only in
         let loop_cache =
           if flags.last then
             let l,tree = cache.under_inspection in
             let l,tree = closegty::l, add_to_th closegty tree closegty in
             {cache with under_inspection = l,tree}
-          else cache in 
+          else cache in
         let failures =
-          List.fold_left  
+          List.fold_left
           (fun allfailures ((_,t),status) ->
-             debug_print ~depth 
-               (lazy ("(re)considering goal " ^ 
-                       (string_of_int g) ^" : "^ppterm status gty)); 
-             debug_print ~depth:depth
+             !debug_print ~depth
+               (lazy ("(re)considering goal " ^
+                       (string_of_int g) ^" : "^ppterm status gty));
+             !debug_print ~depth:depth
                (lazy ("Case: " ^ NotationPp.pp_term status t));
              let depth,cache =
-               if t=Ast.Ident("__whd",None) || 
-                  t=Ast.Ident("__intros",None) 
-               then depth, cache 
-               else depth+1,loop_cache in 
+               if t=Ast.Ident("__whd",None) ||
+                  t=Ast.Ident("__intros",None)
+               then depth, cache
+               else depth+1,loop_cache in
              let cache = add_to_trace status ~depth cache t in
              let cache = {cache with failures = allfailures} in
              try
                auto_clusters flags signature cache depth status ~use_given_only;
                assert false;
              with Gaveup fail ->
-               debug_print ~depth (lazy "Failed");
+               !debug_print ~depth (lazy "Failed");
                fail)
           cache.failures alternatives in
         let failures =
-          if flags.last then 
+          if flags.last then
             let newfail =
               let dty = NCic.Appl [NCic.Implicit (`Typeof depth); ty] in
-              mk_cic_term ctx dty 
-            in 
+              mk_cic_term ctx dty
+            in
             (*prerr_endline ("FAILURE : " ^ ppterm status gty);*)
             add_to_th newfail failures closegty
           else failures in
-        debug_print ~depth (lazy "no more candidates");
+        !debug_print ~depth (lazy "no more candidates");
         raise (Gaveup failures)
 ;;
 
-let int name l def = 
+let int name l def =
   try int_of_string (List.assoc name l)
   with Failure _ | Not_found -> def
 ;;
@@ -1807,14 +1807,14 @@ module AstSet = Set.Make(struct type t = Ast.term let compare = compare end)
 
 let cleanup_trace s trace =
   (* removing duplicates *)
-  let trace_set = 
-    List.fold_left 
+  let trace_set =
+    List.fold_left
       (fun acc t -> AstSet.add t acc)
       AstSet.empty trace in
   let trace = AstSet.elements trace_set
     (* filtering facts *)
-  in List.filter 
-       (fun t -> 
+  in List.filter
+       (fun t ->
           match t with
             | Ast.NRef (NReference.Ref (u,_)) -> not (is_a_fact_obj s u)
             | _ -> false) trace
@@ -1830,7 +1830,7 @@ let cleanup_trace s trace =
   diventano vuoti (ovvero: non usare automaticamente tutte le ipotesi, bensi'
   nessuna)
 
-- reimplementi la auto_params chiamando la auto_params' con il flag a 
+- reimplementi la auto_params chiamando la auto_params' con il flag a
   false e il vecchio codice per andare da parametri a candiddati
   OVVERO: usa tutti le ipotesi locali + candidati globali
 
@@ -1848,85 +1848,91 @@ let auto_tac' candidates ~local_candidates ?(use_given_only=false) flags ?(trace
   let goals = head_goals status#stack in
   let status, facts = mk_th_cache status goals in
 (*  let unit_eq = index_local_equations status#eq_cache status in *)
-  let cache = init_cache ~facts () in 
+  let cache = init_cache ~facts () in
 (*   pp_th status facts; *)
 (*
-  NDiscriminationTree.DiscriminationTree.iter status#auto_cache (fun p t -> 
-    debug_print (lazy(
+  NDiscriminationTree.DiscriminationTree.iter status#auto_cache (fun p t ->
+    !debug_print (lazy(
       NDiscriminationTree.NCicIndexable.string_of_path p ^ " |--> " ^
       String.concat "\n    " (List.map (
       status#ppterm ~metasenv:[] ~context:[] ~subst:[])
         (NDiscriminationTree.TermSet.elements t))
       )));
 *)
-  let depth = int "depth" flags 3 in 
-  let size  = int "size" flags 10 in 
-  let width = int "width" flags 4 (* (3+List.length goals)*) in 
+  let depth = int "depth" flags 3 in
+  let size  = int "size" flags 10 in
+  let width = int "width" flags 4 (* (3+List.length goals)*) in
+  let time  = int "time" flags 300 in
+  NCicParamod.time := float time;
+  Paramod.max_steps := int "steps" flags 2;
+  debug_print := if List.mem_assoc "debug" flags then print else noprint;
+
   (* XXX fix sort *)
 (*   let goals = List.map (fun i -> (i,P)) goals in *)
-  let signature = height_of_goals status in 
-  let flags = { 
+  let signature = height_of_goals status in
+  let flags = {
           last = true;
           candidates = candidates;
           local_candidates = local_candidates;
           maxwidth = width;
           maxsize = size;
           maxdepth = depth;
-          do_types = false; 
+          do_types = false;
   } in
   let initial_time = Unix.gettimeofday() in
   app_counter:= 0;
   let rec up_to x y =
     if x > y then
-      (debug_print(lazy
+      (!debug_print(lazy
         ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
-       debug_print(lazy
-        ("Applicative nodes:"^string_of_int !app_counter)); 
+       !debug_print(lazy
+        ("Applicative nodes:"^string_of_int !app_counter));
        raise (Error (lazy "auto gave up", None)))
     else
-      let _ = debug_print (lazy("\n\nRound "^string_of_int x^"\n")) in
-      let flags = { flags with maxdepth = x } 
-      in 
-        try auto_clusters ~top:true flags signature cache 0 status ~use_given_only;assert false 
+      let _ = !debug_print (lazy("\n\nRound "^string_of_int x^"\n")) in
+      let flags = { flags with maxdepth = x }
+      in
+        try auto_clusters ~top:true flags signature cache 0 status ~use_given_only;assert false
 (*
         try auto_main flags signature cache 0 status;assert false
 *)
         with
           | Gaveup _ -> up_to (x+1) y
-          | Proved (s,trace) -> 
-              debug_print (lazy ("proved at depth " ^ string_of_int x));
+          | Proved (s,trace) ->
+              !debug_print (lazy ("proved at depth " ^ string_of_int x));
               List.iter (toref incr_uses statistics) trace;
               let trace = cleanup_trace s trace in
-              let _ = debug_print (pptrace status trace) in
-              let stack = 
+              let _ = !debug_print (pptrace status trace) in
+              let stack =
                 match s#stack with
                   | (g,t,k,f,p) :: rest -> (filter_open g,t,k,f,p):: rest
                   | _ -> assert false
               in
               let s = s#set_stack stack in
                 trace_ref := trace;
-                oldstatus#set_status s 
+                oldstatus#set_status s
   in
   let s = up_to depth depth in
-    debug_print (print_stat status statistics);
-    debug_print(lazy
+    !debug_print (print_stat status statistics);
+    !debug_print(lazy
         ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
-    debug_print(lazy
+    !debug_print(lazy
         ("Applicative nodes:"^string_of_int !app_counter));
+    debug_print := noprint;
     s
 ;;
 
 let candidates_from_ctx univ ctx status =
     match univ with
-    | None -> None 
-    | Some l -> 
+    | None -> None
+    | Some l ->
         let to_Ast t =
-            (* FG: `XTSort here? *)                    
-            let status, res = disambiguate status ctx t `XTNone in 
-            let _,res = term_of_cic_term status res (ctx_of res) 
-            in Ast.NCic res 
+            (* FG: `XTSort here? *)
+            let status, res = disambiguate status ctx t `XTNone in
+            let _,res = term_of_cic_term status res (ctx_of res)
+            in Ast.NCic res
         in Some (List.map to_Ast l)
-(* FG: adding these lemmas to (List.map to_Ast l) slows auto very much in some cases 
+(* FG: adding these lemmas to (List.map to_Ast l) slows auto very much in some cases
                                     @ [Ast.Ident("refl",None); Ast.Ident("sym_eq",None);
                                        Ast.Ident("trans_eq",None); Ast.Ident("eq_f",None);
                                        Ast.Ident("eq_f2",None); Ast.Ident("eq_f3",None);
@@ -1937,7 +1943,7 @@ let candidates_from_ctx univ ctx status =
 let auto_lowtac ~params:(univ,flags) status goal =
     let gty = get_goalty status goal in
     let ctx = ctx_of gty in
-    let candidates = candidates_from_ctx univ ctx status in 
+    let candidates = candidates_from_ctx univ ctx status in
     auto_tac' candidates ~local_candidates:true ~use_given_only:false flags ~trace_ref:(ref [])
 
 let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status =
@@ -1945,11 +1951,11 @@ let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status =
     auto_tac' candidates ~local_candidates:true ~use_given_only:false flags ~trace_ref status
 
 let auto_tac ~params:(_,flags as params) ?trace_ref =
-  if List.mem_assoc "demod" flags then 
-    demod_tac ~params 
-  else if List.mem_assoc "paramod" flags then 
-    paramod_tac ~params 
-  else if List.mem_assoc "fast_paramod" flags then 
-    fast_eq_check_tac ~params  
+  if List.mem_assoc "demod" flags then
+    demod_tac ~params
+  else if List.mem_assoc "paramod" flags then
+    paramod_tac ~params
+  else if List.mem_assoc "fast_paramod" flags then
+    fast_eq_check_tac ~params
   else auto_tac ~params ?trace_ref
 ;;