X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=ec14f4d3e940470ff42817e48a0d4bcf6e967dc9;hb=5c1794aba0652c0b0bce80a9ffc426192327709f;hp=c5e2919599146b82fb559213a1ce199249658347;hpb=f5b9e1d5511a13ca5bb424c149781087aa0c8e31;p=helm.git

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index c5e291959..ec14f4d3e 100644
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -495,19 +495,26 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
        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
+           | 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
+           | NCic.Sort _ as r -> NotationPt.NCic r (* FG: missing case *)
+	   | _ -> 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
+           | 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
+       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)