From b0e1947743d01746595f9ca39e25ba57f20089ac Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 17 Jul 2009 20:04:36 +0000
Subject: [PATCH] nelim now uses the appropriate _rect_XXX elimination
 principle

---
 helm/software/components/ng_tactics/nTactics.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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 = 
-- 
2.39.2