cicNotation* ==> notation*

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

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index b122366c1ea77d3d9ffb831cb7bd9651da0ba9e6..e87795900c77bef72aee0ac6ffda9371695f8ac0 100644 (file)
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -44,22 +44,6 @@ let concat_nuris uris nuris =
    | `New uris, `New nuris -> `New (nuris@uris)
    | _ -> assert false
 ;;
-(** create a ProofEngineTypes.mk_fresh_name_type function which uses given
-  * names as long as they are available, then it fallbacks to name generation
-  * using FreshNamesGenerator module *)
-let namer_of names =
-  let len = List.length names in
-  let count = ref 0 in
-  fun metasenv context name ~typ ->
-    if !count < len then begin
-      let name = match List.nth names !count with
-         | Some s -> Cic.Name s
-        | None   -> Cic.Anonymous
-      in
-      incr count;
-      name
-    end else
-      FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ
 
 type eval_ast =
  {ea_go:
@@ -302,7 +286,7 @@ let eval_add_constraint status u1 u2 =
  let status = basic_eval_add_constraint (u1,u2) status in
  let dump = inject_constraint (u1,u2)::status#dump in
  let status = status#set_dump dump in
-  status,`Old []
+  status,`New []
 ;;
 
 let add_coercions_of_lemmas lemmas status =
@@ -320,31 +304,6 @@ let add_coercions_of_lemmas lemmas status =
    status#set_coercions (CoercDb.dump ()), 
   lemmas
 
-let eval_coercion status ~add_composites uri arity saturations =
- let uri = 
-   try CicUtil.uri_of_term uri 
-   with Invalid_argument _ -> 
-     raise (Invalid_argument "coercion can only be constants/constructors")
- in
- let status, lemmas =
-  GrafiteSync.add_coercion ~add_composites 
-    ~pack_coercion_obj:CicRefine.pack_coercion_obj
-   status uri arity saturations status#baseuri in
- let moo_content = coercion_moo_statement_of (uri,arity,saturations,0) in
- let status = GrafiteTypes.add_moo_content [moo_content] status in 
-  add_coercions_of_lemmas lemmas status
-
-let eval_prefer_coercion status c =
- let uri = 
-   try CicUtil.uri_of_term c 
-   with Invalid_argument _ -> 
-     raise (Invalid_argument "coercion can only be constants/constructors")
- in
- let status = GrafiteSync.prefer_coercion status uri in
- let moo_content = GrafiteAst.PreferCoercion (HExtlib.dummy_floc,c) in
- let status = GrafiteTypes.add_moo_content [moo_content] status in 
- status, `Old []
-
 let eval_ng_punct (_text, _prefix_len, punct) =
   match punct with
   | GrafiteAst.Dot _ -> NTactics.dot_tac 
@@ -584,7 +543,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
                try
                  let metasenv,subst,status,t =
                   GrafiteDisambiguate.disambiguate_nterm None status [] [] []
-                   ("",0,CicNotationPt.Ident (name,None)) in
+                   ("",0,NotationPt.Ident (name,None)) in
                  assert (metasenv = [] && subst = []);
                  let status, nuris = 
                    NCicCoercDeclaration.
@@ -709,16 +668,9 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
  let status,cmd = disambiguate_command status (text,prefix_len,cmd) in
  let status,uris =
   match cmd with
-  | GrafiteAst.PreferCoercion (loc, coercion) ->
-     eval_prefer_coercion status coercion
-  | GrafiteAst.Coercion (loc, uri, add_composites, arity, saturations) ->
-     let res,uris =
-      eval_coercion status ~add_composites uri arity saturations
-     in
-      res,`Old uris
   | GrafiteAst.Default (loc, what, uris) as cmd ->
      LibraryObjects.set_default what uris;
-     GrafiteTypes.add_moo_content [cmd] status,`Old []
+     GrafiteTypes.add_moo_content [cmd] status,`New []
   | GrafiteAst.Drop loc -> raise Drop
   | GrafiteAst.Include (loc, mode, new_or_old, baseuri) ->
      (* Old Include command is not recursive; new one is *)
@@ -745,9 +697,9 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
        GrafiteTypes.add_moo_content
         [GrafiteAst.Include (loc,mode,`New,baseuri)] status
       in
-       status,`Old []
-  | GrafiteAst.Print (_,_) -> status,`Old []
-  | GrafiteAst.Set (loc, name, value) -> status, `Old []
+       status,`New []
+  | GrafiteAst.Print (_,_) -> status,`New []
+  | GrafiteAst.Set (loc, name, value) -> status, `New []
 (*       GrafiteTypes.set_option status name value,[] *)
   | GrafiteAst.Obj (loc,obj) -> (* MATITA 1.0 *) assert false
  in
@@ -793,7 +745,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
          ~disambiguate_macro:(fun _ _ -> assert false)
          status ast
       in
-       assert (lemmas=`Old []);
+       assert (lemmas=`New []);
        status)
     status moo
 } and eval_ast = {ea_go = fun ~disambiguate_command
@@ -808,7 +760,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
   | GrafiteAst.Comment (_,c) -> 
       eval_comment.ecm_go ~disambiguate_command opts status (text,prefix_len,c) 
 } and eval_comment = { ecm_go = fun ~disambiguate_command opts status (text,prefix_len,c) -> 
-    status, `Old []
+    status, `New []
 }
 ;;