X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=8101dd667b96572d2581108e806004b28ad8f007;hb=11b2157bacf59cfc561c2ef6f92ee41ee2c1a006;hp=a0fdb92d7e9f1319c5b5746ddd775e55e09d2855;hpb=4514417676056e0be6cc481a931e70a627882867;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index a0fdb92d7..8101dd667 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -760,8 +760,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
       let name = UriManager.name_of_uri uri in
       let obj = Cic.Constant (name,Some (Lazy.force bo),ty,[],attrs) in
       let status, lemmas = add_obj uri obj status in
-       {status with 
-	  GrafiteTypes.proof_status = GrafiteTypes.No_proof},
+       {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},
         (*CSC: I throw away the arities *)
         `Old (uri::lemmas)
   | GrafiteAst.NQed loc ->
@@ -769,30 +768,29 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
        | GrafiteTypes.ProofMode
           { NTacStatus.istatus =
              {NTacStatus.pstatus = pstatus; lstatus=lexicon_status} } ->
-            let uri,height,menv,subst,obj = pstatus in
+            let uri,height,menv,subst,obj_kind = pstatus in
              if menv <> [] then
               raise
                (GrafiteTypes.Command_error"You can't Qed an incomplete theorem")
              else
-              let obj =
-prerr_endline "CSC: here we should fix the height!!!";
-               (uri,height,[],[],
-                NCicUntrusted.map_obj_kind 
-                  (NCicUntrusted.apply_subst subst [])
-                 obj) in
-              NCicTypeChecker.typecheck_obj obj;
-              NCicLibrary.add_obj uri obj;
-              let objs = NCicElim.mk_elims obj in
-              let uris =
-               uri::
-                List.map
-                 (fun (uri,_,_,_,_) as obj ->
-                   NCicTypeChecker.typecheck_obj obj;
-                   NCicLibrary.add_obj uri obj;
-                   uri
-                 ) objs
-              in
-               {status with 
+              let obj_kind =
+               NCicUntrusted.map_obj_kind 
+                (NCicUntrusted.apply_subst subst []) obj_kind in
+              let height = NCicUntrusted.height_of_obj_kind uri obj_kind in
+              let obj = uri,height,[],[],obj_kind in
+               NCicTypeChecker.typecheck_obj obj;
+               NCicLibrary.add_obj uri obj;
+               let objs = NCicElim.mk_elims obj in
+               let uris =
+                uri::
+                 List.map
+                  (fun (uri,_,_,_,_) as obj ->
+                    NCicTypeChecker.typecheck_obj obj;
+                    NCicLibrary.add_obj uri obj;
+                    uri
+                  ) objs
+               in
+                {status with 
                  GrafiteTypes.ng_status = 
                   GrafiteTypes.CommandMode lexicon_status },`New uris
        | _ -> raise (GrafiteTypes.Command_error "Not in proof mode"))