]> matita.cs.unibo.it Git - helm.git/commitdiff
nelim now uses the appropriate _rect_XXX elimination principle
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 17 Jul 2009 20:04:36 +0000 (20:04 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 17 Jul 2009 20:04:36 +0000 (20:04 +0000)
helm/software/components/ng_tactics/nTactics.ml

index 596a74e2e5fa1a837c7335a8faf3233462dedd6d..4c5b38369e986e80034f5a1f345004a445240987 100644 (file)
@@ -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 =