Debugging code removed.

[helm.git] / components / tactics / auto.ml

diff --git a/components/tactics/auto.ml b/components/tactics/auto.ml
index 65087f8cbd14571035e856d22ecf389254098714..59e90e6daec19d7aaa6c9e2b4c27f7f61c86feda 100644 (file)
--- a/components/tactics/auto.ml
+++ b/components/tactics/auto.ml
@@ -192,7 +192,7 @@ let empty_tables =
 let init_cache_and_tables dbd use_library paramod universe (proof, goal) =
   (* the local cache in initially empty  *)
   let cache = AutoCache.cache_empty in
-  let _, metasenv, _, _ = proof in
+  let _, metasenv, _, _, _ = proof in
   let signature = MetadataQuery.signature_of metasenv goal in
   let newmeta = CicMkImplicit.new_meta metasenv [] in
   let _,context,_ = CicUtil.lookup_meta goal metasenv in
@@ -335,7 +335,7 @@ let build_equalities auto context metasenv tables universe cache newmeta equatio
 let close_more tables maxmeta context status auto universe cache =
   let (active,passive,bag) = tables in
   let proof, goalno = status in
-  let _, metasenv,_,_ = proof in  
+  let _, metasenv,_,_, _ = proof in  
   let signature = MetadataQuery.signature_of metasenv goalno in
   let equations = retrieve_equations signature universe cache context in
   let eqs_and_types =
@@ -368,7 +368,7 @@ let find_context_equalities
   let module C = Cic in
   let module S = CicSubstitution in
   let module T = CicTypeChecker in
-  let _,metasenv,_,_ = proof in
+  let _,metasenv,_,_, _ = proof in
   let newmeta = max (ProofEngineHelpers.new_meta_of_proof ~proof) maxmeta in
   (* if use_auto is true, we try to close the hypothesis of equational
     statements using auto; a naif, and probably wrong approach *)
@@ -435,8 +435,8 @@ let new_metasenv_and_unify_and_t
    match arguments with [] -> term' | _ -> Cic.Appl (term'::arguments) 
  in
  let proof',oldmetasenv =
-  let (puri,metasenv,pbo,pty) = proof in
-   (puri,newmetasenv,pbo,pty),metasenv
+  let (puri,metasenv,pbo,pty, attrs) = proof in
+   (puri,newmetasenv,pbo,pty, attrs),metasenv
  in
  let goal_for_paramod =
   match LibraryObjects.eq_URI () with
@@ -446,7 +446,7 @@ let new_metasenv_and_unify_and_t
  in
  let newmeta = CicMkImplicit.new_meta newmetasenv (*subst*) [] in
  let metasenv_for_paramod = (newmeta,context,goal_for_paramod)::newmetasenv in
