From: Claudio Sacerdoti Coen Date: Tue, 28 Jul 2009 15:17:51 +0000 (+0000) Subject: Introduction of vectors of implicit (only for NG). X-Git-Tag: make_still_working~3604 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d34061fd1c820139fad38c39dee6377e5057bf26;p=helm.git Introduction of vectors of implicit (only for NG). Proposed concrete syntax: "..." --- diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml index 5eb6b64d2..1e759930a 100644 --- a/helm/software/components/acic_content/cicNotationPp.ml +++ b/helm/software/components/acic_content/cicNotationPp.ml @@ -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 diff --git a/helm/software/components/acic_content/cicNotationPt.ml b/helm/software/components/acic_content/cicNotationPt.ml index 8dbfea799..75e580d00 100644 --- a/helm/software/components/acic_content/cicNotationPt.ml +++ b/helm/software/components/acic_content/cicNotationPt.ml @@ -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 diff --git a/helm/software/components/acic_content/cicNotationUtil.ml b/helm/software/components/acic_content/cicNotationUtil.ml index b426863cf..4e5917a15 100644 --- a/helm/software/components/acic_content/cicNotationUtil.ml +++ b/helm/software/components/acic_content/cicNotationUtil.ml @@ -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 _ diff --git a/helm/software/components/acic_content/termAcicContent.ml b/helm/software/components/acic_content/termAcicContent.ml index 81d0ef0a7..6eeb45749 100644 --- a/helm/software/components/acic_content/termAcicContent.ml +++ b/helm/software/components/acic_content/termAcicContent.ml @@ -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 diff --git a/helm/software/components/cic/cicUtil.ml b/helm/software/components/cic/cicUtil.ml index 36f65391e..9b6ece214 100644 --- a/helm/software/components/cic/cicUtil.ml +++ b/helm/software/components/cic/cicUtil.ml @@ -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 diff --git a/helm/software/components/cic_disambiguation/cicDisambiguate.ml b/helm/software/components/cic_disambiguation/cicDisambiguate.ml index cf59ab553..e52db62dd 100644 --- a/helm/software/components/cic_disambiguation/cicDisambiguate.ml +++ b/helm/software/components/cic_disambiguation/cicDisambiguate.ml @@ -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 diff --git a/helm/software/components/content_pres/cicNotationLexer.ml b/helm/software/components/content_pres/cicNotationLexer.ml index 21031d002..1dab53582 100644 --- a/helm/software/components/content_pres/cicNotationLexer.ml +++ b/helm/software/components/content_pres/cicNotationLexer.ml @@ -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) diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml index 7317f6139..2ac6b7e6a 100644 --- a/helm/software/components/content_pres/cicNotationParser.ml +++ b/helm/software/components/content_pres/cicNotationParser.ml @@ -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 -> diff --git a/helm/software/components/content_pres/content2presMatcher.ml b/helm/software/components/content_pres/content2presMatcher.ml index 0e8561889..23f620924 100644 --- a/helm/software/components/content_pres/content2presMatcher.ml +++ b/helm/software/components/content_pres/content2presMatcher.ml @@ -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 diff --git a/helm/software/components/content_pres/termContentPres.ml b/helm/software/components/content_pres/termContentPres.ml index 2544adb5d..5e8f26a4f 100644 --- a/helm/software/components/content_pres/termContentPres.ml +++ b/helm/software/components/content_pres/termContentPres.ml @@ -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 _ diff --git a/helm/software/components/disambiguation/disambiguate.ml b/helm/software/components/disambiguation/disambiguate.ml index ca6146e56..354a73783 100644 --- a/helm/software/components/disambiguation/disambiguate.ml +++ b/helm/software/components/disambiguation/disambiguate.ml @@ -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 diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 5ed293948..277482456 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -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> (* ≝ *); 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> (* ≝ *); 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 -> diff --git a/helm/software/components/ng_cic_content/nTermCicContent.ml b/helm/software/components/ng_cic_content/nTermCicContent.ml index 68733a8ef..c53a4a31c 100644 --- a/helm/software/components/ng_cic_content/nTermCicContent.ml +++ b/helm/software/components/ng_cic_content/nTermCicContent.ml @@ -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 diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml index 5fa3b8188..b044b51d9 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml @@ -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 = diff --git a/helm/software/components/ng_kernel/nCic.ml b/helm/software/components/ng_kernel/nCic.ml index 97733891e..e52042216 100644 --- a/helm/software/components/ng_kernel/nCic.ml +++ b/helm/software/components/ng_kernel/nCic.ml @@ -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 diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml index 258e83c94..a7b6559a6 100644 --- a/helm/software/components/ng_kernel/nCicPp.ml +++ b/helm/software/components/ng_kernel/nCicPp.ml @@ -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 = diff --git a/helm/software/components/ng_tactics/nCicElim.ml b/helm/software/components/ng_tactics/nCicElim.ml index 4339b2860..0abff3a6c 100644 --- a/helm/software/components/ng_tactics/nCicElim.ml +++ b/helm/software/components/ng_tactics/nCicElim.ml @@ -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) = diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index 895d7c3f0..445ac030e 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -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 ] ;; diff --git a/helm/software/components/tptp_grafite/tptp2grafite.ml b/helm/software/components/tptp_grafite/tptp2grafite.ml index a19fa67c2..244cd1d72 100644 --- a/helm/software/components/tptp_grafite/tptp2grafite.ml +++ b/helm/software/components/tptp_grafite/tptp2grafite.ml @@ -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)) diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index 2055bb9cd..bbe76859f 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/matita/matitaScript.ml @@ -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)