From 9cfd213efc96e1bd60207d4edbf8c21ca80b6d80 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 4 Mar 2014 12:24:19 +0000 Subject: [PATCH] Bug fixed: the tactic to analyze the term and understand whose inductive type it belongs to did not put the sort in whd before concluding that it was not a sort. --- matita/components/ng_tactics/nTactics.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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) ;; -- 2.39.2