From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 29 Nov 2004 12:24:47 +0000 (+0000)
Subject: passes ~subst to FreshNameGenerator
X-Git-Tag: PRE_UNIVERSES~5
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1e51af833318b686d3852fbce5c1b516f3901b5a;p=helm.git

passes ~subst to FreshNameGenerator
---

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index a649d4a23..fe566ab74 100644
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -52,7 +52,7 @@ let rewrite_tac ~term:equality =
         ~what:[t1'] ~with_what:[C.Rel 1] ~where:gty'
       in
        C.Lambda
-        (FreshNamesGenerator.mk_fresh_name metasenv context C.Anonymous ty,
+        (FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context C.Anonymous ~typ:ty,
           ty, gty'')
      in
      let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
@@ -113,7 +113,7 @@ let rewrite_back_tac ~term:equality =
         ~what:[t1'] ~with_what:[C.Rel 1] ~where:gty'
       in
        C.Lambda
-        (FreshNamesGenerator.mk_fresh_name metasenv context C.Anonymous ty,
+        (FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context C.Anonymous ~typ:ty,
           ty, gty'')
      in
      let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index fa6968560..f959746e2 100644
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -119,7 +119,7 @@ let eta_expand metasenv context t arg =
     T.type_of_aux' metasenv context arg
    in
     let fresh_name =
-     FreshNamesGenerator.mk_fresh_name
+     FreshNamesGenerator.mk_fresh_name ~subst:[]
       metasenv context (Cic.Name "Heta") ~typ:argty
     in
      (C.Appl [C.Lambda (fresh_name,argty,aux 0 t) ; arg])
@@ -362,9 +362,9 @@ let apply_tac ~term =
  in
   mk_tactic (apply_tac ~term)
 
-let intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) ()=
+let intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) ()=
  let intros_tac
-  ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) ()
+  ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) ()
   (proof, goal)
  =
   let module C = Cic in
@@ -382,9 +382,9 @@ let intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) ()=
  in
   mk_tactic (intros_tac ~mk_fresh_name_callback ())
   
-let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) ~term=
+let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) ~term=
  let cut_tac
-  ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name)
+  ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
   term (proof, goal)
  =
   let module C = Cic in
@@ -417,9 +417,9 @@ let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) ~term=
  in
   mk_tactic (cut_tac ~mk_fresh_name_callback term)
 
-let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name) ~term=
+let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst:[]) ~term=
  let letin_tac
-  ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name)
+  ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
   term (proof, goal)
  =
   let module C = Cic in
diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index 5be94e7df..5e2e39c5d 100644
--- a/helm/ocaml/tactics/variousTactics.ml
+++ b/helm/ocaml/tactics/variousTactics.ml
@@ -65,7 +65,7 @@ e li aggiunga nel context, poi si conta la lunghezza di questo nuovo
 contesto e si lifta di tot... COSA SIGNIFICA TUTTO CIO'?????? *)
 
 let generalize_tac 
- ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) terms
+ ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) terms
  =
   let module PET = ProofEngineTypes in
   let generalize_tac mk_fresh_name_callback terms status =