let hvar=Hashtbl.create 50 in (* la table des variables des inéquations *)
List.iter (fun f ->
Hashtbl.iter (fun x c ->
- try (Hashtbl.find hvar x;())
- with _-> nvar:=(!nvar)+1;
+ try ignore(Hashtbl.find hvar x)
+ with Not_found -> nvar:=(!nvar)+1;
Hashtbl.add hvar x (!nvar);
debug("aggiungo una var "^
string_of_int !nvar^" per "^
(*let cste = pf_parse_constr gl in*)
let pall str (proof,goal) t =
debug ("tac "^str^" :\n" );
- let curi,metasenv,pbo,pty, attrs = 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");
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, attrs = 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
let apply_type_tac ~cast:t ~applist:al =
let apply_type_tac ~cast:t ~applist:al (proof,goal) =
- let curi,metasenv,pbo,pty, attrs = 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, attrs in
+ let proof' = curi,metasenv',_subst,pbo,pty, attrs in
let proof'',goals =
apply_tactic
(PrimitiveTactics.apply_tac
let my_cut ~term:c =
let my_cut ~term:c (proof,goal) =
- let curi,metasenv,pbo,pty, attrs = 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, attrs in
+ let proof' = curi,metasenv',_subst,pbo,pty, attrs in
let proof'',goals =
apply_tactic
(apply_type_tac
let tac_use h status =
let (proof, goal) = status in
debug("Inizio TC_USE\n");
- let curi,metasenv,pbo,pty, attrs = 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");
[] -> []
| Some(name,Cic.Decl(a))::next ->
[Some(name,Cic.Decl(CicSubstitution.lift n a))]@ superlift next (n+1)
- | Some(name,Cic.Def(a,None))::next ->
- [Some(name,Cic.Def((CicSubstitution.lift n a),None))]@ superlift next (n+1)
- | Some(name,Cic.Def(a,Some ty))::next ->
+ | Some(name,Cic.Def(a,ty))::next ->
[Some(name,
- Cic.Def((CicSubstitution.lift n a),Some (CicSubstitution.lift n ty)))
+ Cic.Def((CicSubstitution.lift n a),CicSubstitution.lift n ty))
] @ superlift next (n+1)
| _::next -> superlift next (n+1) (*?? ??*)
debug("inizio EQ\n");
let module C = Cic in
let proof,goal = status in
- let curi,metasenv,pbo,pty, attrs = 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
~direction:`LeftToRight
~pattern:(ProofEngineTypes.conclusion_pattern None)
(C.Meta (fresh_meta,irl)) [])
- ((curi,metasenv',pbo,pty, attrs),goal)
+ ((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) ^" = "
(* ********************* TATTICA ******************************** *)
let rec fourier (s_proof,s_goal)=
- let s_curi,s_metasenv,s_pbo,s_pty, attrs = 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;
(* now we have all the right environment *)
- let curi,metasenv,pbo,pty, attrs = 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
(Tacticals.thens
~start:(mk_tactic (fun status ->
debug ("inizio t1 strict\n");
- let curi,metasenv,pbo,pty, attrs = 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");
tac1:=(Tacticals.thens
~start:(mk_tactic (fun status ->
debug("INIZIO TAC 1 2\n");
- let curi,metasenv,pbo,pty, attrs = 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");
~continuations:[Tacticals.then_
~start:( mk_tactic (fun status ->
let (proof, goal) = status in
- let curi,metasenv,pbo,pty, attrs = 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
~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, attrs = 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 =