X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FeliminationTactics.ml;h=5a293bcafcd4683661b077eee638a24d7992e971;hb=806ecbdd749ecf2a1cabff52b41cf748fe022401;hp=f18d2b333b68b322523b656db7db9527816c7324;hpb=acc9067d3263ffced81c52539f918d47d418d5c7;p=helm.git diff --git a/helm/software/components/tactics/eliminationTactics.ml b/helm/software/components/tactics/eliminationTactics.ml index f18d2b333..5a293bcaf 100644 --- 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