-(* The term bo must be closed in the current context *)
-let exact bo =
- let module T = CicTypeChecker in
- let module R = CicReduction in
- let metasenv =
- match !proof with
- None -> assert false
- | Some (metasenv,_,_) -> metasenv
- in
- let (metano,context,ty) =
- match !goal with
- None -> assert false
- | Some (metano,(context,ty)) ->
- assert (ty = List.assoc metano metasenv) ;
- (* Invariant: context is the actual context of the meta in the proof *)
- metano,context,ty
- in
- (*CSC: deve sparire! *)
- let context = cic_context_of_context context in
- if R.are_convertible (T.type_of_aux' metasenv context bo) ty then
- refine_meta metano bo []
- else
- raise (Fail "The type of the provided term is not the one expected.")
-;;
+let whd_in_scratch = reduction_tactic_in_scratch CicReduction.whd
+let reduce_in_scratch = reduction_tactic_in_scratch ProofEngineReduction.reduce
+let simpl_in_scratch = reduction_tactic_in_scratch ProofEngineReduction.simpl
+
+(************************************************************)
+(* Tactics defined elsewhere *)
+(************************************************************)
+
+ (* primitive tactics *)
+
+let apply term = apply_tactic (PrimitiveTactics.apply_tac ~term)
+let intros ?mk_fresh_name_callback () =
+ apply_tactic (PrimitiveTactics.intros_tac ?mk_fresh_name_callback ())
+let cut ?mk_fresh_name_callback term =
+ apply_tactic (PrimitiveTactics.cut_tac ?mk_fresh_name_callback term)
+let letin ?mk_fresh_name_callback term =
+ apply_tactic (PrimitiveTactics.letin_tac ?mk_fresh_name_callback term)
+let exact term = apply_tactic (PrimitiveTactics.exact_tac ~term)
+let elim_intros_simpl term =
+ apply_tactic (PrimitiveTactics.elim_intros_simpl_tac ~term)
+let change ~goal_input:what ~input:with_what =
+ apply_tactic (PrimitiveTactics.change_tac ~what ~with_what)
+
+ (* structural tactics *)
+
+let clearbody hyp = apply_tactic (ProofEngineStructuralRules.clearbody ~hyp)
+let clear hyp = apply_tactic (ProofEngineStructuralRules.clear ~hyp)
+
+ (* reduction tactics *)
+
+let whd terms =
+ apply_tactic
+ (ReductionTactics.whd_tac ~also_in_hypotheses:true ~terms:(Some terms))
+let reduce terms =
+ apply_tactic
+ (ReductionTactics.reduce_tac ~also_in_hypotheses:true ~terms:(Some terms))
+let simpl terms =
+ apply_tactic
+ (ReductionTactics.simpl_tac ~also_in_hypotheses:true ~terms:(Some terms))
+
+let fold_whd term =
+ apply_tactic
+ (ReductionTactics.fold_tac ~reduction:CicReduction.whd
+ ~also_in_hypotheses:true ~term)
+let fold_reduce term =
+ apply_tactic
+ (ReductionTactics.fold_tac ~reduction:ProofEngineReduction.reduce
+ ~also_in_hypotheses:true ~term)
+let fold_simpl term =
+ apply_tactic
+ (ReductionTactics.fold_tac ~reduction:ProofEngineReduction.simpl
+ ~also_in_hypotheses:true ~term)
+
+ (* other tactics *)
+
+let elim_type term = apply_tactic (EliminationTactics.elim_type_tac ~term)
+let ring () = apply_tactic Ring.ring_tac
+let fourier () = apply_tactic FourierR.fourier_tac
+let auto mqi_handle () = apply_tactic (VariousTactics.auto_tac mqi_handle)
+
+let rewrite_simpl term = apply_tactic (EqualityTactics.rewrite_simpl_tac ~term)
+let rewrite_back_simpl term = apply_tactic (EqualityTactics.rewrite_back_simpl_tac ~term)
+let replace ~goal_input:what ~input:with_what =
+ apply_tactic (EqualityTactics.replace_tac ~what ~with_what)
+
+let reflexivity () = apply_tactic EqualityTactics.reflexivity_tac
+let symmetry () = apply_tactic EqualityTactics.symmetry_tac
+let transitivity term = apply_tactic (EqualityTactics.transitivity_tac ~term)
+
+let exists () = apply_tactic IntroductionTactics.exists_tac
+let split () = apply_tactic IntroductionTactics.split_tac
+let left () = apply_tactic IntroductionTactics.left_tac
+let right () = apply_tactic IntroductionTactics.right_tac
+
+let assumption () = apply_tactic VariousTactics.assumption_tac
+
+let generalize ?mk_fresh_name_callback terms =
+ apply_tactic (VariousTactics.generalize_tac ?mk_fresh_name_callback terms)
+
+let absurd term = apply_tactic (NegationTactics.absurd_tac ~term)
+let contradiction () = apply_tactic NegationTactics.contradiction_tac
+
+let decompose ~uris_choice_callback term =
+ apply_tactic (EliminationTactics.decompose_tac ~uris_choice_callback term)
+
+let injection term = apply_tactic (DiscriminationTactics.injection_tac ~term)
+let discriminate term = apply_tactic (DiscriminationTactics.discriminate_tac ~term)
+let decide_equality () = apply_tactic DiscriminationTactics.decide_equality_tac
+let compare term = apply_tactic (DiscriminationTactics.compare_tac ~term)
+
+(*
+let prova_tatticali () = apply_tactic Tacticals.prova_tac
+*)
+