From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 15 Jun 2005 11:39:45 +0000 (+0000)
Subject: apply_tac used to calculate the type of the term before generalizing on explicit... 
X-Git-Tag: PRE_STORAGE~11
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6e5cebb351c9cbc119143da528083f142f81b582;p=helm.git

apply_tac used to calculate the type of the term before generalizing on explicit name subts
---

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 7bbdbf6b0..c155d81cc 100644
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -328,12 +328,10 @@ let apply_tac_verbose ~term (proof, goal) =
    in
    let metasenv' = metasenv@newmetasenvfragment in
    let termty,_ = 
-     CicTypeChecker.type_of_aux' metasenv' context term CicUniv.empty_ugraph in
+     CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph in
    let termty =
      CicSubstitution.subst_vars exp_named_subst_diff termty
    in
-(*   prerr_endline ("term:" ^ CicPp.ppterm term);*)
-(*   prerr_endline ("termty:" ^ CicPp.ppterm termty);*)
    let subst,newmetasenv',t = 
      try
        new_metasenv_and_unify_and_t newmeta' metasenv' proof context term' ty