compact coercion command: "coercion foo."

[helm.git] / matitaB / components / grafite_engine / grafiteEngine.ml

diff --git a/matitaB/components/grafite_engine/grafiteEngine.ml b/matitaB/components/grafite_engine/grafiteEngine.ml
index cbaa4d93a8f38f8b845476910d89ca51cb8422d9..c0d9baee7e56c814773cdc993337d778cba68bf3 100644 (file)
--- a/matitaB/components/grafite_engine/grafiteEngine.ml
+++ b/matitaB/components/grafite_engine/grafiteEngine.ml
@@ -493,7 +493,32 @@ 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, t, ty, source, target) ->
+  | GrafiteAst.NCoercion (loc, name, None) ->
+     let status, t, ty, source, target =
+       let o_t = NotationPt.Ident (name,`Ambiguous) 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 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, Some (t, ty, source, target)) ->
      let status, composites =
       NCicCoercDeclaration.eval_ncoercion status name t ty source target in
      let mode = GrafiteAst.WithPreferences in (* MATITA 1.0: fixme *)