]> matita.cs.unibo.it Git - helm.git/commitdiff
Introduction of vectors of implicit (only for NG).
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 28 Jul 2009 15:17:51 +0000 (15:17 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 28 Jul 2009 15:17:51 +0000 (15:17 +0000)
Proposed concrete syntax: "..."

20 files changed:
helm/software/components/acic_content/cicNotationPp.ml
helm/software/components/acic_content/cicNotationPt.ml
helm/software/components/acic_content/cicNotationUtil.ml
helm/software/components/acic_content/termAcicContent.ml
helm/software/components/cic/cicUtil.ml
helm/software/components/cic_disambiguation/cicDisambiguate.ml
helm/software/components/content_pres/cicNotationLexer.ml
helm/software/components/content_pres/cicNotationParser.ml
helm/software/components/content_pres/content2presMatcher.ml
helm/software/components/content_pres/termContentPres.ml
helm/software/components/disambiguation/disambiguate.ml
helm/software/components/grafite_parser/grafiteParser.ml
helm/software/components/ng_cic_content/nTermCicContent.ml
helm/software/components/ng_disambiguation/nCicDisambiguate.ml
helm/software/components/ng_kernel/nCic.ml
helm/software/components/ng_kernel/nCicPp.ml
helm/software/components/ng_tactics/nCicElim.ml
helm/software/components/ng_tactics/nTactics.ml
helm/software/components/tptp_grafite/tptp2grafite.ml
helm/software/matita/matitaScript.ml

index 5eb6b64d2ad26fd1c27a3904bb94126a12176b22..1e759930ac4ef706175c85c181244657e3dd5558 100644 (file)
@@ -117,14 +117,14 @@ let rec pp_term ?(pp_parens = true) t =
           (pp_term ~pp_parens:true t3)
     | Ast.LetRec (kind, definitions, term) ->
        let rec get_guard i = function
-          | []                   -> (*assert false*) Ast.Implicit
+          | []                   -> (*assert false*) Ast.Implicit `JustOne
           | [term, _] when i = 1 -> term
           | _ :: tl              -> get_guard (pred i) tl
        in
        let map (params, (id,typ), body, i) =
          let typ =
           match typ with
-             None -> Ast.Implicit
+             None -> Ast.Implicit `JustOne
            | Some typ -> typ
          in
           sprintf "%s %s on %s: %s \\def %s" 
@@ -143,7 +143,8 @@ let rec pp_term ?(pp_parens = true) t =
     | Ast.Ident (name, Some substs)
     | Ast.Uri (name, Some substs) ->
         sprintf "%s \\subst [%s]" name (pp_substs substs)
-    | Ast.Implicit -> "?"
+    | Ast.Implicit `Vector -> "?"
+    | Ast.Implicit `JustOne -> "..."
     | Ast.Meta (index, substs) ->
         sprintf "%d[%s]" index
           (String.concat "; "
@@ -166,7 +167,7 @@ let rec pp_term ?(pp_parens = true) t =
   in
   match pp_parens, t with
     | false, _ 
-    | true, Ast.Implicit
+    | true, Ast.Implicit _
     | true, Ast.Sort _
     | true, Ast.Ident (_, Some []) 
     | true, Ast.Ident (_, None)    -> t_pp
index 8dbfea7992019a4e69a894cda12cec357b55d666..75e580d00e0cc0c93a93aacb1c35c505783916e6 100644 (file)
@@ -83,7 +83,7 @@ type term =
       (* literal, substitutions.
       * Some [] -> user has given an empty explicit substitution list 
       * None -> user has given no explicit substitution list *)
-  | Implicit
+  | Implicit of [`Vector | `JustOne]
   | Meta of int * meta_subst list
   | Num of string * int (* literal, instance *)
   | Sort of sort_kind
index b426863cf613e7f77d1123bb89cf747fe4ac18cf..4e5917a154aa87abdd493d46921e0c8bd07eccf0 100644 (file)
@@ -63,7 +63,7 @@ let visit_ast ?(special_k = fun _ -> assert false)
       | Ast.Variable _) as t -> special_k t
     | (Ast.Ident _
       | Ast.NRef _
-      | Ast.Implicit
+      | Ast.Implicit _
       | Ast.Num _
       | Ast.Sort _
       | Ast.Symbol _
@@ -208,7 +208,7 @@ let meta_names_of_term term =
     | Ast.Ident (_, Some substs) -> aux_substs substs
     | Ast.Meta (_, substs) -> aux_meta_substs substs
 
-    | Ast.Implicit
+    | Ast.Implicit _
     | Ast.Ident _
     | Ast.Num _
     | Ast.Sort _
index 81d0ef0a74f12211cb7a8e74ba7fd504fbf5311e..6eeb45749510c8ed03c6444209bef4863f2fd219 100644 (file)
@@ -121,7 +121,7 @@ let ast_of_acic0 ~output_type term_info acic k =
     | Cic.ASort (id,Cic.Type u) -> idref id (Ast.Sort (`Type u))
     | Cic.ASort (id,Cic.CProp u) -> idref id (Ast.Sort (`CProp u))
     | Cic.AImplicit (id, Some `Hole) -> idref id Ast.UserInput
-    | Cic.AImplicit (id, _) -> idref id Ast.Implicit
+    | Cic.AImplicit (id, _) -> idref id (Ast.Implicit `JustOne)
     | Cic.AProd (id,n,s,t) ->
         let binder_kind =
           match sort_of_id id with
index 36f65391eeac23d27c565b65d8e09ea52cd22f0c..9b6ece214f4d1d251c28f85b25e82c3613c058fb 100644 (file)
@@ -622,11 +622,12 @@ let pp_rel out c i =
       | Some (s, _)    -> out (Printf.sprintf "%u[" i); pp_name out s; out "]"
    with Failure "nth" -> out (Printf.sprintf "%u[%i]" i (List.length c - i))
 
-let pp_implict out = function
+let pp_implicit out = function
    | None         -> out "?"
    | Some `Closed -> out "?[Closed]" 
    | Some `Type   -> out "?[Type]"
    | Some `Hole   -> out "?[Hole]"
+   | Some `Vector -> out "?[...]"
 
 let pp_uri out a =
    out (Printf.sprintf "%s<%s>" (UM.name_of_uri a) (UM.string_of_uri a)) 
@@ -634,7 +635,7 @@ let pp_uri out a =
 let rec pp_term out e c = function
    | C.Sort h                      -> pp_sort out h
    | C.Rel i                       -> pp_rel out c i
-   | C.Implicit x                  -> pp_implict out x
+   | C.Implicit x                  -> pp_implicit out x
    | C.Meta (i, iss)               ->
       let map = function None   -> out "_" | Some v -> pp_term out e c v in
       out (Printf.sprintf "?%u" i); xiter out "[" "; " "]" map iss
index cf59ab553c33efc202208ea7d0cea86f7734aa74..e52db62ddf293312f8707cf8cbde58a40528485f 100644 (file)
@@ -353,7 +353,9 @@ let interpretate_term ~mk_choice ?(create_dummy_ids=false) ~context ~env ~uri
               let cic_body =
                aux ~localize loc context' (add_binders `Lambda body) in
               let typ =
-               match typ with Some typ -> typ | None-> CicNotationPt.Implicit in
+               match typ with
+                  Some typ -> typ
+                | None-> CicNotationPt.Implicit `JustOne in
               let cic_type =
                aux_option ~localize loc context (Some `Type)
                 (Some (add_binders `Pi typ)) in
@@ -482,7 +484,8 @@ let interpretate_term ~mk_choice ?(create_dummy_ids=false) ~context ~env ~uri
            with 
              CicEnvironment.CircularDependency _ -> 
                raise (DisambiguateTypes.Invalid_choice (lazy (loc,"Circular dependency in the environment")))))
-    | CicNotationPt.Implicit -> Cic.Implicit None
+    | CicNotationPt.Implicit `Vector -> assert false
+    | CicNotationPt.Implicit `JustOne -> Cic.Implicit None
     | CicNotationPt.UserInput -> Cic.Implicit (Some `Hole)
     | CicNotationPt.Num (num, i) ->
        Disambiguate.resolve ~mk_choice ~env
@@ -539,7 +542,7 @@ let interpretate_obj ~mk_choice ~context ~env ~uri ~is_path obj
         (fun (context,res) (name,t) ->
           let t =
            match t with
-              None -> CicNotationPt.Implicit
+              None -> CicNotationPt.Implicit `JustOne
             | Some t -> t in
           let name = CicNotationUtil.cic_name_of_name name in
            name::context,(name, interpretate_term context env None false t)::res
@@ -581,7 +584,7 @@ let interpretate_obj ~mk_choice ~context ~env ~uri ~is_path obj
         (fun (context,res) (name,t) ->
           let t =
            match t with
-              None -> CicNotationPt.Implicit
+              None -> CicNotationPt.Implicit `JustOne
             | Some t -> t in
           let name = CicNotationUtil.cic_name_of_name name in
            name::context,(name, interpretate_term context env None false t)::res
index 21031d002fc10fba43eb915623f054d45743ecd0..1dab53582f590d6addf47af680be5cfe25580799 100644 (file)
@@ -69,6 +69,7 @@ let regexp delim_end = "\\]"
 let regexp qkeyword = "'" ( ident | pident ) "'"
 
 let regexp implicit = '?'
+let regexp implicit_vector = "..."
 let regexp placeholder = '%'
 let regexp meta = implicit number
 
@@ -316,6 +317,7 @@ and level2_ast_token =
      let s = Ulexing.utf8_lexeme lexbuf in
       return lexbuf ("META", String.sub s 1 (String.length s - 1))
   | implicit -> return lexbuf ("IMPLICIT", "")
+  | implicit_vector -> return lexbuf ("IMPLICITVECTOR", "")
   | placeholder -> return lexbuf ("PLACEHOLDER", "")
   | ident -> handle_keywords lexbuf (Hashtbl.mem !level2_ast_keywords) "IDENT"
   | variable_ident -> return lexbuf ("IDENT", Ulexing.utf8_lexeme lexbuf)
index 7317f6139b0bf96e8ec4d8595b51e72d6d1ced6e..2ac6b7e6a4ad31e702b9c58768c09f7effcd50d2 100644 (file)
@@ -756,7 +756,8 @@ EXTEND
       | u = URI -> return_term loc (Ast.Uri (u, None))
       | r = NREF -> return_term loc (Ast.NRef (NReference.reference_of_string r))
       | n = NUMBER -> return_term loc (Ast.Num (n, 0))
-      | IMPLICIT -> return_term loc (Ast.Implicit)
+      | IMPLICIT -> return_term loc (Ast.Implicit `JustOne)
+      | IMPLICITVECTOR -> return_term loc (Ast.Implicit `Vector)
       | PLACEHOLDER -> return_term loc Ast.UserInput
       | m = META -> return_term loc (Ast.Meta (int_of_string m, []))
       | m = META; s = meta_substs ->
index 0e85618896833b254b52e12970ff81f6a3f96b72..23f62092496d16eb7b47dd086d0ba0b017671616 100644 (file)
@@ -36,7 +36,7 @@ let get_tag term0 =
   let subterms = ref [] in
   let map_term t =
     subterms := t :: !subterms ; 
-    Ast.Implicit
+    Ast.Implicit `JustOne
   in
   let rec aux t = 
     CicNotationUtil.visit_ast 
index 2544adb5d0deaec128f9d842a0768176f0a61e30..5e8f26a4f7758deb8816c37633b97e0b2b2d15b7 100644 (file)
@@ -253,7 +253,8 @@ let pp_ast0 t k =
           ((hvbox false false
             (fst_row :: List.flatten tl_rows
              @ [ break; keyword "in"; break; k where ])))
-    | Ast.Implicit -> builtin_symbol "?"
+    | Ast.Implicit `JustOne -> builtin_symbol "?"
+    | Ast.Implicit `Vector -> builtin_symbol "..."
     | Ast.Meta (n, l) ->
         let local_context l =
             List.map (function None -> None | Some t -> Some (k t)) l
@@ -596,7 +597,7 @@ let instantiate_level2 env term =
         Ast.Ident (name, Some (aux_substs env substs))
     | Ast.Meta (index, substs) -> Ast.Meta (index, aux_meta_substs env substs)
 
-    | Ast.Implicit
+    | Ast.Implicit _
     | Ast.Ident _
     | Ast.Num _
     | Ast.Sort _
index ca6146e5614011db63632dbea398e7a9bca109a4..354a737832bd15085e5ce8f89ec6f8fa25951cd0 100644 (file)
@@ -311,7 +311,7 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
             [ Node ([loc], Id name, terms) ]))
   | Ast.Uri _ -> []
   | Ast.NRef _ -> []
-  | Ast.Implicit -> []
+  | Ast.Implicit -> []
   | Ast.Num (num, i) -> [ Node ([loc], Num i, []) ]
   | Ast.Meta (index, local_context) ->
       List.fold_left
index 5ed2939488b82f7355296f08a26c01a3686f52c2..27748245654989ef634ad940b51a6b026ec3f6c7 100644 (file)
@@ -79,7 +79,7 @@ let mk_rec_corec ind_kind defs loc =
   let name,ty = 
     match defs with
     | (params,(N.Ident (name, None), ty),_,_) :: _ ->
-        let ty = match ty with Some ty -> ty | None -> N.Implicit in
+        let ty = match ty with Some ty -> ty | None -> N.Implicit `JustOne in
         let ty =
          List.fold_right
           (fun var ty -> N.Binder (`Pi,var,ty)
@@ -209,11 +209,11 @@ EXTEND
       let deannotate = function
         | N.AttributedTerm (_,t) | t -> t
       in match deannotate params with
-      | N.Implicit -> [false]
+      | N.Implicit -> [false]
       | N.UserInput -> [true]
       | N.Appl l -> 
          List.map (fun x -> match deannotate x with  
-           | N.Implicit -> false
+           | N.Implicit -> false
            | N.UserInput -> true
            | _ -> raise (Invalid_argument "malformed target parameter list 1")) l
       | _ -> raise (Invalid_argument ("malformed target parameter list 2\n" ^ CicNotationPp.pp_term params)) ]
@@ -789,7 +789,7 @@ EXTEND
         G.NObj (loc, N.Theorem (nflavour, name, typ, body))
     | nflavour = ntheorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
       body = term ->
-        G.NObj (loc, N.Theorem (nflavour, name, N.Implicit, Some body))
+        G.NObj (loc, N.Theorem (nflavour, name, N.Implicit `JustOne, Some body))
     | IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term ->
         G.NObj (loc, N.Theorem (`Axiom, name, typ, None))
     | NLETCOREC ; defs = let_defs -> 
@@ -859,7 +859,7 @@ EXTEND
     | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
       body = term ->
         G.Obj (loc,
-          N.Theorem (flavour, name, N.Implicit, Some body))
+          N.Theorem (flavour, name, N.Implicit `JustOne, Some body))
     | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
         G.Obj (loc, N.Theorem (`Axiom, name, typ, None))
     | LETCOREC ; defs = let_defs -> 
index 68733a8ef36a24328f80e98111da58ae297eadcc..c53a4a31c6ad0b7603f4dc8497323889012ea5c8 100644 (file)
@@ -93,7 +93,8 @@ let nast_of_cic0 status
        F.fprintf f ")"*)
     (* CSC: qua siamo grezzi *)
     | NCic.Implicit `Hole -> idref (Ast.UserInput)
-    | NCic.Implicit _ -> idref (Ast.Implicit)
+    | NCic.Implicit `Vector -> idref (Ast.Implicit `Vector)
+    | NCic.Implicit _ -> idref (Ast.Implicit `JustOne)
     | NCic.Prod (n,s,t) ->
         let n = if n.[0] = '_' then "_" else n in
         let binder_kind = `Forall in
index 5fa3b81887b9b7f17ff4fe52a23fb4ee6fb1b6da..b044b51d9a33a42973ec08c1c129116b7bdae47b 100644 (file)
@@ -324,7 +324,8 @@ let interpretate_term_and_interpretate_term_option
         with NRef.IllFormedReference _ ->
          CicNotationPt.fail loc "Ill formed reference")
     | CicNotationPt.NRef nref -> NCic.Const nref
-    | CicNotationPt.Implicit -> NCic.Implicit `Term
+    | CicNotationPt.Implicit `Vector -> NCic.Implicit `Vector
+    | CicNotationPt.Implicit `JustOne -> NCic.Implicit `Term
     | CicNotationPt.UserInput -> NCic.Implicit `Hole
     | CicNotationPt.Num (num, i) -> 
         Disambiguate.resolve ~env ~mk_choice (Num i) (`Num_arg num)
@@ -362,7 +363,8 @@ let interpretate_term_and_interpretate_term_option
         res
     | Some (CicNotationPt.AttributedTerm (_, term)) ->
         aux_option ~localize loc context annotation (Some term)
-    | Some CicNotationPt.Implicit -> NCic.Implicit annotation
+    | Some CicNotationPt.Implicit `JustOne -> NCic.Implicit annotation
+    | Some CicNotationPt.Implicit `Vector -> assert false
     | Some term -> aux ~localize loc context term
   in
    (fun ~context -> aux ~localize:true HExtlib.dummy_floc context),
@@ -493,7 +495,7 @@ let interpretate_obj
        (fun (context,res) (name,t) ->
          let t =
           match t with
-             None -> CicNotationPt.Implicit
+             None -> CicNotationPt.Implicit `JustOne
            | Some t -> t in
          let name = cic_name_of_name name in
          let t =
@@ -551,7 +553,7 @@ let interpretate_obj
        (fun (context,res) (name,t) ->
          let t =
           match t with
-             None -> CicNotationPt.Implicit
+             None -> CicNotationPt.Implicit `JustOne
            | Some t -> t in
          let name = cic_name_of_name name in
          let t =
index 97733891e8745b4e3251500878f4804abe1743ef..e520422160ab7fc77a41069b3970b960c4b2ca6d 100644 (file)
@@ -19,7 +19,8 @@ type universe = (bool * NUri.uri) list
 
 type sort = Prop | Type of universe
 
-type implicit_annotation = [ `Closed | `Type | `Hole | `Term | `Typeof of int ]
+type implicit_annotation =
+ [ `Closed | `Type | `Hole | `Term | `Typeof of int | `Vector ]
 
 type lc_kind = Irl of int | Ctx of term list
 
index 258e83c949da272dd1b412faa010fe5d7b558b4f..a7b6559a6520300c108b3167272264bce37f70cc 100644 (file)
@@ -60,6 +60,7 @@ let string_of_implicit_annotation = function
   | `Hole -> "□"
   | `Term -> "Term"
   | `Typeof x -> "Ty("^string_of_int x^")"
+  | `Vector -> "..."
 ;;
 
 let ppterm ~formatter:f ~context ~subst ~metasenv:_ ?(inside_fix=false) t =
index 4339b2860f42531eef867c1860a5536e0b44e586..0abff3a6c694727f79cc2e07eded3fd6ce48cc82 100644 (file)
@@ -98,7 +98,7 @@ let mk_elim uri leftno [it] (outsort,suffix) =
                       params @
                       [p_name] @
                       k_names @
-                      List.map (fun _ -> CicNotationPt.Implicit)
+                      List.map (fun _ -> CicNotationPt.Implicit `JustOne)
                        (List.tl args) @
                       [mk_appl (name::abs)])))
               | _ -> mk_id name,None
@@ -148,7 +148,8 @@ let mk_elim uri leftno [it] (outsort,suffix) =
      (function x::_ -> x | _ -> assert false) 80 
      (CicNotationPres.mpres_of_box boxml)));
 *)
-  CicNotationPt.Theorem (`Definition,srec_name,CicNotationPt.Implicit,Some res)
+  CicNotationPt.Theorem
+   (`Definition,srec_name,CicNotationPt.Implicit `JustOne,Some res)
 ;;
 
 let ast_of_sort s =
@@ -280,7 +281,8 @@ let mk_projection leftno tyname consname consty (projname,_,_) i =
      (function x::_ -> x | _ -> assert false)
      80 (CicNotationPres.render (fun _ -> None)
      (TermContentPres.pp_ast res)));*)
-  CicNotationPt.Theorem (`Definition,projname,CicNotationPt.Implicit,Some res)
+  CicNotationPt.Theorem
+   (`Definition,projname,CicNotationPt.Implicit `JustOne,Some res)
 ;;
 
 let mk_projections (_,_,_,_,obj) =
index 895d7c3f0666007e61a4b78f6c9d2b728d60eaa4..445ac030e7674e758998ac74543a84162b05e991 100644 (file)
@@ -303,7 +303,7 @@ let clear_tac names =
 
 let generalize0_tac args =
  if args = [] then id_tac
- else exact_tac ("",0,Ast.Appl (Ast.Implicit :: args))
+ else exact_tac ("",0,Ast.Appl (Ast.Implicit `JustOne :: args))
 ;;
 
 let select0_tac ~where:(wanted,hyps,where) ~job  =
@@ -429,7 +429,8 @@ let change_tac ~where ~with_what =
 let letin_tac ~where ~what:(_,_,w) name =
  block_tac [
   select_tac ~where ~job:(`Substexpand 1) true;
-  exact_tac ("",0,Ast.LetIn((Ast.Ident (name,None),None),w,Ast.Implicit));
+  exact_tac
+   ("",0,Ast.LetIn((Ast.Ident (name,None),None),w,Ast.Implicit `JustOne));
  ]
 ;;
 
@@ -486,7 +487,8 @@ let elim_tac ~what ~where =
        | _ -> assert false 
      in
      let holes = 
-       HExtlib.mk_list Ast.Implicit (ity.leftno+1+ ity.consno + ity.rightno) in
+      HExtlib.mk_list (Ast.Implicit `JustOne)
+       (ity.leftno+1+ ity.consno + ity.rightno) in
      let eliminator = 
        let _,_,w = what in
        Ast.Appl(Ast.Ident(name,None)::holes @ [ w ])
@@ -519,7 +521,7 @@ let rewrite_tac ~dir ~what:(_,_,what) ~where status =
    [ select_tac ~where ~job:(`Substexpand 1) true;
      exact_tac
       ("",0,
-       Ast.Appl(Ast.Ident(name,None)::HExtlib.mk_list Ast.Implicit 5 @
+       Ast.Appl(Ast.Ident(name,None)::HExtlib.mk_list (Ast.Implicit `JustOne) 5@
         [what]))] status
 ;;
 
@@ -527,7 +529,7 @@ let intro_tac name =
  block_tac
   [ exact_tac
      ("",0,(Ast.Binder (`Lambda,
-      (Ast.Ident (name,None),None),Ast.Implicit)));
+      (Ast.Ident (name,None),None),Ast.Implicit `JustOne)));
     if name = "_" then clear_tac [name] else id_tac ]
 ;;
 
index a19fa67c20d3281967d8ec77a754f84ede510a51..244cd1d728975ebc22f000402bf99e5e589329ea 100644 (file)
@@ -237,8 +237,9 @@ let ng_generate_tactics fv ueq_case context arities =
       (fun _ -> 
         [GA.Executable(floc,GA.NTactic(floc, 
           [GA.NApply (floc,
-            PT.Appl [mk_ident "ex_intro";PT.Implicit;PT.Implicit;
-              PT.Implicit;PT.Implicit]);GA.NBranch floc]));
+            PT.Appl
+             [mk_ident "ex_intro";PT.Implicit `JustOne;PT.Implicit `JustOne;
+              PT.Implicit `JustOne;PT.Implicit `JustOne]);GA.NBranch floc]));
          GA.Executable(floc,GA.NTactic(floc, 
           [GA.NPos (floc,[2])]))])
       fv)) 
index 2055bb9cdbe3c2a99c7ef25e4722bafbee87dd6e..bbe76859f3daf7f1ffffaba61175940114e47f85 100644 (file)
@@ -210,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)
@@ -220,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)