fixed auto when the context has some deleted hypothesis

[helm.git] / helm / ocaml / tactics / primitiveTactics.ml

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 06e83a125335ea218df3a3e25f2c02f197910397..b185d693cf14f02e086e89e07f19d7ca0642a0c3 100644 (file)
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -61,10 +61,13 @@ let lambda_abstract ?(howmany=(-1)) metasenv context newmeta ty mk_fresh_name =
          in
           (context',ty,C.LetIn(n,s,bo))
       | _ as t ->
-        let irl =
+        if howmany <= 0 then
+         let irl =
           CicMkImplicit.identity_relocation_list_for_metavariable context
-        in
-         context, t, (C.Meta (newmeta,irl))
+         in
+          context, t, (C.Meta (newmeta,irl))
+        else
+         raise (Fail "intro(s): not enough products or let-ins")
   in
    collect_context context howmany ty 
 
@@ -231,11 +234,11 @@ let
          [],[] -> []
        | uri::tl,[] ->
           let ty =
-           let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+            let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
               match o with
-                 C.Variable (_,_,ty,_,_) ->
-                   CicSubstitution.subst_vars !exp_named_subst_diff ty
-               | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
+                  C.Variable (_,_,ty,_,_) ->
+                    CicSubstitution.subst_vars !exp_named_subst_diff ty
+                | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
           in
 (* CSC: patch to generate ?1 : ?2 : Type in place of ?1 : Type to simulate ?1 :< Type
            (match ty with
@@ -246,7 +249,7 @@ let
                   let subst_item = uri,C.Meta (fresh_meta',[]) in
                    newmetasenvfragment :=
                     (fresh_meta,[],C.Sort (C.Type (CicUniv.fresh()))) ::
-                    (* TASSI: ?? *)
+                     (* TASSI: ?? *)
                      (fresh_meta',[],C.Meta (fresh_meta,[])) :: !newmetasenvfragment ;
                    exp_named_subst_diff := !exp_named_subst_diff @ [subst_item] ;
                    subst_item::(aux (tl,[]))
@@ -352,7 +355,7 @@ let apply_tac_verbose ~term (proof, goal) =
 (*    prerr_endline ("me: " ^ CicMetaSubst.ppmetasenv newmetasenv'' subst); *)
    let subst_in =
      (* if we just apply the subtitution, the type is irrelevant:
-             we may use Implicit, since it will be dropped *)
+              we may use Implicit, since it will be dropped *)
      CicMetaSubst.apply_subst ((metano,(context,bo',Cic.Implicit None))::subst)
    in
    let (newproof, newmetasenv''') = 
@@ -498,7 +501,6 @@ 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
-      (* TASSI: FIXME *)
     let uri,exp_named_subst,typeno,args =
      match termty with
         C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[])
@@ -509,7 +511,7 @@ let elim_tac ~term =
      let eliminator_uri =
       let buri = U.buri_of_uri uri in
       let name = 
-       let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+        let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
        match o with
           C.InductiveDefinition (tys,_,_,_) ->
            let (name,_,_,_) = List.nth tys typeno in
@@ -517,7 +519,6 @@ let elim_tac ~term =
         | _ -> assert false
       in
       let ty_ty,_ = T.type_of_aux' metasenv context ty CicUniv.empty_ugraph in
-       (* TASSI: FIXME *)
       let ext =
        match ty_ty with
           C.Sort C.Prop -> "_ind"
@@ -531,7 +532,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
@@ -550,9 +551,9 @@ let elim_tac ~term =
          in
           let metasenv', term_to_refine' =
            CicMkImplicit.expand_implicits metasenv [] context term_to_refine in
-          let refined_term,_,metasenv'',_ = (* TASSI: FIXME *)
+          let refined_term,_,metasenv'',_ = 
            CicRefine.type_of_aux' metasenv' context term_to_refine' 
-            CicUniv.empty_ugraph
+             CicUniv.empty_ugraph
           in
            let new_goals =
             ProofEngineHelpers.compare_metasenvs