Changes to declarative tactics, implementation of equality chain

[helm.git] / matita / components / ng_tactics / nTactics.ml

diff --git a/matita/components/ng_tactics/nTactics.ml b/matita/components/ng_tactics/nTactics.ml
index 6241a3ea6baa7f13b25a9f2105b443e0ea018624..ed98b6d1e46e292bb711c3c1a621b4bc51b4873d 100644 (file)
--- a/matita/components/ng_tactics/nTactics.ml
+++ b/matita/components/ng_tactics/nTactics.ml
@@ -53,7 +53,7 @@ let branch_tac ?(force=false) status =
     | (g, t, k, tag) :: s ->
           match init_pos g with (* TODO *)
           | [] -> fail (lazy "empty goals")
-         | [_] when (not force) -> fail (lazy "too few goals to branch")
+          | [_] when (not force) -> fail (lazy "too few goals to branch")
           | loc :: loc_tl ->
                ([ loc ], [], [], `BranchTag) :: (loc_tl, t, k, tag) :: s
   in
@@ -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)
 ;;