- let proof'' = let uri,_,p,ty = proof' in uri,metasenv_for_paramod,p,ty in
+ let proof'' = let uri,_,p,ty, attrs = proof' in uri,metasenv_for_paramod,p,ty, attrs in
  let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
  let proof''',goals =
   ProofEngineTypes.apply_tactic
@@ -471,7 +471,7 @@ let new_metasenv_and_unify_and_t
  | Some (_,proof''''',_), active,passive,_  ->
      subst,proof''''',
      ProofEngineHelpers.compare_metasenvs ~oldmetasenv
-       ~newmetasenv:(let _,m,_,_ = proof''''' in m),  active, passive
+       ~newmetasenv:(let _,m,_,_, _ = proof''''' in m),  active, passive
 ;;
 
 let rec count_prods context ty =
@@ -483,7 +483,7 @@ let apply_smart ~dbd ~term ~subst ~universe ?tables flags (proof, goal) =
  let module T = CicTypeChecker in
  let module R = CicReduction in
  let module C = Cic in
-  let (_,metasenv,_,_) = proof in
+  let (_,metasenv,_,_, _) = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let newmeta = CicMkImplicit.new_meta metasenv subst in
    let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
@@ -653,7 +653,7 @@ let equational_case
        with 
          | None, active, passive, maxmeta -> 
              [], (active,passive,bag), cache, maxmeta, flags
-         | Some(subst',(_,metasenv,proof,_),open_goals),active,passive,maxmeta ->
+         | Some(subst',(_,metasenv,proof,_, _),open_goals),active,passive,maxmeta ->
              assert_subst_are_disjoint subst subst';
              let subst = subst@subst' in
              let open_goals = order_new_goals metasenv subst open_goals ppterm in
@@ -668,7 +668,7 @@ let equational_case
         assert (maxmeta >= maxm);
        let res' =
          List.map 
-           (fun subst',(_,metasenv,proof,_),open_goals ->
+           (fun subst',(_,metasenv,proof,_, _),open_goals ->
               assert_subst_are_disjoint subst subst';
               let subst = subst@subst' in
               let open_goals = order_new_goals metasenv subst open_goals ppterm in
@@ -702,7 +702,7 @@ let try_candidate
 =
   let ppterm = ppterm context in
   try 
-    let subst', ((_,metasenv,_,_), open_goals), maxmeta =
+    let subst', ((_,metasenv,_,_, _), open_goals), maxmeta =
       PrimitiveTactics.apply_with_subst 
         ~maxmeta:maxm ~term:cand ~subst (fake_proof,goalno) 
     in
@@ -863,7 +863,7 @@ let rec auto_main tables maxm context flags elems universe cache =
     | Notfound 
     | Failed_in _ when depth > 0 -> (* we have more depth now *)
         let cache = cache_add_underinspection cache goalty depth in
-        let fake_proof = None,metasenv,Cic.Meta(goalno,irl),goalty in
+        let fake_proof = None,metasenv,Cic.Meta(goalno,irl),goalty, [] in (* FG: attrs *)
         let elems, tables, cache, maxm, flags =
           if is_equational_case goalty flags then
             let elems,tables,cache,maxm1, flags =
@@ -1044,7 +1044,7 @@ let rec position_of i x = function
 let superposition_tac ~target ~table ~subterms_only ~demod_table status = 
   Saturation.reset_refs();
   let proof,goalno = status in 
-  let curi,metasenv,pbo,pty = proof in
+  let curi,metasenv,pbo,pty, attrs = proof in
   let metano,context,ty = CicUtil.lookup_meta goalno metasenv in
   let eq_uri,tty = eq_and_ty_of_goal ty in
   let env = (metasenv, context, CicUniv.empty_ugraph) in
@@ -1148,7 +1148,7 @@ let auto_tac ~(dbd:HMysql.dbd) ~params ~universe (proof, goal) =
         ~target ~table ~subterms_only ~demod_table (proof,goal)
   | false -> 
       (* this is the real auto *)
-      let _,metasenv,_,_ = proof in
+      let _,metasenv,_,_, _ = proof in
       let _,context,_ = CicUtil.lookup_meta goal metasenv in
       let flags = flags_of_params params () in
       (* just for testing *)
@@ -1162,7 +1162,7 @@ let auto_tac ~(dbd:HMysql.dbd) ~params ~universe (proof, goal) =
            tables newmeta context (proof, goal) auto_all_solutions universe cache 
        else tables,cache,newmeta in
       let initial_time = Unix.gettimeofday() in
-      let (_,oldmetasenv,_,_) = proof in
+      let (_,oldmetasenv,_,_, _) = proof in
       let elem = metasenv,[],[goal,flags.maxdepth,AutoTypes.P] in
       match auto_main tables newmeta context flags [elem] universe cache with
        | Success (metasenv,subst,_), tables,cache,_ -> 
@@ -1191,7 +1191,7 @@ let eq_of_goal = function
 
 (* DEMODULATE *)
 let demodulate_tac ~dbd ~universe (proof,goal)= 
-  let curi,metasenv,pbo,pty = proof in
+  let curi,metasenv,pbo,pty, attrs = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
   let initgoal = [], [], ty in
@@ -1218,7 +1218,7 @@ let demodulate_tac ~dbd ~universe (proof,goal)=
       in
         let extended_metasenv = (maxm,context,newty)::metasenv in
         let extended_status = 
-          (curi,extended_metasenv,pbo,pty),goal in
+          (curi,extended_metasenv,pbo,pty, attrs),goal in
         let (status,newgoals) = 
           ProofEngineTypes.apply_tactic 
             (PrimitiveTactics.apply_tac ~term:proofterm)