From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 26 Mar 2009 12:29:56 +0000 (+0000)
Subject: new apply almost there
X-Git-Tag: make_still_working~4136
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=42f25c258b0b199ee96dd8eaa3d44c86eb6916ab;p=helm.git

new apply almost there
---

diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index 018c5a44f..7593fe53a 100644
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/components/grafite/grafiteAst.ml
@@ -47,7 +47,8 @@ type 'term just =
  | `Auto of 'term auto_params ]
 
 type ntactic =
-   NApply of loc * CicNotationPt.term
+   | NApply of loc * CicNotationPt.term
+   | NId of loc
 
 type ('term, 'lazy_term, 'reduction, 'ident) tactic =
   (* Higher order tactics (i.e. tacticals) *)
@@ -189,7 +190,7 @@ type non_punctuation_tactical =
 type ('term, 'lazy_term, 'reduction, 'obj, 'ident) code =
   | Command of loc * ('term, 'obj) command
   | Macro of loc * ('term,'lazy_term) macro 
-  | NTactic of loc * ntactic option * punctuation_tactical
+  | NTactic of loc * ntactic * punctuation_tactical
   | Tactic of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic option
       * punctuation_tactical
   | NonPunctuationTactical of loc * non_punctuation_tactical
diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index a33bf6d9d..5785a1071 100644
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -91,6 +91,7 @@ let pp_just ~term_pp =
 
 let pp_ntactic ~map_unicode_to_tex = function
   | NApply (_,t) -> "napply " ^ CicNotationPp.pp_term t
+  | NId _ -> "nid"
 ;;
 
 let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =
@@ -368,11 +369,9 @@ let pp_executable ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp =
       ^ pp_punctuation_tactical punct
   | Tactic (_, None, punct) ->
      pp_punctuation_tactical punct
-  | NTactic (_,Some tac, punct) ->
+  | NTactic (_,tac, punct) ->
      pp_ntactic ~map_unicode_to_tex tac
      ^ pp_punctuation_tactical punct
-  | NTactic (_,None, punct) ->
-     pp_punctuation_tactical punct
   | NonPunctuationTactical (_, tac, punct) ->
      pp_non_punctuation_tactical tac
      ^ pp_punctuation_tactical punct
diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index b0df46ba3..0b87b40be 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -571,7 +571,24 @@ let eval_tactical status tac =
   status
 
 let add_obj = GrafiteSync.add_obj ~pack_coercion_obj:CicRefine.pack_coercion_obj
-      
+
+let eval_ng_punct (_text, _prefix_len, punct) =
+  match punct with
+  | GrafiteAst.Dot _ -> NTactics.dot_tac 
+  | GrafiteAst.Semicolon _ -> fun x -> x
+  | GrafiteAst.Branch _ -> NTactics.branch_tac 
+  | GrafiteAst.Shift _ -> NTactics.shift_tac 
+  | GrafiteAst.Pos (_,l) -> NTactics.pos_tac l
+  | GrafiteAst.Wildcard _ -> NTactics.wildcard_tac 
+  | GrafiteAst.Merge _ -> NTactics.merge_tac 
+;;
+
+let eval_ng_tac (text, prefix_len, tac) =
+  match tac with
+  | GrafiteAst.NApply (_loc, t) -> NTactics.apply_tac (text,prefix_len,t) 
+  | GrafiteAst.NId _ -> fun x -> x
+;;
+
 let rec eval_command = {ec_go = fun ~disambiguate_command opts status
 (text,prefix_len,cmd) ->
  let status,cmd = disambiguate_command status (text,prefix_len,cmd) in
@@ -672,18 +689,24 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
        | _ -> assert false
      in
      let suri = "cic:/ng_matita/" ^ name ^ ".def" in
+     let nlexicon_status =
+       match status.GrafiteTypes.ng_status with
+       | GrafiteTypes.ProofMode _ -> assert false
+       | GrafiteTypes.CommandMode ls -> ls
+     in
      let nmenv, nsubst, nlexicon_status, nty = 
        GrafiteDisambiguate.disambiguate_nterm None
-       LexiconEngine.initial_status [] [] [] (text,prefix_len,ty)
+       nlexicon_status [] [] [] (text,prefix_len,ty)
      in
      let nmenv, nsubst, nlexicon_status, nbo = 
        GrafiteDisambiguate.disambiguate_nterm (Some nty)
-       LexiconEngine.initial_status [] nmenv nsubst ("",0,CicNotationPt.Implicit)
+       nlexicon_status [] nmenv nsubst ("",0,CicNotationPt.Implicit)
      in
      let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
      prerr_endline ("nuovo lemma: " ^ NCicPp.ppmetasenv ~subst:nsubst nmenv);
      { status with
-        GrafiteTypes.ng_status = Some { NTactics.gstatus = ninitial_stack; 
+        GrafiteTypes.ng_status = 
+           GrafiteTypes.ProofMode { NTactics.gstatus = ninitial_stack; 
           istatus = { 
             NTactics.pstatus = 
              NUri.uri_of_string suri, 0, nmenv, nsubst, 
@@ -782,22 +805,14 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
   | GrafiteAst.Tactic (_, None, punct) ->
       eval_tactical status
        (punctuation_tactical_of_ast (text,prefix_len,punct)),[]
-  | GrafiteAst.NTactic (_(*loc*), Some (GrafiteAst.NApply (_loc, t)), punct) ->
+  | GrafiteAst.NTactic (_(*loc*), tac, punct) ->
       (match  status.GrafiteTypes.ng_status with
-      | None -> assert false
-      | Some status ->
-          let nts = NTactics.apply_tac (text,prefix_len,t) status in
-          prerr_endline "esco da apply";
-          NTactics.pp_tac_status nts;
-    (*
-     let tac = apply_tactic ~disambiguate_tactic (text,prefix_len,tac) in
-     let status = eval_tactical status (tactic_of_ast' tac) in
-      eval_tactical status
-       (punctuation_tactical_of_ast (text,prefix_len,punct)),[]
-     *) assert false)
-  | GrafiteAst.NTactic (_, None, _punct) -> assert false (*
-      eval_tactical status
-       (punctuation_tactical_of_ast (text,prefix_len,punct)),[] *)
+      | GrafiteTypes.CommandMode _ -> assert false
+      | GrafiteTypes.ProofMode nstatus ->
+         let nstatus = eval_ng_tac (text,prefix_len,tac) nstatus in
+         let nstatus = eval_ng_punct (text,prefix_len,punct) nstatus in
+         NTactics.pp_tac_status nstatus;
+         { status with GrafiteTypes.ng_status = GrafiteTypes.ProofMode nstatus }, [])
   | GrafiteAst.NonPunctuationTactical (_, tac, punct) ->
      let status = 
       eval_tactical status
diff --git a/helm/software/components/grafite_engine/grafiteSync.ml b/helm/software/components/grafite_engine/grafiteSync.ml
index 3fc67f2fd..5a746f41c 100644
--- a/helm/software/components/grafite_engine/grafiteSync.ml
+++ b/helm/software/components/grafite_engine/grafiteSync.ml
@@ -115,14 +115,14 @@ let time_travel ~present ~past =
   CoercDb.restore past.GrafiteTypes.coercions;
 ;;
 
-let initial_status baseuri = {
+let initial_status lexicon_status baseuri = {
     GrafiteTypes.moo_content_rev = [];
     proof_status = GrafiteTypes.No_proof;
     objects = [];
     coercions = CoercDb.empty_coerc_db;
     universe = Universe.empty;
     baseuri = baseuri;
-    ng_status = None;
+    ng_status = GrafiteTypes.CommandMode lexicon_status;
   }
 
 
diff --git a/helm/software/components/grafite_engine/grafiteSync.mli b/helm/software/components/grafite_engine/grafiteSync.mli
index be455ea1e..d15896dab 100644
--- a/helm/software/components/grafite_engine/grafiteSync.mli
+++ b/helm/software/components/grafite_engine/grafiteSync.mli
@@ -43,7 +43,7 @@ val time_travel:
 
   (* also resets the imperative part of the status 
    * init: the baseuri of the current script *)
-val init: string -> GrafiteTypes.status
+val init: LexiconEngine.status -> string -> GrafiteTypes.status
 
 (*
   (* just an empty status, does not reset imperative 
diff --git a/helm/software/components/grafite_engine/grafiteTypes.ml b/helm/software/components/grafite_engine/grafiteTypes.ml
index aa90dc0e0..836872779 100644
--- a/helm/software/components/grafite_engine/grafiteTypes.ml
+++ b/helm/software/components/grafite_engine/grafiteTypes.ml
@@ -44,6 +44,10 @@ type proof_status =
       (* Status in which the proof could be while it is being processed by the
       * engine. No status entering/exiting the engine could be in it. *)
 
+type ng_status =
+  | ProofMode of NTactics.tac_status
+  | CommandMode of LexiconEngine.status
+
 type status = {
   moo_content_rev: GrafiteMarshal.moo;
   proof_status: proof_status;
@@ -51,7 +55,7 @@ type status = {
   coercions: CoercDb.coerc_db;
   universe:Universe.universe;  
   baseuri: string;
-  ng_status: NTactics.tac_status option;
+  ng_status: ng_status;
 }
 
 let get_current_proof status =
diff --git a/helm/software/components/grafite_engine/grafiteTypes.mli b/helm/software/components/grafite_engine/grafiteTypes.mli
index 3a833f6da..b159a7fe6 100644
--- a/helm/software/components/grafite_engine/grafiteTypes.mli
+++ b/helm/software/components/grafite_engine/grafiteTypes.mli
@@ -42,14 +42,18 @@ type proof_status =
   | Proof of ProofEngineTypes.proof
   | Intermediate of Cic.metasenv
 
+type ng_status =
+  | ProofMode of NTactics.tac_status
+  | CommandMode of LexiconEngine.status
+
 type status = {
   moo_content_rev: GrafiteMarshal.moo;
-  proof_status: proof_status;                             (** logical status *)
-  objects: UriManager.uri list;  (** in-scope objects *)
+  proof_status: proof_status;
+  objects: UriManager.uri list;
   coercions: CoercDb.coerc_db;
-  universe:Universe.universe;  (** universe of terms used by auto *)
+  universe:Universe.universe;  
   baseuri: string;
-  ng_status: NTactics.tac_status option;
+  ng_status: ng_status;
 }
 
 val dump_status : status -> unit
diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 7fbd49968..b9c33232e 100644
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -744,7 +744,7 @@ EXTEND
         GrafiteAst.Tactic (loc, Some tac, punct)
     | punct = punctuation_tactical -> GrafiteAst.Tactic (loc, None, punct)
     | tac = ntactic; punct = punctuation_tactical ->
-        GrafiteAst.NTactic (loc, Some tac, punct)
+        GrafiteAst.NTactic (loc, tac, punct)
     | tac = non_punctuation_tactical; punct = punctuation_tactical ->
         GrafiteAst.NonPunctuationTactical (loc, tac, punct)
     | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac)
diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 492e55055..4ce980b28 100644
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -201,18 +201,30 @@ let fold_tactic tac status =
        { gstatus = stack; istatus = sn }
 ;;
 
+let compare_menv ~past ~present =
+  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)
+;;
 
 let apply t (status,goal) =
- let _,_,metasenv, subst,_ = status.pstatus in
- let _,context,gty = List.assoc goal metasenv in
+ let uri,height,(metasenv as old_metasenv), subst,obj = status.pstatus in
+ let name,context,gty = List.assoc goal metasenv in
  let metasenv, subst, lexicon_status, t = 
    GrafiteDisambiguate.disambiguate_nterm (Some gty) status.lstatus context metasenv subst t 
  in
+ let subst, metasenv = 
+   (goal, (name, context, t, gty)):: subst,
+   List.filter(fun (x,_) -> x <> goal) metasenv
+ in
+ let open_goals, closed_goals = compare_menv ~past:old_metasenv ~present:metasenv in
+ let new_pstatus = uri,height,metasenv,subst,obj in
+
    prerr_endline ("termine disambiguato: " ^ NCicPp.ppterm ~context ~metasenv ~subst t);
    prerr_endline ("menv:" ^ NCicPp.ppmetasenv ~subst metasenv);
    prerr_endline ("subst:" ^ NCicPp.ppsubst subst ~metasenv);
    prerr_endline "fine napply";
-   { status with lstatus = lexicon_status }, [goal], []
+
+  { lstatus = lexicon_status; pstatus = new_pstatus }, open_goals, closed_goals
 ;;
 
 let apply_tac t = fold_tactic (apply t) ;;
diff --git a/helm/software/matita/library/didactic/exercises/natural_deduction_fst_order.ma b/helm/software/matita/library/didactic/exercises/natural_deduction_fst_order.ma
index 9a865597b..dfecc3c13 100644
--- a/helm/software/matita/library/didactic/exercises/natural_deduction_fst_order.ma
+++ b/helm/software/matita/library/didactic/exercises/natural_deduction_fst_order.ma
@@ -193,7 +193,7 @@ apply rule (prove (¬(∀x.P x) ⇒ ∃x.¬ P x));
 apply rule (⇒_i [h1] (∃x.¬ P x));
 apply rule (RAA [h2] (⊥));
 apply rule (¬_e (¬(∀x.P x)) (∀x.P x));
-	[ apply rule (discharge [h1]);
+	[ apply rule (discharge [h2]);
 	| apply rule (∀_i {y} (P y));
     apply rule (RAA [h3] (⊥));
     apply rule (¬_e (¬∃x.¬ P x) (∃x.¬ P x));
diff --git a/helm/software/matita/matitaEngine.ml b/helm/software/matita/matitaEngine.ml
index a5331764e..128f33ac3 100644
--- a/helm/software/matita/matitaEngine.ml
+++ b/helm/software/matita/matitaEngine.ml
@@ -63,14 +63,34 @@ let eval_ast ?do_heavy_checks lexicon_status
 =
  let lexicon_status_ref = ref lexicon_status in
  let baseuri = GrafiteTypes.get_baseuri grafite_status in
+ let changed_lexicon = ref false in
+ let wrap f x = changed_lexicon := true; f x in
+ let grafite_status = 
+   match grafite_status.GrafiteTypes.ng_status with
+   | GrafiteTypes.CommandMode _ -> 
+      { grafite_status with GrafiteTypes.ng_status = 
+         GrafiteTypes.CommandMode lexicon_status }
+   | GrafiteTypes.ProofMode s -> 
+      { grafite_status with GrafiteTypes.ng_status = 
+         GrafiteTypes.ProofMode 
+          { s with NTactics.istatus = { s.NTactics.istatus with NTactics.lstatus =  lexicon_status }}}
+ in
  let new_grafite_status,new_objs =
   GrafiteEngine.eval_ast
-   ~disambiguate_tactic:(disambiguate_tactic text prefix_len lexicon_status_ref)
-   ~disambiguate_command:(disambiguate_command lexicon_status_ref)
-   ~disambiguate_macro:(disambiguate_macro lexicon_status_ref)
+   ~disambiguate_tactic:(wrap (disambiguate_tactic text prefix_len lexicon_status_ref))
+   ~disambiguate_command:(wrap (disambiguate_command lexicon_status_ref))
+   ~disambiguate_macro:(wrap (disambiguate_macro lexicon_status_ref))
    ?do_heavy_checks grafite_status (text,prefix_len,ast) in
+ let lexicon_status =
+  if !changed_lexicon then
+   !lexicon_status_ref
+  else
+   match new_grafite_status.GrafiteTypes.ng_status with
+   | GrafiteTypes.CommandMode l -> l
+   | GrafiteTypes.ProofMode s -> s.NTactics.istatus.NTactics.lstatus
+ in
  let new_lexicon_status =
-  LexiconSync.add_aliases_for_objs !lexicon_status_ref new_objs in
+  LexiconSync.add_aliases_for_objs lexicon_status new_objs in
  let new_aliases =
   LexiconSync.alias_diff ~from:lexicon_status new_lexicon_status in
  let _,intermediate_states = 
diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index 7768e2287..3ff2d0349 100644
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -675,7 +675,7 @@ let initial_statuses baseuri =
    CicNotation2.load_notation ~include_paths:[]
      BuildTimeConf.core_notation_script 
  in
- let grafite_status = GrafiteSync.init baseuri in
+ let grafite_status = GrafiteSync.init lexicon_status baseuri in
   grafite_status,lexicon_status
 in
 let read_include_paths file =
diff --git a/helm/software/matita/matitaWiki.ml b/helm/software/matita/matitaWiki.ml
index 87e9a4417..0fa8554ba 100644
--- a/helm/software/matita/matitaWiki.ml
+++ b/helm/software/matita/matitaWiki.ml
@@ -207,10 +207,10 @@ let main () =
   let system_mode =  Helm_registry.get_bool "matita.system" in
   let include_paths =
    Helm_registry.get_list Helm_registry.string "matita.includes" in
-  grafite_status := [GrafiteSync.init "cic:/matita/tests/"];
   lexicon_status :=
    [CicNotation2.load_notation ~include_paths
      BuildTimeConf.core_notation_script] ;
+  grafite_status := [GrafiteSync.init (List.hd !lexicon_status) "cic:/matita/tests/"];
   Sys.catch_break true;
   let origcb = HLog.get_log_callback () in
   let origcb t s = origcb t ((if system_mode then "[S] " else "") ^ s) in
diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml
index cfec1c507..e793a725b 100644
--- a/helm/software/matita/matitacLib.ml
+++ b/helm/software/matita/matitacLib.ml
@@ -193,11 +193,11 @@ let compile options fname =
     Librarian.baseuri_of_script ~include_paths fname in
   if Http_getter_storage.is_read_only baseuri then assert false;
   activate_extraction baseuri fname ;
-  let grafite_status = GrafiteSync.init baseuri in
   let lexicon_status = 
     CicNotation2.load_notation ~include_paths:[]
       BuildTimeConf.core_notation_script 
   in
+  let grafite_status = GrafiteSync.init lexicon_status baseuri in
   let big_bang = Unix.gettimeofday () in
   let { Unix.tms_utime = big_bang_u ; Unix.tms_stime = big_bang_s} = 
     Unix.times () 
diff --git a/helm/software/matita/tests/a.ma b/helm/software/matita/tests/a.ma
new file mode 100644
index 000000000..1061544d0
--- /dev/null
+++ b/helm/software/matita/tests/a.ma
@@ -0,0 +1,30 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+axiom A : Prop.
+axiom B : Prop.
+axiom C : Prop.
+axiom a: A.
+axiom b: B.
+
+
+notation "#" non associative with precedence 90 for @{ 'sharp }.
+interpretation "a" 'sharp = a.
+interpretation "b" 'sharp = b. 
+
+ntheorem prova : (A → B → C) → C.
+napply (λH.?);
+napply (H ? ?);
+napply #.
+nqed. 
\ No newline at end of file
diff --git a/helm/software/matita/tests/depends b/helm/software/matita/tests/depends
index b5507979b..77c709c70 100644
--- a/helm/software/matita/tests/depends
+++ b/helm/software/matita/tests/depends
@@ -1,334 +1,345 @@
-apply.ma coq.ma
-tinycals.ma logic/connectives.ma
-first.ma 
-coercions_propagation.ma logic/connectives.ma nat/orders.ma
-inversion2.ma coq.ma
-coercions_nonuniform.ma 
-clearbody.ma coq.ma
-coercions_open.ma logic/equality.ma nat/nat.ma
-compose.ma logic/equality.ma
-overred.ma logic/equality.ma
-hard_refine.ma coq.ma
-second.ma first.ma
-record.ma 
-mysql_escaping.ma 
-decompose.ma logic/connectives.ma
-fold.ma coq.ma
-generalize.ma coq.ma
-comments.ma coq.ma
-constructor.ma coq.ma
-clear.ma coq.ma
-bool.ma coq.ma
-coercions_russell.ma datatypes/bool.ma datatypes/constructors.ma list/list.ma list/sort.ma nat/compare.ma nat/orders.ma
-fix_betareduction.ma coq.ma
-contradiction.ma coq.ma
-test4.ma coq.ma
-multiple_inheritance.ma logic/equality.ma
-apply2.ma nat/nat.ma
-coercions_dependent.ma decidable_kit/list_aux.ma list/list.ma nat/nat.ma
-continuationals.ma coq.ma
-replace.ma coq.ma
-metasenv_ordering.ma coq.ma
-absurd.ma coq.ma
-demodulation_matita.ma nat/minus.ma
-coercions.ma nat/compare.ma nat/times.ma
-simpl.ma coq.ma
-unfold.ma coq.ma
-cut.ma coq.ma
-pullback.ma 
-destruct.ma datatypes/constructors.ma logic/equality.ma nat/nat.ma
-letrecand.ma nat/nat.ma
-bad_induction.ma logic/equality.ma nat/nat.ma
-assumption.ma coq.ma
-test3.ma coq.ma
-naiveparamod.ma logic/equality.ma
-decl.ma nat/orders.ma nat/times.ma
-tacticals.ma 
-applys.ma nat/div_and_mod.ma nat/factorial.ma nat/primes.ma
-match_inference.ma 
-third.ma first.ma second.ma
-letrec.ma 
-coercions_contravariant.ma logic/equality.ma nat/nat.ma
-dependent_type_inference.ma nat/nat.ma
-change.ma coq.ma
-elim.ma coq.ma
-demodulation_coq.ma coq.ma
-test2.ma coq.ma
-coercions_dupelim.ma logic/equality.ma nat/nat.ma
-fguidi.ma coq.ma
-dependent_injection.ma coq.ma
-inversion.ma coq.ma
-paramodulation.ma coq.ma
-rewrite.ma coq.ma
-injection.ma coq.ma
-paramodulation/BOO075-1.ma 
-paramodulation/boolean_algebra.ma coq.ma
-paramodulation/group.ma coq.ma
-paramodulation/irratsqrt2.ma nat/minus.ma nat/times.ma
-TPTP/Veloci/GRP456-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP168-2.p.ma logic/equality.ma
-TPTP/Veloci/GRP547-1.p.ma logic/equality.ma
-TPTP/Veloci/LDA007-3.p.ma logic/equality.ma
-TPTP/Veloci/GRP188-2.p.ma logic/equality.ma
-TPTP/Veloci/GRP486-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP567-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP496-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP577-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP597-1.p.ma logic/equality.ma
-TPTP/Veloci/COL010-1.p.ma logic/equality.ma
-TPTP/Veloci/LCL141-1.p.ma logic/equality.ma
-TPTP/Veloci/COL050-1.p.ma logic/equality.ma
-TPTP/Veloci/LCL161-1.p.ma logic/equality.ma
-TPTP/Veloci/ROB010-1.p.ma logic/equality.ma
-TPTP/Veloci/BOO011-4.p.ma logic/equality.ma
+TPTP/Veloci/GRP570-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP595-1.p.ma logic/equality.ma
+dependent_guarded_bove_capretta.ma nat/nat.ma
+interactive/test5.ma 
 TPTP/Veloci/SYN083-1.p.ma logic/equality.ma
 TPTP/Veloci/COL008-1.p.ma logic/equality.ma
-TPTP/Veloci/ROB030-1.p.ma logic/equality.ma
-TPTP/Veloci/COL018-1.p.ma logic/equality.ma
-TPTP/Veloci/COL062-3.p.ma logic/equality.ma
-TPTP/Veloci/LCL139-1.p.ma logic/equality.ma
-TPTP/Veloci/BOO017-2.p.ma logic/equality.ma
-TPTP/Veloci/COL048-1.p.ma logic/equality.ma
-TPTP/Veloci/BOO009-4.p.ma logic/equality.ma
-TPTP/Veloci/COL064-5.p.ma logic/equality.ma
-TPTP/Veloci/GRP010-4.p.ma logic/equality.ma
-TPTP/Veloci/GRP142-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP152-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP162-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP182-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP192-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP604-1.p.ma logic/equality.ma
+record.ma 
 TPTP/Veloci/GRP516-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP455-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP546-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP556-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP485-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP566-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP495-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP576-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP586-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP596-1.p.ma logic/equality.ma
-TPTP/Veloci/LCL140-1.p.ma logic/equality.ma
-TPTP/Veloci/BOO001-1.p.ma logic/equality.ma
-TPTP/Veloci/LCL115-2.p.ma logic/equality.ma
-TPTP/Veloci/BOO010-4.p.ma logic/equality.ma
-TPTP/Veloci/COL007-1.p.ma logic/equality.ma
-TPTP/Veloci/COL017-1.p.ma logic/equality.ma
-TPTP/Veloci/BOO006-2.p.ma logic/equality.ma
-TPTP/Veloci/COL061-3.p.ma logic/equality.ma
-TPTP/Veloci/BOO071-1.p.ma logic/equality.ma
-TPTP/Veloci/BOO016-2.p.ma logic/equality.ma
-TPTP/Veloci/COL064-2.p.ma logic/equality.ma
-TPTP/Veloci/LCL158-1.p.ma logic/equality.ma
-TPTP/Veloci/COL063-5.p.ma logic/equality.ma
-TPTP/Veloci/BOO018-4.p.ma logic/equality.ma
-TPTP/Veloci/LAT039-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP141-1.p.ma logic/equality.ma
-TPTP/Veloci/BOO069-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP151-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP161-1.p.ma logic/equality.ma
-TPTP/Veloci/RNG024-7.p.ma logic/equality.ma
-TPTP/Veloci/GRP515-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP606-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP454-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP139-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP616-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP149-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP545-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP176-2.p.ma logic/equality.ma
-TPTP/Veloci/GRP159-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP484-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP565-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP494-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP189-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP595-1.p.ma logic/equality.ma
-TPTP/Veloci/LCL114-2.p.ma logic/equality.ma
-TPTP/Veloci/COL016-1.p.ma logic/equality.ma
-TPTP/Veloci/LAT040-1.p.ma logic/equality.ma
-TPTP/Veloci/BOO005-2.p.ma logic/equality.ma
 TPTP/Veloci/COL060-3.p.ma logic/equality.ma
-TPTP/Veloci/COL063-2.p.ma logic/equality.ma
+TPTP/Veloci/COL016-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP612-1.p.ma logic/equality.ma
+TPTP/Veloci/COL024-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP139-1.p.ma logic/equality.ma
+TPTP/Veloci/BOO006-2.p.ma logic/equality.ma
+TPTP/Veloci/ROB010-1.p.ma logic/equality.ma
 TPTP/Veloci/LCL157-1.p.ma logic/equality.ma
-TPTP/Veloci/LAT008-1.p.ma logic/equality.ma
-TPTP/Veloci/COL086-1.p.ma logic/equality.ma
-TPTP/Veloci/COL058-3.p.ma logic/equality.ma
-TPTP/Veloci/RNG011-5.p.ma logic/equality.ma
-TPTP/Veloci/COL064-7.p.ma logic/equality.ma
-TPTP/Veloci/GRP150-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP160-1.p.ma logic/equality.ma
-TPTP/Veloci/RNG023-7.p.ma logic/equality.ma
-TPTP/Veloci/GRP118-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP514-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP605-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP615-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP182-3.p.ma logic/equality.ma
-TPTP/Veloci/GRP463-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP544-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP158-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP168-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP564-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP493-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP574-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP188-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP584-1.p.ma logic/equality.ma
-TPTP/Veloci/LCL113-2.p.ma logic/equality.ma
-TPTP/Veloci/COL015-1.p.ma logic/equality.ma
-TPTP/Veloci/BOO004-2.p.ma logic/equality.ma
-TPTP/Veloci/COL025-1.p.ma logic/equality.ma
-TPTP/Veloci/COL045-1.p.ma logic/equality.ma
-TPTP/Veloci/COL062-2.p.ma logic/equality.ma
-TPTP/Veloci/LCL156-1.p.ma logic/equality.ma
-TPTP/Veloci/BOO006-4.p.ma logic/equality.ma
-TPTP/Veloci/COL085-1.p.ma logic/equality.ma
-TPTP/Veloci/COL064-4.p.ma logic/equality.ma
-TPTP/Veloci/GRP023-2.p.ma logic/equality.ma
-TPTP/Veloci/GRP117-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP513-1.p.ma logic/equality.ma
-TPTP/Veloci/LDA001-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP604-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP137-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP614-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP543-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP157-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP492-1.p.ma logic/equality.ma
+TPTP/Veloci/LCL132-1.p.ma logic/equality.ma
+constructor.ma coq.ma
+TPTP/Veloci/GRP565-1.p.ma logic/equality.ma
+elim.ma coq.ma
+TPTP/Veloci/GRP155-1.p.ma logic/equality.ma
+TPTP/Veloci/BOO004-4.p.ma logic/equality.ma
+TPTP/Veloci/LCL140-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP598-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP573-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP583-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP186-4.p.ma logic/equality.ma
+TPTP/Veloci/GRP485-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP460-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP188-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP163-1.p.ma logic/equality.ma
+TPTP/Veloci/BOO012-4.p.ma logic/equality.ma
+TPTP/Veloci/GRP581-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP493-1.p.ma logic/equality.ma
+TPTP/Veloci/COL063-3.p.ma logic/equality.ma
 TPTP/Veloci/LCL112-2.p.ma logic/equality.ma
-TPTP/Veloci/COL014-1.p.ma logic/equality.ma
-TPTP/Veloci/BOO003-2.p.ma logic/equality.ma
-TPTP/Veloci/COL024-1.p.ma logic/equality.ma
+formal_topology.ma logic/connectives.ma
+TPTP/Veloci/RNG023-7.p.ma logic/equality.ma
+replace.ma coq.ma
+test2.ma coq.ma
+TPTP/Veloci/COL064-7.p.ma logic/equality.ma
+TPTP/Veloci/BOO009-2.p.ma logic/equality.ma
+TPTP/Veloci/GRP510-1.p.ma logic/equality.ma
+TPTP/Veloci/COL010-1.p.ma logic/equality.ma
+TPTP/Veloci/BOO017-2.p.ma logic/equality.ma
 TPTP/Veloci/LCL135-1.p.ma logic/equality.ma
-TPTP/Veloci/BOO013-2.p.ma logic/equality.ma
 TPTP/Veloci/COL061-2.p.ma logic/equality.ma
-TPTP/Veloci/LCL155-1.p.ma logic/equality.ma
-TPTP/Veloci/BOO005-4.p.ma logic/equality.ma
+elim_pattern.ma nat/plus.ma
+assumption.ma coq.ma
+interactive/grafite.ma 
+TPTP/Veloci/GRP551-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP463-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP141-1.p.ma logic/equality.ma
+fix_betareduction.ma coq.ma
+TPTP/Veloci/GRP606-1.p.ma logic/equality.ma
+coercions_dependent.ma decidable_kit/list_aux.ma list/list.ma nat/nat.ma
+TPTP/Veloci/GRP584-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP518-1.p.ma logic/equality.ma
+paramodulation/boolean_algebra.ma coq.ma
+TPTP/Veloci/GRP496-1.p.ma logic/equality.ma
 TPTP/Veloci/COL084-1.p.ma logic/equality.ma
-TPTP/Veloci/COL063-4.p.ma logic/equality.ma
-TPTP/Veloci/GRP022-2.p.ma logic/equality.ma
-TPTP/Veloci/COL064-9.p.ma logic/equality.ma
+TPTP/Veloci/GRP174-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP614-1.p.ma logic/equality.ma
+TPTP/Veloci/RNG011-5.p.ma logic/equality.ma
+inversion.ma coq.ma
+TPTP/Veloci/GRP592-1.p.ma logic/equality.ma
+bad_tests/baseuri.ma 
+TPTP/Veloci/GRP182-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP116-1.p.ma logic/equality.ma
+coercions.ma nat/compare.ma nat/times.ma
+TPTP/Veloci/GRP011-4.p.ma logic/equality.ma
+TPTP/Veloci/GRP149-1.p.ma logic/equality.ma
+TPTP/Veloci/COL013-1.p.ma logic/equality.ma
+TPTP/Veloci/COL064-2.p.ma logic/equality.ma
+TPTP/Veloci/GRP567-1.p.ma logic/equality.ma
+comments.ma coq.ma
+TPTP/Veloci/COL021-1.p.ma logic/equality.ma
+TPTP/Veloci/BOO006-4.p.ma logic/equality.ma
+TPTP/Veloci/BOO003-2.p.ma logic/equality.ma
+TPTP/Veloci/RNG024-6.p.ma logic/equality.ma
+bool.ma coq.ma
+TPTP/Veloci/BOO011-2.p.ma logic/equality.ma
+TPTP/Veloci/LCL154-1.p.ma logic/equality.ma
+TPTP/Veloci/LCL114-2.p.ma logic/equality.ma
+letrec.ma 
+TPTP/Veloci/BOO001-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP160-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP600-1.p.ma logic/equality.ma
+TPTP/Veloci/COL063-5.p.ma logic/equality.ma
 TPTP/Veloci/GRP512-1.p.ma logic/equality.ma
+continuationals.ma coq.ma
+TPTP/Veloci/GRP490-1.p.ma logic/equality.ma
+TPTP/Veloci/BOO034-1.p.ma logic/equality.ma
+fold.ma coq.ma
+TPTP/Veloci/GRP545-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP520-1.p.ma logic/equality.ma
+a.ma 
+TPTP/Veloci/GRP457-1.p.ma logic/equality.ma
+TPTP/Veloci/COL064-9.p.ma logic/equality.ma
+TPTP/Veloci/BOO009-4.p.ma logic/equality.ma
+TPTP/Veloci/LAT040-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP578-1.p.ma logic/equality.ma
+change.ma coq.ma
+TPTP/Veloci/GRP168-1.p.ma logic/equality.ma
+TPTP/Veloci/BOO075-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP143-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP586-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP561-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP498-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP176-1.p.ma logic/equality.ma
+overred.ma logic/equality.ma
+TPTP/Veloci/COL007-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP603-1.p.ma logic/equality.ma
-TPTP/Veloci/RNG024-6.p.ma logic/equality.ma
-TPTP/Veloci/GRP136-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP613-1.p.ma logic/equality.ma
+TPTP/Veloci/COL058-2.p.ma logic/equality.ma
+TPTP/Veloci/GRP515-1.p.ma logic/equality.ma
+TPTP/Veloci/COL015-1.p.ma logic/equality.ma
+TPTP/Veloci/RNG007-4.p.ma logic/equality.ma
+TPTP/Veloci/GRP548-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP182-3.p.ma logic/equality.ma
+TPTP/Veloci/COL048-1.p.ma logic/equality.ma
+TPTP/Veloci/BOO005-2.p.ma logic/equality.ma
+TPTP/Veloci/GRP189-2.p.ma logic/equality.ma
+TPTP/Veloci/GRP556-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP146-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP542-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP156-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP552-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP481-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP562-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP176-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP491-1.p.ma logic/equality.ma
+TPTP/Veloci/COL064-4.p.ma logic/equality.ma
+TPTP/Veloci/LCL156-1.p.ma logic/equality.ma
+contradiction.ma coq.ma
+TPTP/Veloci/GRP564-1.p.ma logic/equality.ma
+inversion2.ma coq.ma
+TPTP/Veloci/GRP154-1.p.ma logic/equality.ma
+TPTP/Veloci/ROB009-1.p.ma logic/equality.ma
+TPTP/Veloci/LCL164-1.p.ma logic/equality.ma
+TPTP/Veloci/BOO003-4.p.ma logic/equality.ma
+TPTP/Veloci/GRP597-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP572-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP582-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP592-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP459-1.p.ma logic/equality.ma
-TPTP/Veloci/COL013-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP484-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP162-1.p.ma logic/equality.ma
+fix_che_non_passa_ma_dovrebbe.ma list/list.ma nat/nat.ma
+TPTP/Veloci/BOO011-4.p.ma logic/equality.ma
+TPTP/Veloci/GRP580-1.p.ma logic/equality.ma
+TPTP/Veloci/COL062-3.p.ma logic/equality.ma
+TPTP/Veloci/GRP492-1.p.ma logic/equality.ma
+cut.ma coq.ma
+TPTP/Veloci/LAT034-1.p.ma logic/equality.ma
+TPTP/Veloci/COL018-1.p.ma logic/equality.ma
+tinycals.ma logic/connectives.ma
+coercions_contravariant.ma logic/equality.ma nat/nat.ma
+interactive/automatic_insertion.ma 
+clearbody.ma coq.ma
 TPTP/Veloci/LCL134-1.p.ma logic/equality.ma
-TPTP/Veloci/BOO012-2.p.ma logic/equality.ma
 TPTP/Veloci/COL060-2.p.ma logic/equality.ma
-TPTP/Veloci/LCL154-1.p.ma logic/equality.ma
-TPTP/Veloci/LCL164-1.p.ma logic/equality.ma
-TPTP/Veloci/BOO004-4.p.ma logic/equality.ma
-TPTP/Veloci/ROB013-1.p.ma logic/equality.ma
+TPTP/Veloci/BOO016-2.p.ma logic/equality.ma
+TPTP/Veloci/LAT039-2.p.ma logic/equality.ma
+TPTP/Veloci/GRP542-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP186-4.p.ma logic/equality.ma
+TPTP/Veloci/GRP454-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP157-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP509-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP550-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP487-1.p.ma logic/equality.ma
+paramodulation/BOO075-1.ma 
+TPTP/Veloci/GRP605-1.p.ma logic/equality.ma
+fguidi.ma logic/connectives.ma nat/nat.ma
+TPTP/Veloci/GRP583-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP517-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP173-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP495-1.p.ma logic/equality.ma
 TPTP/Veloci/COL083-1.p.ma logic/equality.ma
+coercions_propagation.ma logic/connectives.ma nat/orders.ma
 TPTP/Veloci/LAT045-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP001-2.p.ma logic/equality.ma
-TPTP/Veloci/BOO075-1.p.ma logic/equality.ma
-TPTP/Veloci/COL058-2.p.ma logic/equality.ma
+TPTP/Veloci/GRP558-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP010-4.p.ma logic/equality.ma
+interactive/test_instance.ma 
+TPTP/Veloci/COL012-1.p.ma logic/equality.ma
+TPTP/Veloci/COL063-2.p.ma logic/equality.ma
+first.ma 
+TPTP/Veloci/COL045-1.p.ma logic/equality.ma
+TPTP/Veloci/BOO005-4.p.ma logic/equality.ma
+interactive/test7.ma 
+bad_induction.ma logic/equality.ma nat/nat.ma
+TPTP/Veloci/RNG023-6.p.ma logic/equality.ma
+color.ma logic/equality.ma nat/nat.ma
 TPTP/Veloci/COL064-6.p.ma logic/equality.ma
-TPTP/Veloci/GRP115-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP511-1.p.ma logic/equality.ma
+metasenv_ordering.ma coq.ma
+apply2.ma nat/nat.ma
+TPTP/Veloci/GRP608-1.p.ma logic/equality.ma
+TPTP/Veloci/BOO010-2.p.ma logic/equality.ma
+TPTP/Veloci/LCL153-1.p.ma logic/equality.ma
+pullback.ma logic/equality.ma
+TPTP/Veloci/COL086-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP151-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP616-1.p.ma logic/equality.ma
+TPTP/Veloci/LCL161-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP023-2.p.ma logic/equality.ma
 TPTP/Veloci/GRP206-1.p.ma logic/equality.ma
+decompose.ma logic/connectives.ma
+TPTP/Veloci/GRP481-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP118-1.p.ma logic/equality.ma
+generalize.ma coq.ma
+TPTP/Veloci/GRP511-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP192-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP569-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP544-1.p.ma logic/equality.ma
+dependent_type_inference.ma nat/nat.ma
+TPTP/Veloci/GRP456-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP159-1.p.ma logic/equality.ma
+TPTP/Veloci/ROB030-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP552-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP577-1.p.ma logic/equality.ma
+TPTP/Veloci/BOO013-2.p.ma logic/equality.ma
+rewrite.ma coq.ma
+bad_tests/auto.ma coq.ma
+TPTP/Veloci/GRP497-1.p.ma logic/equality.ma
+diabolic_fix.ma nat/nat.ma
+TPTP/Veloci/GRP001-2.p.ma logic/equality.ma
+test4.ma coq.ma
+clear.ma coq.ma
 TPTP/Veloci/GRP602-1.p.ma logic/equality.ma
-TPTP/Veloci/RNG023-6.p.ma logic/equality.ma
-TPTP/Veloci/GRP612-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP514-1.p.ma logic/equality.ma
+TPTP/Veloci/LCL139-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP547-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP137-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP459-1.p.ma logic/equality.ma
+TPTP/Veloci/BOO069-1.p.ma logic/equality.ma
+TPTP/Veloci/COL004-3.p.ma logic/equality.ma
+TPTP/Veloci/GRP188-2.p.ma logic/equality.ma
+apply.ma coq.ma
+TPTP/Veloci/GRP467-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP145-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP460-1.p.ma logic/equality.ma
+TPTP/Veloci/LCL155-1.p.ma logic/equality.ma
+TPTP/Veloci/COL063-4.p.ma logic/equality.ma
+TPTP/Veloci/GRP588-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP153-1.p.ma logic/equality.ma
+paramodulation.ma coq.ma
+TPTP/Veloci/GRP596-1.p.ma logic/equality.ma
+coercions_nonuniform.ma 
+TPTP/Veloci/GRP161-1.p.ma logic/equality.ma
+TPTP/Veloci/COL064-8.p.ma logic/equality.ma
+TPTP/Veloci/LDA001-1.p.ma logic/equality.ma
+TPTP/Veloci/COL050-1.p.ma logic/equality.ma
+TPTP/Veloci/BOO010-4.p.ma logic/equality.ma
+TPTP/Veloci/LCL110-2.p.ma logic/equality.ma
+TPTP/Veloci/GRP491-1.p.ma logic/equality.ma
+TPTP/Veloci/COL061-3.p.ma logic/equality.ma
+TPTP/Veloci/COL017-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP613-1.p.ma logic/equality.ma
+compose.ma logic/equality.ma
+TPTP/Veloci/COL025-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP115-1.p.ma logic/equality.ma
+unifhint.ma list/list.ma nat/nat.ma nat/plus.ma
+hard_refine.ma coq.ma
+letrecand.ma nat/nat.ma
+paramodulation/group.ma coq.ma
+TPTP/Veloci/LCL158-1.p.ma logic/equality.ma
+TPTP/Veloci/LCL133-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP566-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP541-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP155-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP551-1.p.ma logic/equality.ma
+decl.ma nat/orders.ma nat/times.ma
+TPTP/Veloci/GRP156-1.p.ma logic/equality.ma
+universe_inconsistency.ma 
+mysql_escaping.ma 
+TPTP/Veloci/LCL141-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP182-2.p.ma logic/equality.ma
-TPTP/Veloci/GRP561-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP490-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP509-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP581-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP458-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP549-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP488-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP569-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP498-1.p.ma logic/equality.ma
-TPTP/Veloci/LCL110-2.p.ma logic/equality.ma
+interactive/drop.ma 
+interactive/test6.ma 
 TPTP/Veloci/GRP599-1.p.ma logic/equality.ma
-TPTP/Veloci/COL012-1.p.ma logic/equality.ma
-TPTP/Veloci/COL022-1.p.ma logic/equality.ma
-TPTP/Veloci/LCL133-1.p.ma logic/equality.ma
-TPTP/Veloci/BOO011-2.p.ma logic/equality.ma
-TPTP/Veloci/COL004-3.p.ma logic/equality.ma
-TPTP/Veloci/LCL153-1.p.ma logic/equality.ma
-TPTP/Veloci/ROB002-1.p.ma logic/equality.ma
-TPTP/Veloci/BOO003-4.p.ma logic/equality.ma
-TPTP/Veloci/BOO034-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP574-1.p.ma logic/equality.ma
+TPTP/Veloci/LDA007-3.p.ma logic/equality.ma
+unfold.ma coq.ma
+TPTP/Veloci/GRP189-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP486-1.p.ma logic/equality.ma
+TPTP/Veloci/BOO071-1.p.ma logic/equality.ma
 TPTP/Veloci/BOO013-4.p.ma logic/equality.ma
-TPTP/Veloci/LAT034-1.p.ma logic/equality.ma
-TPTP/Veloci/BOO009-2.p.ma logic/equality.ma
+TPTP/Veloci/GRP582-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP494-1.p.ma logic/equality.ma
 TPTP/Veloci/COL064-3.p.ma logic/equality.ma
-TPTP/Veloci/COL063-6.p.ma logic/equality.ma
-TPTP/Veloci/LAT039-2.p.ma logic/equality.ma
-TPTP/Veloci/GRP012-4.p.ma logic/equality.ma
-TPTP/Veloci/GRP510-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP520-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP144-1.p.ma logic/equality.ma
+TPTP/Veloci/LCL113-2.p.ma logic/equality.ma
 TPTP/Veloci/RNG008-4.p.ma logic/equality.ma
-TPTP/Veloci/GRP154-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP550-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP560-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP174-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP570-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP580-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP518-1.p.ma logic/equality.ma
+demodulation_matita.ma nat/minus.ma
+TPTP/Veloci/ROB002-1.p.ma logic/equality.ma
+tacticals.ma 
+TPTP/Veloci/GRP001-4.p.ma logic/equality.ma
 TPTP/Veloci/GRP590-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP457-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP549-1.p.ma logic/equality.ma
+applys.ma nat/div_and_mod.ma nat/factorial.ma nat/primes.ma
+TPTP/Veloci/RNG024-7.p.ma logic/equality.ma
+injection.ma coq.ma
+second.ma first.ma
+TPTP/Veloci/COL062-2.p.ma logic/equality.ma
+match_inference.ma 
+unifhint_simple.ma logic/equality.ma
+simpl.ma coq.ma
+TPTP/Veloci/COL063-6.p.ma logic/equality.ma
+TPTP/Veloci/GRP142-1.p.ma logic/equality.ma
+third.ma first.ma second.ma
+TPTP/Veloci/GRP560-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP150-1.p.ma logic/equality.ma
+TPTP/Veloci/COL085-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP615-1.p.ma logic/equality.ma
+TPTP/Veloci/LAT039-1.p.ma logic/equality.ma
+luo.ma Z/times.ma logic/equality.ma
+TPTP/Veloci/GRP022-2.p.ma logic/equality.ma
 TPTP/Veloci/GRP186-3.p.ma logic/equality.ma
-TPTP/Veloci/GRP467-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP548-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP558-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP189-2.p.ma logic/equality.ma
-TPTP/Veloci/GRP487-1.p.ma logic/equality.ma
+coercions_russell.ma datatypes/bool.ma datatypes/constructors.ma list/list.ma list/sort.ma nat/compare.ma nat/orders.ma
+TPTP/Veloci/GRP117-1.p.ma logic/equality.ma
+multiple_inheritance.ma logic/equality.ma
+test3.ma coq.ma
+TPTP/Veloci/ROB013-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP168-2.p.ma logic/equality.ma
+TPTP/Veloci/GRP012-4.p.ma logic/equality.ma
+naiveparamod.ma logic/equality.ma
+TPTP/Veloci/GRP176-2.p.ma logic/equality.ma
+TPTP/Veloci/COL014-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP568-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP497-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP578-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP588-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP598-1.p.ma logic/equality.ma
-TPTP/Veloci/COL021-1.p.ma logic/equality.ma
-TPTP/Veloci/LCL132-1.p.ma logic/equality.ma
-TPTP/Veloci/BOO010-2.p.ma logic/equality.ma
-TPTP/Veloci/BOO012-4.p.ma logic/equality.ma
-TPTP/Veloci/LAT033-1.p.ma logic/equality.ma
-TPTP/Veloci/COL063-3.p.ma logic/equality.ma
-TPTP/Veloci/ROB009-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP001-4.p.ma logic/equality.ma
-TPTP/Veloci/GRP011-4.p.ma logic/equality.ma
-TPTP/Veloci/COL064-8.p.ma logic/equality.ma
-TPTP/Veloci/GRP600-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP143-1.p.ma logic/equality.ma
-TPTP/Veloci/RNG007-4.p.ma logic/equality.ma
-TPTP/Veloci/GRP153-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP163-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP173-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP517-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP543-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP455-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP158-1.p.ma logic/equality.ma
+TPTP/Veloci/COL022-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP576-1.p.ma logic/equality.ma
+TPTP/Veloci/BOO004-2.p.ma logic/equality.ma
+TPTP/Veloci/GRP488-1.p.ma logic/equality.ma
+TPTP/Veloci/COL058-3.p.ma logic/equality.ma
+dependent_injection.ma coq.ma
+TPTP/Veloci/BOO012-2.p.ma logic/equality.ma
+TPTP/Veloci/LCL115-2.p.ma logic/equality.ma
+absurd.ma coq.ma
 TPTP/Veloci/GRP182-4.p.ma logic/equality.ma
-TPTP/Veloci/GRP608-1.p.ma logic/equality.ma
-interactive/test_instance.ma 
-interactive/drop.ma 
-interactive/test5.ma 
-interactive/test6.ma 
-interactive/test7.ma 
-interactive/automatic_insertion.ma 
-interactive/grafite.ma 
-bad_tests/auto.ma coq.ma
-bad_tests/baseuri.ma 
+destruct.ma datatypes/constructors.ma logic/equality.ma nat/nat.ma
+TPTP/Veloci/COL064-5.p.ma logic/equality.ma
+TPTP/Veloci/GRP513-1.p.ma logic/equality.ma
+TPTP/Veloci/LAT033-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP546-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP136-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP458-1.p.ma logic/equality.ma
+coercions_open.ma logic/equality.ma nat/nat.ma
+paramodulation/irratsqrt2.ma nat/minus.ma nat/times.ma
+TPTP/Veloci/GRP144-1.p.ma logic/equality.ma
+TPTP/Veloci/BOO018-4.p.ma logic/equality.ma
+TPTP/Veloci/LAT008-1.p.ma logic/equality.ma
+demodulation_coq.ma coq.ma
+TPTP/Veloci/GRP562-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP152-1.p.ma logic/equality.ma
+Z/times.ma 
 coq.ma 
 datatypes/bool.ma 
 datatypes/constructors.ma 
@@ -343,5 +354,6 @@ nat/factorial.ma
 nat/minus.ma 
 nat/nat.ma 
 nat/orders.ma 
+nat/plus.ma 
 nat/primes.ma 
 nat/times.ma 
diff --git a/helm/software/matita/tests/unifhint.ma b/helm/software/matita/tests/unifhint.ma
index 42e9f6878..310512b5a 100644
--- a/helm/software/matita/tests/unifhint.ma
+++ b/helm/software/matita/tests/unifhint.ma
@@ -88,6 +88,18 @@ unification hint 0 (∀g:group.∀G:list (gcarr g).∀x.
       〚x,G〛 = V).
 *)
 
+include "nat/plus.ma".
+unification hint 0 (∀x,y.S x + y = S (x + y)).
+
+axiom T : nat → Prop.
+axiom F : ∀n,k.T (S (n + k)) → Prop. 
+lemma diverge: ∀k,k1.∀h:T (? + k).F ? k1 h. 
+    ?+k    = S(?+k1)
+    S?1 + k   S(?1+k1)
+    
+lemma test : ∀g:group.∀x,y:gcarr g. ∀h:P ? ((𝟙 * x) * (x^-1 * y)). 
+   start g ? ? h.
+
 lemma test : ∀g:group.∀x,y:gcarr g. ∀h:P ? ((𝟙 * x) * (x^-1 * y)). 
    start g ? ? h.