X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnTactics.ml;h=ed98b6d1e46e292bb711c3c1a621b4bc51b4873d;hb=3fab56d1663ba3d5aeb9207612279e0bb0edbb8c;hp=6241a3ea6baa7f13b25a9f2105b443e0ea018624;hpb=f7da48c844105a52a705872dfa0d4104de010c82;p=helm.git diff --git a/matita/components/ng_tactics/nTactics.ml b/matita/components/ng_tactics/nTactics.ml index 6241a3ea6..ed98b6d1e 100644 --- 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) ;;