From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 17 Jul 2009 20:04:36 +0000 (+0000)
Subject: nelim now uses the appropriate _rect_XXX elimination principle
X-Git-Tag: make_still_working~3660
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=b0e1947743d01746595f9ca39e25ba57f20089ac;p=helm.git

nelim now uses the appropriate _rect_XXX elimination principle
---

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 596a74e2e..4c5b38369 100644
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -481,7 +481,8 @@ let elim_tac ~what ~where =
      let name = NUri.name_of_uri uri ^
       match sort with
        | NCic.Sort NCic.Prop -> "_ind"
-       | NCic.Sort _ -> "_rect"
+       | NCic.Sort NCic.Type u ->
+          "_rect_" ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] sort
        | _ -> assert false 
      in
      let holes =