- Procedural: generation of "exact" is now complete

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

diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml
index 70b82092c8b16b688f186e7495d6104d67a56e3b..0040d7ebfe1a0ff34ba38b5d4b773114f7eb1002 100644 (file)
--- a/helm/software/components/tactics/primitiveTactics.ml
+++ b/helm/software/components/tactics/primitiveTactics.ml
@@ -462,26 +462,8 @@ let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst:
  in
   PET.mk_tactic (letin_tac ~mk_fresh_name_callback term)
 
-  (** functional part of the "exact" tactic *)
-let exact_tac ~term =
- let exact_tac ~term (proof, goal) =
-  (* Assumption: the term bo must be closed in the current context *)
-  let (_,metasenv,_subst,_,_, _) = proof in
-  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
-  let module T = CicTypeChecker in
-  let module R = CicReduction in
-  let ty_term,u = T.type_of_aux' metasenv context term CicUniv.oblivion_ugraph in
-  let b,_ = R.are_convertible context ty_term ty u in (* TASSI: FIXME *)
-  if b then
-   begin
-    let (newproof, metasenv') =
-      ProofEngineHelpers.subst_meta_in_proof proof metano term [] in
-    (newproof, [])
-   end
-  else
-   raise (PET.Fail (lazy "The type of the provided term is not the one expected."))
- in
-  PET.mk_tactic (exact_tac ~term)
+(* FG: exact_tac := apply_tac as in NTactics *)
+let exact_tac ~term = apply_tac ~term
 
 (* not really "primitive" tactics .... *)