X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fauto.ml;h=973cc1d782433a91e3296b9022dc808b433eb1c7;hb=a90c31c1b53222bd6d57360c5ba5c2d0fe7d5207;hp=a89bbd4a164b9e1c673b9ea9a7a0e2620788904d;hpb=4377e950998c9c63937582952a79975947aa9a45;p=helm.git

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index a89bbd4a1..973cc1d78 100644
--- 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