X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnTactics.ml;h=3ef2dbe5b0c331a122e57137fadab9ec44242379;hb=9cfd213efc96e1bd60207d4edbf8c21ca80b6d80;hp=6241a3ea6baa7f13b25a9f2105b443e0ea018624;hpb=b8bf1433f739c8befdf410ace0a0ff6e779a3339;p=helm.git

diff --git a/matita/components/ng_tactics/nTactics.ml b/matita/components/ng_tactics/nTactics.ml
index 6241a3ea6..3ef2dbe5b 100644
--- a/matita/components/ng_tactics/nTactics.ml
+++ b/matita/components/ng_tactics/nTactics.ml
@@ -515,7 +515,9 @@ let sort_of_goal_tac sortref = distribute_tac (fun status goal ->
   let goalty = get_goalty status goal in
   let status,sort = typeof status (ctx_of goalty) goalty in
   let status, sort = fix_sorts status sort in
-  let status, sort = term_of_cic_term status sort (ctx_of goalty) in
+  let ctx = ctx_of goalty in
+  let status, sort = whd status (ctx_of sort) sort in
+  let status, sort = term_of_cic_term status sort ctx in
    sortref := sort;
    status)
 ;;