X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=1c918ac50bbb1693dc7bef890fd775994464ca91;hb=833b0c94d93d3fe66cecbf0b0f9edf1287669b75;hp=037a36f38ca164790ba9b5af23f75c88c752d841;hpb=df753672ee6c511b6ce721c2124e3294d0a28dbd;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 037a36f38..1c918ac50 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -604,6 +604,9 @@ let eval_ng_tac (text, prefix_len, tac) =
            ) hyps,
           (text,prefix_len,concl))
        ) seqs)
+  | GrafiteAst.NAuto (_loc, (l,a)) ->
+      NTactics.auto_tac
+	~params:(List.map (fun x -> "",0,x) l,a)
   | GrafiteAst.NCases (_loc, what, where) ->
       NTactics.cases_tac 
         ~what:(text,prefix_len,what)
@@ -629,6 +632,17 @@ let eval_ng_tac (text, prefix_len, tac) =
      NTactics.rewrite_tac ~dir ~what:(text,prefix_len,what)
       ~where:(text,prefix_len,where)
 ;;
+      
+let subst_metasenv_and_fix_names s =
+  let u,h,metasenv, subst,o = s.NTacStatus.istatus.NTacStatus.pstatus in
+  let o = 
+    NCicUntrusted.map_obj_kind ~skip_body:true 
+     (NCicUntrusted.apply_subst subst []) o
+  in
+  { s with NTacStatus.istatus =
+     { s.NTacStatus.istatus with NTacStatus.pstatus =
+        u,h,NCicUntrusted.apply_subst_metasenv subst metasenv,subst,o}}
+;;
 
 let rec eval_command = {ec_go = fun ~disambiguate_command opts status
 (text,prefix_len,cmd) ->
@@ -696,7 +710,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
      LibraryObjects.set_default what uris;
      GrafiteTypes.add_moo_content [cmd] status,`Old []
   | GrafiteAst.Drop loc -> raise Drop
-  | GrafiteAst.Include (loc, baseuri) ->
+  | GrafiteAst.Include (loc, _, baseuri) ->
      let moopath_rw, moopath_r = 
        LibraryMisc.obj_file_of_baseuri 
          ~must_exist:false ~baseuri ~writable:true,
@@ -749,8 +763,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 ->
@@ -758,29 +771,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 = NCicTypeChecker.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"))
@@ -806,9 +819,10 @@ prerr_endline "CSC: here we should fix the height!!!";
       { status with
          GrafiteTypes.ng_status = 
           GrafiteTypes.ProofMode
-           { NTacStatus.gstatus = ninitial_stack; 
-             istatus = { NTacStatus.pstatus = obj; lstatus = lexicon_status}}
-           }
+           (subst_metasenv_and_fix_names
+            { NTacStatus.gstatus = ninitial_stack; 
+             istatus = { NTacStatus.pstatus = obj; lstatus = lexicon_status}})
+             }
      in
      (match nmenv with
          [] ->
@@ -909,6 +923,7 @@ prerr_endline "CSC: here we should fix the height!!!";
       | GrafiteTypes.CommandMode _ -> assert false
       | GrafiteTypes.ProofMode nstatus ->
          let nstatus = eval_ng_tac (text,prefix_len,tac) nstatus in
+         let nstatus = subst_metasenv_and_fix_names nstatus in
          let nstatus = eval_ng_punct (text,prefix_len,punct) nstatus in
          NTacStatus.pp_tac_status nstatus;
          { status with GrafiteTypes.ng_status= GrafiteTypes.ProofMode nstatus },