Release 0.5.9.

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

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index a89bbd4a164b9e1c673b9ea9a7a0e2620788904d..973cc1d782433a91e3296b9022dc808b433eb1c7 100644 (file)
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/components/tactics/auto.ml
@@ -141,7 +141,7 @@ let is_an_equational_goal = function
   | _ -> false
 ;;
 
-type auto_params = Cic.term list option * (string * string) list 
+type auto_params = Cic.term list * (string * string) list 
 
 let elems = ref [] ;;
 
@@ -377,53 +377,52 @@ let init_cache_and_tables
            metasenv subst context t None)
       automation_cache ct
   in
-  match restricted_univ with
-    | None ->
-       let ct = 
-         if use_context then find_context_theorems context metasenv else [] 
-       in
-       let lt = 
-         match use_library, dbd with
-           | true, Some dbd -> find_library_theorems dbd metasenv goal 
-           | _ -> []
-       in
-       let cache = AutoCache.cache_empty in
-       let cache = cache_add_list cache context (ct@lt) in  
-       let automation_cache = 
-         add_list_to_tables metasenv subst automation_cache ct 
-       in
+  if restricted_univ = [] then
+    let ct = 
+      if use_context then find_context_theorems context metasenv else [] 
+    in
+    let lt = 
+      match use_library, dbd with
+      | true, Some dbd -> find_library_theorems dbd metasenv goal 
+      | _ -> []
+    in
+    let cache = AutoCache.cache_empty in
+    let cache = cache_add_list cache context (ct@lt) in  
+    let automation_cache = 
+      add_list_to_tables metasenv subst automation_cache ct 
+    in
 (*     AutomationCache.pp_cache automation_cache; *)
-         automation_cache.AutomationCache.univ, 
-       automation_cache.AutomationCache.tables, 
-       cache
-    | Some restricted_univ ->
-       let t_ty = 
-         List.map
-            (fun  t ->
-               let ty, _ = CicTypeChecker.type_of_aux' 
-                metasenv ~subst:[] context t CicUniv.oblivion_ugraph
-               in
-                t, ty)
-            restricted_univ
-       in
-         (* let automation_cache = AutomationCache.empty () in *) 
-       let automation_cache = 
-         let universe = Universe.empty in
-         let universe = 
-            Universe.index_list universe context t_ty
-         in
-           { automation_cache with AutomationCache.univ = universe }
-       in
-       let ct = 
-         if use_context then find_context_theorems context metasenv else t_ty
-       in
-       let automation_cache = 
-         add_list_to_tables metasenv subst automation_cache ct
-       in
+    automation_cache.AutomationCache.univ, 
+    automation_cache.AutomationCache.tables, 
+    cache
+  else
+    let t_ty = 
+      List.map
+        (fun  t ->
+          let ty, _ = CicTypeChecker.type_of_aux' 
+            metasenv ~subst:[] context t CicUniv.oblivion_ugraph
+          in
+            t, ty)
+        restricted_univ
+    in
+    (* let automation_cache = AutomationCache.empty () in *) 
+    let automation_cache = 
+      let universe = Universe.empty in
+      let universe = 
+        Universe.index_list universe context t_ty
+      in
+      { automation_cache with AutomationCache.univ = universe }
+    in
+    let ct = 
+     if use_context then find_context_theorems context metasenv else t_ty
+    in
+    let automation_cache = 
+      add_list_to_tables metasenv subst automation_cache ct
+    in
     (* AutomationCache.pp_cache automation_cache; *)
-         automation_cache.AutomationCache.univ, 
-       automation_cache.AutomationCache.tables, 
-       cache_empty
+    automation_cache.AutomationCache.univ, 
+    automation_cache.AutomationCache.tables, 
+    cache_empty
 ;;
 
 let fill_hypothesis context metasenv subst term tables (universe:Universe.universe) cache auto fast = 
@@ -957,7 +956,7 @@ let demodulate_tac ~dbd ~params:(_,flags as params) ~automation_cache =
 (***************** applyS *******************)
 
 let apply_smart_aux 
- dbd automation_cache (params:auto_params) proof goal newmeta' metasenv' subst
+ dbd automation_cache params proof goal newmeta' metasenv' subst
   context term' ty termty goal_arity 
 = 
  let consthead,newmetasenv,arguments,_ =
@@ -1674,7 +1673,7 @@ let try_smart_candidate dbd
 =
   let ppterm = ppterm context in
   try
-    let params = (None,[]) in
+    let params = ([],[]) in
     let automation_cache = { 
           AutomationCache.tables = tables ;
           AutomationCache.univ = Universe.empty; }
@@ -2130,20 +2129,17 @@ let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goa
   let _,metasenv,subst,_,_, _ = proof in
   let _,context,goalty = CicUtil.lookup_meta goal metasenv in
   let signature = MetadataQuery.signature_of metasenv goal in
-  let signature =
-    match univ with
-      | None -> signature
-      | Some l -> 
-         List.fold_left 
-           (fun set t ->
-               let ty, _ = 
-                CicTypeChecker.type_of_aux' metasenv context t 
-                  CicUniv.oblivion_ugraph
-              in
-                MetadataConstraints.UriManagerSet.union set 
-                  (MetadataConstraints.constants_of ty)
-           )
-           signature l
+  let signature = 
+    List.fold_left 
+      (fun set t ->
+         let ty, _ = 
+          CicTypeChecker.type_of_aux' metasenv context t 
+            CicUniv.oblivion_ugraph
+        in
+        MetadataConstraints.UriManagerSet.union set 
+          (MetadataConstraints.constants_of ty)
+       )
+      signature univ
   in
   let tables,cache =
     if flags.close_more then