case tactic first tries with a simple outtype and then with a more sofisticated one

only if necessary since refine time may be long

diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml
index d6a6c91b9d8e60ad78d5b95fea237865869a37af..70b82092c8b16b688f186e7495d6104d67a56e3b 100644 (file)
--- a/helm/software/components/tactics/primitiveTactics.ml
+++ b/helm/software/components/tactics/primitiveTactics.ml
@@ -955,7 +955,7 @@ let cases_intros_tac ?(howmany=(-1)) ?(mk_fresh_name_callback = FreshNamesGenera
         right_args
     | _ -> assert false
   in
-  let outtype =
+  let outtypes =
     let n_right_args = List.length right_args in
     let n_lambdas = n_right_args + 1 in
     let lifted_ty = CicSubstitution.lift n_lambdas ty in
@@ -985,10 +985,11 @@ let cases_intros_tac ?(howmany=(-1)) ?(mk_fresh_name_callback = FreshNamesGenera
       if not !replaced then
         (* this means the matched term is not there, 
          * but maybe right params are: we user rels (to right args lambdas) *)
-        replace ~what ~with_what:(with_what false) ~where:captured
+        [replace ~what ~with_what:(with_what false) ~where:captured]
       else
         (* since the matched is there, rights should be inferrable *)
-        replace ~what ~with_what:(with_what true) ~where:captured
+        [replace ~what ~with_what:(with_what false) ~where:captured;
+         replace ~what ~with_what:(with_what true) ~where:captured]
     in
     let captured_term_ty = 
       let term_ty = CicSubstitution.lift n_right_args termty in
@@ -1003,38 +1004,46 @@ let cases_intros_tac ?(howmany=(-1)) ?(mk_fresh_name_callback = FreshNamesGenera
                fstn [] args paramsno @ mkrels n_right_args)
       | _ -> raise NotAnInductiveTypeToEliminate
     in
-    let rec add_lambdas = function
+    let rec add_lambdas captured_ty = function
       | 0 -> captured_ty
       | 1 -> 
-          C.Lambda (C.Name "matched", captured_term_ty, (add_lambdas 0))
+          C.Lambda (C.Name "matched", captured_term_ty, (add_lambdas captured_ty 0))
       | n -> 
            C.Lambda (C.Name ("right_"^(string_of_int (n-1))),
-                     C.Implicit None, (add_lambdas (n-1)))
+                     C.Implicit None, (add_lambdas captured_ty (n-1)))
     in
-    add_lambdas n_lambdas
+    List.map (fun x -> add_lambdas x n_lambdas) captured_ty
   in
-  let term_to_refine = C.MutCase (uri,typeno,outtype,term,patterns) in
-  let refined_term,_,metasenv'',_ = 
-    CicRefine.type_of_aux' metasenv' context term_to_refine
-      CicUniv.oblivion_ugraph
-  in
-  let new_goals =
-    ProofEngineHelpers.compare_metasenvs
-      ~oldmetasenv:metasenv ~newmetasenv:metasenv''
-  in
-  let proof' = curi,metasenv'',_subst,proofbo,proofty, attrs in
-  let proof'', new_goals' =
-    PET.apply_tactic (apply_tac ~term:refined_term) (proof',goal)
-  in
-  (* The apply_tactic can have closed some of the new_goals *)
-  let patched_new_goals =
-    let (_,metasenv''',_subst,_,_,_) = proof'' in
-      List.filter
-        (function i -> List.exists (function (j,_,_) -> j=i) metasenv''')
-        new_goals @ new_goals'
-    in
-    proof'', patched_new_goals
+  let rec first = (* easier than using tacticals *)
+  function 
+  | [] -> raise (PET.Fail (lazy ("unable to generate a working outtype")))
+  | outtype::rest -> 
+     let term_to_refine = C.MutCase (uri,typeno,outtype,term,patterns) in
+     try
+       let refined_term,_,metasenv'',_ = 
+         CicRefine.type_of_aux' metasenv' context term_to_refine
+           CicUniv.oblivion_ugraph
+       in
+       let new_goals =
+         ProofEngineHelpers.compare_metasenvs
+           ~oldmetasenv:metasenv ~newmetasenv:metasenv''
+       in
+       let proof' = curi,metasenv'',_subst,proofbo,proofty, attrs in
+         let proof'', new_goals' =
+           PET.apply_tactic (apply_tac ~term:refined_term) (proof',goal)
+         in
+         (* The apply_tactic can have closed some of the new_goals *)
+         let patched_new_goals =
+           let (_,metasenv''',_subst,_,_,_) = proof'' in
+             List.filter
+               (function i -> List.exists (function (j,_,_) -> j=i) metasenv''')
+               new_goals @ new_goals'
+         in
+         proof'', patched_new_goals
+     with PET.Fail _ | CicRefine.RefineFailure _ | CicRefine.Uncertain _ -> first rest
   in
+   first outtypes
+ in
    let reorder_pattern ((proof, goal) as status) =
      let _,metasenv,_,_,_,_ = proof in
      let conjecture = CicUtil.lookup_meta goal metasenv in