From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 7 Jun 2012 11:53:26 +0000 (+0000)
Subject: Patch to avoid generating _inv_ind_recTX for X the largest universe.
X-Git-Tag: make_still_working~1650
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=46990564407e2402686022884767fc749a97d734;p=helm.git

Patch to avoid generating _inv_ind_recTX for X the largest universe.
Rational: for some unknown reason, that takes ages to fail.
---

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index af0abe04a..57491cbda 100644
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -634,7 +634,16 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
                   (*HLog.warn "error in generating projection/eliminator";*)
                   status
              ) status boxml in             
-           let _,_,_,_,nobj = obj in 
+           let _,_,_,_,nobj = obj in
+           (* attempting to generate an inversion principle on the maximum
+            * universe can take a long time to fail: this code removes maximal
+            * sorts from the universe list *)
+           let universes = NCicEnvironment.get_universes () in
+           let max_univ = List.fold_left max [] universes in
+           let universes = 
+             List.filter (fun x -> NCicEnvironment.universe_lt x max_univ)
+               universes
+           in
            let status = match nobj with
                NCic.Inductive (is_ind,leftno,itl,_) ->
                  List.fold_left (fun status it ->      
@@ -660,8 +669,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
                                 let status = status#set_ng_mode `CommandMode in status)
                   status
                   (NCic.Prop::
-                    List.map (fun s -> NCic.Type s)
-                    (NCicEnvironment.get_universes ())))) status itl
+                    List.map (fun s -> NCic.Type s) universes))) status itl
               | _ -> status
            in
            let status = match nobj with