Elim generalized: the term to eliminate is now saturated (i.e. it is applied

to as many ? as needed to make its type become something different from a
product).

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 2b67b521f6d0e1ea1cc26f184237280abc48ab11..c43034f93dfd7f672ade503c0723e9474bd021ea 100644 (file)
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -455,6 +455,10 @@ let elim_tac ~term =
    let (curi,metasenv,proofbo,proofty) = proof in
    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
     let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in
+    let (termty,metasenv',arguments,fresh_meta) =
+     ProofEngineHelpers.saturate_term
+      (ProofEngineHelpers.new_meta_of_proof proof) metasenv context termty in
+    let term = if arguments = [] then term else Cic.Appl (term::arguments) in
     let uri,exp_named_subst,typeno,args =
      match termty with
         C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[])
@@ -472,7 +476,7 @@ let elim_tac ~term =
             name
         | _ -> assert false
       in
-      let ty_ty,_ = T.type_of_aux' metasenv context ty CicUniv.empty_ugraph in
+      let ty_ty,_ = T.type_of_aux' metasenv' context ty CicUniv.empty_ugraph in
       let ext =
        match ty_ty with
           C.Sort C.Prop -> "_ind"
@@ -486,7 +490,7 @@ let elim_tac ~term =
      in
       let eliminator_ref = C.Const (eliminator_uri,exp_named_subst) in
        let ety,_ = 
-         T.type_of_aux' metasenv context eliminator_ref CicUniv.empty_ugraph in
+         T.type_of_aux' metasenv' context eliminator_ref CicUniv.empty_ugraph in
         let rec find_args_no =
          function
             C.Prod (_,_,t) -> 1 + find_args_no t
@@ -504,7 +508,7 @@ let elim_tac ~term =
            C.Appl (eliminator_ref :: make_tl term (args_no - 1))
          in
           let metasenv', term_to_refine' =
-           CicMkImplicit.expand_implicits metasenv [] context term_to_refine in
+           CicMkImplicit.expand_implicits metasenv' [] context term_to_refine in
           let refined_term,_,metasenv'',_ = 
            CicRefine.type_of_aux' metasenv' context term_to_refine' 
              CicUniv.empty_ugraph