X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=c5e2919599146b82fb559213a1ce199249658347;hb=e305a62a7cb0a49fea3d241474e4c5bcd40e7272;hp=59821ac09734d36345d29ef1825e22acfd1fe95d;hpb=59e3ddd15ee1983027e8929c073b06a80d523875;p=helm.git

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index 59821ac09..c5e291959 100644
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -485,7 +485,33 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
       GrafiteTypes.Serializer.require
        ~alias_only ~baseuri ~fname:fullpath status
   | GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n
-  | GrafiteAst.NCoercion (loc, name, compose, t, ty, source, target) ->
+  | GrafiteAst.NCoercion (loc, name, compose, None) ->
+     let status, t, ty, source, target =
+       let o_t = NotationPt.Ident (name,None) in
+       let metasenv,subst, status,t =
+         GrafiteDisambiguate.disambiguate_nterm 
+           status None [] [] [] ("",0,o_t) in
+       assert( metasenv = [] && subst = []);
+       let ty = NCicTypeChecker.typeof status [] [] [] t in
+       let source, target =
+         let clean = function
+         | NCic.Appl (NCic.Const _ as r :: l) -> 
+             NotationPt.Appl (NotationPt.NCic r ::
+               List.map (fun _ -> NotationPt.Implicit `JustOne)l)
+         | NCic.Const _ as r -> NotationPt.NCic r
+         | _ -> assert false in
+         let rec aux = function
+         | NCic.Prod (_,_, (NCic.Prod _ as rest)) -> aux rest
+         | NCic.Prod (name, src, tgt) -> (name, clean src), clean tgt
+         | _ -> assert false in aux ty 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)
+  | GrafiteAst.NCoercion (loc, name, compose, Some (t, ty, source, target)) ->
      let status, composites =
       NCicCoercDeclaration.eval_ncoercion status name compose t ty source
        target in
@@ -512,7 +538,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
               (match spec with
               | NReference.Def _ -> NReference.Def height
               | NReference.Fix (i,j,_) -> NReference.Fix(i,j,height)
-              | NReference.CoFix _ -> NReference.CoFix height
+              | NReference.CoFix i -> NReference.CoFix i
               | NReference.Ind _ | NReference.Con _
               | NReference.Decl as s -> s))
           | t -> NCicUtils.map status (fun _ () -> ()) () fix t
@@ -561,7 +587,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
                try
                 let nstatus =
                  eval_ncommand ~include_paths opts status
-                  ("",0,GrafiteAst.NObj (HExtlib.dummy_floc,boxml))
+                  ("",0,GrafiteAst.NObj (HExtlib.dummy_floc,boxml,true))
                 in
                 if nstatus#ng_mode <> `CommandMode then
                   begin
@@ -579,9 +605,10 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
              ) status boxml in             
            let _,_,_,_,nobj = obj in 
            let status = match nobj with
-               NCic.Inductive (is_ind,leftno,[it],_) ->
-                 let _,ind_name,ty,cl = it in
-                 List.fold_left 
+               NCic.Inductive (is_ind,leftno,itl,_) ->
+                 List.fold_left (fun status it ->      
+                 (let _,ind_name,ty,cl = it in
+                  List.fold_left 
                    (fun status outsort ->
                       let status = status#set_ng_mode `ProofMode in
                       try
@@ -600,7 +627,8 @@ 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 ()))
+                    List.map (fun s -> NCic.Type s)
+                    (NCicEnvironment.get_universes ())))) status itl
               | _ -> status
            in
            let status = match nobj with
@@ -718,7 +746,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
        let status = subst_metasenv_and_fix_names status in
        let status = status#set_ng_mode `ProofMode in
        eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,false))
-  | GrafiteAst.NObj (loc,obj) ->
+  | GrafiteAst.NObj (loc,obj,index) ->
      if status#ng_mode <> `CommandMode then
       raise (GrafiteTypes.Command_error "Not in command mode")
      else
@@ -733,7 +761,8 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
       let status = status#set_ng_mode `ProofMode in
       (match nmenv with
           [] ->
-           eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,true))
+           eval_ncommand ~include_paths opts status
+             ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,index))
         | _ -> status)
   | GrafiteAst.NDiscriminator (loc, indty) ->
       if status#ng_mode <> `CommandMode then