From: Claudio Sacerdoti Coen Date: Thu, 13 Aug 2009 17:15:16 +0000 (+0000) Subject: Some quick patch to fix elimination that used to look for X-Git-Tag: make_still_working~3547 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5366f90df289f2ab2bd97c68643198f54ad2d2ac;p=helm.git Some quick patch to fix elimination that used to look for nat_rect_max{CProp0,Type0} --- diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml index 52a45bbd4..035e65ac7 100644 --- a/helm/software/components/ng_tactics/nTacStatus.ml +++ b/helm/software/components/ng_tactics/nTacStatus.ml @@ -152,6 +152,14 @@ let unify status ctx a b = ;; let unify a b c d = wrap (unify a b c) d;; +let fix_sorts (name,ctx,t) = + let f () = + let t = NCicUnification.fix_sorts t in + name,ctx,t + in + wrap f () +;; + let refine status ctx term expty = let status, (nt,_,term) = relocate status ctx term in let status, ne, expty = diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli index 3fdc0330d..9279de399 100644 --- a/helm/software/components/ng_tactics/nTacStatus.mli +++ b/helm/software/components/ng_tactics/nTacStatus.mli @@ -55,6 +55,7 @@ val refine: 'status * cic_term * cic_term (* status, term, type *) val apply_subst: #pstatus as 'status -> NCic.context -> cic_term -> 'status * cic_term +val fix_sorts: cic_term -> cic_term val get_goalty: #pstatus -> int -> cic_term val mk_meta: diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index 0d06da71d..0030fd75a 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -468,6 +468,7 @@ let elim_tac ~what:(txt,len,what) ~where = let compute_goal_sort_tac = distribute_tac (fun status goal -> let goalty = get_goalty status goal in let status, goalsort = typeof status (ctx_of goalty) goalty in + let goalsort = fix_sorts goalsort in sort := Some goalsort; exec id_tac status goal) in @@ -514,7 +515,9 @@ let rewrite_tac ~dir ~what:(_,_,what) ~where status = | _ -> assert false in let name = - match dir with `LeftToRight -> "eq_elim_r" | `RightToLeft -> "eq" ^ suffix + match dir with + `LeftToRight -> "eq" ^ suffix ^ "_r" + | `RightToLeft -> "eq" ^ suffix in block_tac [ select_tac ~where ~job:(`Substexpand 1) true;