Introduction of vectors of implicit (only for NG).

[helm.git] / helm / software / matita / matitaScript.ml

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index e72644d105a6f238703539c4edc7c8c3847a4265..bbe76859f3daf7f1ffffaba61175940114e47f85 100644 (file)
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -74,8 +74,6 @@ type guistuff = {
 let eval_with_engine include_paths guistuff grafite_status user_goal
  skipped_txt nonskipped_txt st
 =
-  let module TAPp = GrafiteAstPp in
-  let module DTE = DisambiguateTypes.Environment in
   let parsed_text_length =
     String.length skipped_txt + String.length nonskipped_txt 
   in
@@ -212,7 +210,7 @@ let cic2grafite context menv t =
       | Cic.Const _ as t -> 
           PT.Ident (pp_t c t, None)
       | Cic.Appl l -> PT.Appl (List.map (aux c) l)
-      | Cic.Implicit _ -> PT.Implicit
+      | Cic.Implicit _ -> PT.Implicit `JustOne
       | Cic.Lambda (Cic.Name n, s, t) ->
           PT.Binder (`Lambda, (PT.Ident (n,None), Some (aux c s)),
             aux (Some (Cic.Name n, Cic.Decl s)::c) t)
@@ -222,7 +220,7 @@ let cic2grafite context menv t =
       | Cic.LetIn (Cic.Name n, s, ty, t) ->
           PT.Binder (`Lambda, (PT.Ident (n,None), Some (aux c s)),
             aux (Some (Cic.Name n, Cic.Def (s,ty))::c) t)
-      | Cic.Meta _ -> PT.Implicit
+      | Cic.Meta _ -> PT.Implicit `JustOne
       | Cic.Sort (Cic.Type u) -> PT.Sort (`Type u)
       | Cic.Sort Cic.Set -> PT.Sort `Set
       | Cic.Sort (Cic.CProp u) -> PT.Sort (`CProp u)
@@ -369,11 +367,8 @@ let cic2grafite context menv t =
 ;;
 
 let rec eval_macro include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text parsed_text script mac =
-  let module TAPp = GrafiteAstPp in
   let module MQ = MetadataQuery in
-  let module MDB = LibraryDb in
   let module CTC = CicTypeChecker in
-  let module CU = CicUniv in
   (* no idea why ocaml wants this *)
   let parsed_text_length = String.length parsed_text in
   let dbd = LibraryDb.instance () in
@@ -581,9 +576,6 @@ and eval_executable include_paths (buffer : GText.buffer) guistuff
 grafite_status user_goal unparsed_text skipped_txt nonskipped_txt
 script ex loc
 =
- let module TAPp = GrafiteAstPp in
- let module MD = MultiPassDisambiguator in
- let module ML = MatitaMisc in
   try
    ignore (buffer#move_mark (`NAME "beginning_of_statement")
     ~where:((buffer#get_iter_at_mark (`NAME "locked"))#forward_chars