From: Claudio Sacerdoti Coen Date: Mon, 4 Feb 2013 18:09:37 +0000 (+0000) Subject: Bug fixed: the indty can be typed with a Prod, not only with a Sort. X-Git-Tag: make_still_working~1276 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bdfe00cdb41263098c747853ae6b10fac73fcd35;p=helm.git Bug fixed: the indty can be typed with a Prod, not only with a Sort. --- diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index 5828bdea1..493d409da 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -882,7 +882,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = else let status = status#set_ng_mode `ProofMode in let metasenv,subst,status,indty = - GrafiteDisambiguate.disambiguate_nterm status `XTSort [] [] [] (text,prefix_len,indty) in + GrafiteDisambiguate.disambiguate_nterm status `XTNone [] [] [] (text,prefix_len,indty) in let indtyno, (_,_,tys,_,_),leftno = match indty with NCic.Const ((NReference.Ref (_,NReference.Ind (_,indtyno,leftno))) as r) -> indtyno, NCicEnvironment.get_checked_indtys status r, leftno