From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 27 Sep 2006 15:50:51 +0000 (+0000)
Subject: One less open helps understanding the code!
X-Git-Tag: 0.4.95@7852~985
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9897efac755aac85095075b7e0a967fe340092c1;p=helm.git

One less open helps understanding the code!
---

diff --git a/components/tactics/primitiveTactics.ml b/components/tactics/primitiveTactics.ml
index e09f0a1f7..139842435 100644
--- a/components/tactics/primitiveTactics.ml
+++ b/components/tactics/primitiveTactics.ml
@@ -25,7 +25,6 @@
 
 (* $Id$ *)
 
-open ProofEngineHelpers
 open ProofEngineTypes
 
 exception TheTypeOfTheCurrentGoalIsAMetaICannotChooseTheRightElimiantionPrinciple
@@ -232,7 +231,8 @@ let
 
 let new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty termty goal_arity =
   let (consthead,newmetasenv,arguments,_) =
-   saturate_term newmeta' metasenv' context termty goal_arity in
+   ProofEngineHelpers.saturate_term newmeta' metasenv' context termty
+    goal_arity in
   let subst,newmetasenv',_ = 
    CicUnification.fo_unif newmetasenv context consthead ty CicUniv.empty_ugraph
   in
@@ -318,7 +318,8 @@ let apply_with_subst ~term ~subst (proof, goal) =
      CicMetaSubst.apply_subst ((metano,(context,bo',Cic.Implicit None))::subst)
    in
    let (newproof, newmetasenv''') = 
-     subst_meta_and_metasenv_in_proof proof metano subst_in newmetasenv''
+    ProofEngineHelpers.subst_meta_and_metasenv_in_proof proof metano subst_in
+     newmetasenv''
    in
    (((metano,(context,bo',Cic.Implicit None))::subst)(* subst_in *), (* ALB *)
     (newproof, 
@@ -366,12 +367,13 @@ let intros_tac ?howmany ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_
   let module R = CicReduction in
    let (_,metasenv,_,_) = proof in
    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
-    let newmeta = new_meta_of_proof ~proof in
+    let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
      let (context',ty',bo') =
       lambda_abstract ?howmany metasenv context newmeta ty mk_fresh_name_callback
      in
       let (newproof, _) =
-        subst_meta_in_proof proof metano bo' [newmeta,context',ty']
+       ProofEngineHelpers.subst_meta_in_proof proof metano bo'
+        [newmeta,context',ty']
       in
        (newproof, [newmeta])
  in
@@ -385,7 +387,7 @@ let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:
   let module C = Cic in
    let curi,metasenv,pbo,pty = proof in
    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
-    let newmeta1 = new_meta_of_proof ~proof in
+    let newmeta1 = ProofEngineHelpers.new_meta_of_proof ~proof in
     let newmeta2 = newmeta1 + 1 in
     let fresh_name =
      mk_fresh_name_callback metasenv context (Cic.Name "Hcut") ~typ:term in
@@ -405,7 +407,7 @@ let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:
         C.Meta (newmeta2,irl2)]
      in
       let (newproof, _) =
-       subst_meta_in_proof proof metano bo'
+       ProofEngineHelpers.subst_meta_in_proof proof metano bo'
         [newmeta2,context,term; newmeta1,context_for_newmeta1,newmeta1ty];
       in
        (newproof, [newmeta1 ; newmeta2])
@@ -431,7 +433,7 @@ let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst:
          "You can't letin a term containing the current goal"));
     let _,_ =
       CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in
-     let newmeta = new_meta_of_proof ~proof in
+     let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
      let fresh_name =
       mk_fresh_name_callback metasenv context (Cic.Name "Hletin") ~typ:term in
      let context_for_newmeta =
@@ -443,7 +445,7 @@ let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst:
       let newmetaty = CicSubstitution.lift 1 ty in
       let bo' = C.LetIn (fresh_name,term,C.Meta (newmeta,irl)) in
        let (newproof, _) =
-         subst_meta_in_proof
+         ProofEngineHelpers.subst_meta_in_proof
            proof metano bo'[newmeta,context_for_newmeta,newmetaty]
        in
         (newproof, [newmeta])
@@ -463,7 +465,7 @@ let exact_tac ~term =
   if b then
    begin
     let (newproof, metasenv') =
-      subst_meta_in_proof proof metano term [] in
+      ProofEngineHelpers.subst_meta_in_proof proof metano term [] in
     (newproof, [])
    end
   else
@@ -586,13 +588,13 @@ let letout_tac =
    let letout_tac (proof, goal) =
       let curi, metasenv, pbo, pty = proof in
       let metano, context, ty = CicUtil.lookup_meta goal metasenv in
-      let newmeta = new_meta_of_proof ~proof in
+      let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
       let fresh_name = mk_fresh_name_callback metasenv context (Cic.Name "hole") ~typ:term in
       let context_for_newmeta = None :: context in
       let irl = CicMkImplicit.identity_relocation_list_for_metavariable context_for_newmeta in
       let newmetaty = CicSubstitution.lift 1 ty in
       let bo' = C.LetIn (fresh_name, term, C.Meta (newmeta,irl)) in
-      let newproof, _ = subst_meta_in_proof proof metano bo'[newmeta,context_for_newmeta,newmetaty] in
+      let newproof, _ = ProofEngineHelpers.subst_meta_in_proof proof metano bo'[newmeta,context_for_newmeta,newmetaty] in
       newproof, [newmeta]
    in
    mk_tactic letout_tac