X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2FfourierR.ml;h=8e443447a892f2a160fd7c724697698857a987b8;hb=b0a6c05decc9f0e731f70cfc5ae5350ae4046b79;hp=8b910bded8ebabe6c5695016930b4ef4325c721b;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git diff --git a/components/tactics/fourierR.ml b/components/tactics/fourierR.ml index 8b910bded..8e443447a 100644 --- a/components/tactics/fourierR.ml +++ b/components/tactics/fourierR.ml @@ -577,7 +577,7 @@ let tac_zero_inf_pos (n,d) = (*let cste = pf_parse_constr gl in*) let pall str (proof,goal) t = debug ("tac "^str^" :\n" ); - let curi,metasenv,pbo,pty = proof in + let curi,metasenv,_subst,pbo,pty, attrs = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in debug ("th = "^ CicPp.ppterm t ^"\n"); debug ("ty = "^ CicPp.ppterm ty^"\n"); @@ -675,7 +675,7 @@ let tac_zero_inf_false gl (n,d) = let tac_zero_infeq_false gl (n,d) = let tac_zero_infeq_false gl (n,d) status = let (proof, goal) = status in - let curi,metasenv,pbo,pty = proof in + let curi,metasenv,_subst,pbo,pty, attrs = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in debug("faccio fold di " ^ CicPp.ppterm @@ -713,13 +713,13 @@ let tac_zero_infeq_false gl (n,d) = let apply_type_tac ~cast:t ~applist:al = let apply_type_tac ~cast:t ~applist:al (proof,goal) = - let curi,metasenv,pbo,pty = proof in + let curi,metasenv,_subst,pbo,pty, attrs = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in let metasenv' = (fresh_meta,context,t)::metasenv in - let proof' = curi,metasenv',pbo,pty in + let proof' = curi,metasenv',_subst,pbo,pty, attrs in let proof'',goals = apply_tactic (PrimitiveTactics.apply_tac @@ -734,13 +734,13 @@ let apply_type_tac ~cast:t ~applist:al = let my_cut ~term:c = let my_cut ~term:c (proof,goal) = - let curi,metasenv,pbo,pty = proof in + let curi,metasenv,_subst,pbo,pty, attrs = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in let metasenv' = (fresh_meta,context,c)::metasenv in - let proof' = curi,metasenv',pbo,pty in + let proof' = curi,metasenv',_subst,pbo,pty, attrs in let proof'',goals = apply_tactic (apply_type_tac @@ -762,7 +762,7 @@ let tac_use h = let tac_use h status = let (proof, goal) = status in debug("Inizio TC_USE\n"); - let curi,metasenv,pbo,pty = proof in + let curi,metasenv,_subst,pbo,pty, attrs = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in debug ("hname = "^ CicPp.ppterm h.hname ^"\n"); debug ("ty = "^ CicPp.ppterm ty^"\n"); @@ -873,7 +873,7 @@ let equality_replace a b = debug("inizio EQ\n"); let module C = Cic in let proof,goal = status in - let curi,metasenv,pbo,pty = proof in + let curi,metasenv,_subst,pbo,pty, attrs = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] in let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in @@ -885,8 +885,8 @@ let equality_replace a b = (EqualityTactics.rewrite_simpl_tac ~direction:`LeftToRight ~pattern:(ProofEngineTypes.conclusion_pattern None) - (C.Meta (fresh_meta,irl))) - ((curi,metasenv',pbo,pty),goal) + (C.Meta (fresh_meta,irl)) []) + ((curi,metasenv',_subst,pbo,pty, attrs),goal) in let new_goals = fresh_meta::goals in debug("fine EQ -> goals : "^string_of_int( List.length new_goals) ^" = " @@ -934,7 +934,7 @@ let contradiction_tac (proof,goal)= (* ********************* TATTICA ******************************** *) let rec fourier (s_proof,s_goal)= - let s_curi,s_metasenv,s_pbo,s_pty = s_proof in + let s_curi,s_metasenv,_subst,s_pbo,s_pty, attrs = s_proof in let s_metano,s_context,s_ty = CicUtil.lookup_meta s_goal s_metasenv in debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto:\n"); debug_pcontext s_context; @@ -974,7 +974,7 @@ let rec fourier (s_proof,s_goal)= (* now we have all the right environment *) - let curi,metasenv,pbo,pty = proof in + let curi,metasenv,_subst,pbo,pty, attrs = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in (* now we want to convert hp to inequations, but first we must lift @@ -1061,7 +1061,7 @@ let rec fourier (s_proof,s_goal)= (Tacticals.thens ~start:(mk_tactic (fun status -> debug ("inizio t1 strict\n"); - let curi,metasenv,pbo,pty = proof in + let curi,metasenv,_subst,pbo,pty, attrs = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n"); debug ("ty = "^ CicPp.ppterm ty^"\n"); @@ -1092,7 +1092,7 @@ let rec fourier (s_proof,s_goal)= tac1:=(Tacticals.thens ~start:(mk_tactic (fun status -> debug("INIZIO TAC 1 2\n"); - let curi,metasenv,pbo,pty = proof in + let curi,metasenv,_subst,pbo,pty, attrs = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in debug ("th = "^ CicPp.ppterm _Rfourier_lt_le ^"\n"); debug ("ty = "^ CicPp.ppterm ty^"\n"); @@ -1128,7 +1128,7 @@ let rec fourier (s_proof,s_goal)= ~continuations:[Tacticals.then_ ~start:( mk_tactic (fun status -> let (proof, goal) = status in - let curi,metasenv,pbo,pty = proof in + let curi,metasenv,_subst,pbo,pty, attrs = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in apply_tactic (ReductionTactics.change_tac @@ -1161,13 +1161,13 @@ let rec fourier (s_proof,s_goal)= ~continuations: [PrimitiveTactics.apply_tac ~term:_Rinv_R1; Tacticals.first - ~tactics:[ "ring",Ring.ring_tac; "id", Tacticals.id_tac] + ~tactics:[Ring.ring_tac; Tacticals.id_tac] ]) ;(*Tacticals.id_tac*) Tacticals.then_ ~start:(mk_tactic (fun status -> let (proof, goal) = status in - let curi,metasenv,pbo,pty = proof in + let curi,metasenv,_subst,pbo,pty, attrs = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in (* check if ty is of type *) let w1 =