From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
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;