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

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

diff --git a/helm/software/components/tactics/eliminationTactics.ml b/helm/software/components/tactics/eliminationTactics.ml
index f18d2b333b68b322523b656db7db9527816c7324..5a293bcafcd4683661b077eee638a24d7992e971 100644 (file)
--- a/helm/software/components/tactics/eliminationTactics.ml
+++ b/helm/software/components/tactics/eliminationTactics.ml
@@ -43,7 +43,7 @@ module PEH  = ProofEngineHelpers
 let premise_pattern what = None, [what, C.Implicit (Some `Hole)], None 
 
 let get_inductive_def uri =
-   match E.get_obj Un.empty_ugraph uri with
+   match E.get_obj Un.oblivion_ugraph uri with
       | C.InductiveDefinition (tys, _, lpsno, _), _ -> 
          lpsno, tys
       | _                                           -> assert false
@@ -70,7 +70,7 @@ let rec check_type sorts metasenv context t =
          let _, psno = PEH.split_with_whd ([], arity) in
          let not_relation = (lpsno = psno) in
          let not_recursive = is_not_recursive uri tyno tys in
-         let ty_ty, _ = TC.type_of_aux' metasenv context t Un.empty_ugraph in
+         let ty_ty, _ = TC.type_of_aux' metasenv context t Un.oblivion_ugraph in
          let sort = match PEH.split_with_whd (context, ty_ty) with
             | (_, C.Sort sort) ::_ , _ -> CicPp.ppsort sort
            | (_, C.Meta _) :: _, _    -> CicPp.ppsort (C.Type (Un.fresh ()))
@@ -91,7 +91,7 @@ let rec check_type sorts metasenv context t =
 let rec scan_tac ~old_context_length ~index ~tactic =
    let scan_tac status =
       let (proof, goal) = status in
-      let _, metasenv, _, _, _ = proof in
+      let _, metasenv, _subst, _, _, _ = proof in
       let _, context, _ = CicUtil.lookup_meta goal metasenv in
       let context_length = List.length context in
       let rec aux index =
@@ -111,7 +111,7 @@ let rec scan_tac ~old_context_length ~index ~tactic =
 let elim_clear_unfold_tac ~sorts ~mk_fresh_name_callback ~what =
    let elim_clear_unfold_tac status =
       let (proof, goal) = status in
-      let _, metasenv, _, _, _ = proof in
+      let _, metasenv, _subst, _, _, _ = proof in
       let _, context, _ = CicUtil.lookup_meta goal metasenv in
       let index, ty = PEH.lookup_type metasenv context what in
       let tac = 
@@ -155,11 +155,11 @@ let warn s = debug_print (lazy ("DECOMPOSE: " ^ (Lazy.force s)))
 
 (* roba seria ------------------------------------------------------------- *)
 
-let decompose_tac ?(sorts=[CicPp.ppsort C.Prop; CicPp.ppsort C.CProp]) 
+let decompose_tac ?(sorts=[CicPp.ppsort C.Prop; CicPp.ppsort (C.CProp (CicUniv.fresh ()))]) 
                   ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) () =
    let decompose_tac status =
       let (proof, goal) = status in
-      let _, metasenv,_,_, _ = proof in
+      let _, metasenv, _subst, _,_, _ = proof in
       let _, context, _ = CicUtil.lookup_meta goal metasenv in
       let tactic = elim_clear_unfold_tac ~sorts ~mk_fresh_name_callback in
       let old_context_length = List.length context in