X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=5086eb845c6424574c565f8471ecc96b216bac14;hb=b9d48c1a4433b3a2b17483bc207b2092f7ac4fd2;hp=493d409da7fb954bfe79811ce53b282f66d9de7e;hpb=bdfe00cdb41263098c747853ae6b10fac73fcd35;p=helm.git

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index 493d409da..5086eb845 100644
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -549,6 +549,14 @@ let compute_relevance status uri =
       NCic.Inductive (ind,leftno,tys,attrs)
 ;;
 
+let extract_uris status uris =
+ List.fold_left
+  (fun status uri ->
+    let obj = NCicEnvironment.get_checked_obj status uri in
+     let status = eval_extract_obj status obj in
+      eval_extract_ocaml_obj status obj
+  ) status uris
+;;
 
 let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
   match cmd with
@@ -590,17 +598,15 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
        in
        status, o_t, NotationPt.NCic ty, source, target
      in
-     let status, composites =
-      NCicCoercDeclaration.eval_ncoercion status name compose t ty source
-       target
-     in
-     let mode = GrafiteAst.WithPreferences in (* MATITA 1.0: fixme *)
-     let aliases = GrafiteDisambiguate.aliases_for_objs status composites in
-      eval_alias status (mode,aliases)
+      let cmd = 
+       GrafiteAst.NCoercion (loc, name, compose, Some (t, ty, source, target))
+      in
+      eval_ncommand ~include_paths opts status (text,prefix_len,cmd)
   | GrafiteAst.NCoercion (loc, name, compose, Some (t, ty, source, target)) ->
      let status, composites =
       NCicCoercDeclaration.eval_ncoercion status name compose t ty source
        target in
+     let status = extract_uris status composites in
      let mode = GrafiteAst.WithPreferences in (* MATITA 1.0: fixme *)
      let aliases = GrafiteDisambiguate.aliases_for_objs status composites in
       eval_alias status (mode,aliases)
@@ -657,6 +663,9 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
             | _ -> status)
          else
           status in
+        (* purge tinycals stack *)
+        let ninitial_stack = Continuationals.Stack.of_nmetasenv [] in
+        let status = status#set_stack ninitial_stack in
 (*
 	  try 
 	    index_eq uri status
@@ -688,7 +697,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
                 else
                   nstatus
                with
-               | MultiPassDisambiguator.DisambiguationError _ as e ->
+               | MultiPassDisambiguator.DisambiguationError _ ->
                   HLog.warn "error in disambiguating projection/eliminator";
                   status
                | NCicTypeChecker.TypeCheckerFailure _ ->
@@ -808,14 +817,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
                      basic_eval_and_record_ncoercion_from_t_cpos_arity 
                       status (name,true,t,cpos,arity) in
                  let aliases = GrafiteDisambiguate.aliases_for_objs status nuris in
-                 let status =
-                  List.fold_left
-                   (fun status uri ->
-                     let obj = NCicEnvironment.get_checked_obj status uri in
-                      let status = eval_extract_obj status obj in
-                       eval_extract_ocaml_obj status obj
-                   ) status nuris
-                 in
+                 let status = extract_uris status nuris in
                   eval_alias status (mode,aliases)
                with MultiPassDisambiguator.DisambiguationError _-> 
                  HLog.warn ("error in generating coercion: "^name);