diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/classops.ml | 4 | ||||
| -rw-r--r-- | pretyping/detyping.ml | 32 | ||||
| -rw-r--r-- | pretyping/evarconv.ml | 4 | ||||
| -rw-r--r-- | pretyping/extend.ml | 134 | ||||
| -rw-r--r-- | pretyping/glob_ops.ml | 14 | ||||
| -rw-r--r-- | pretyping/indrec.ml | 4 | ||||
| -rw-r--r-- | pretyping/patternops.ml | 18 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 10 | ||||
| -rw-r--r-- | pretyping/pretyping.mllib | 2 | ||||
| -rw-r--r-- | pretyping/recordops.ml | 4 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 12 | ||||
| -rw-r--r-- | pretyping/typeclasses.ml | 18 | ||||
| -rw-r--r-- | pretyping/unification.ml | 16 | ||||
| -rw-r--r-- | pretyping/vernacexpr.ml | 529 |
14 files changed, 63 insertions, 738 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml index afa8a12fc0..7dbef01c22 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -316,7 +316,7 @@ let lookup_pattern_path_between env (s,t) = let coercion_value { coe_value = c; coe_type = t; coe_context = ctx; coe_is_identity = b; coe_is_projection = b' } = - let subst, ctx = Universes.fresh_universe_context_set_instance ctx in + let subst, ctx = UnivGen.fresh_universe_context_set_instance ctx in let c' = Vars.subst_univs_level_constr subst c and t' = Vars.subst_univs_level_constr subst t in (make_judge (EConstr.of_constr c') (EConstr.of_constr t'), b, b'), ctx @@ -440,7 +440,7 @@ let cache_coercion env sigma (_, c) = let () = add_class c.coercion_target in let is, _ = class_info c.coercion_source in let it, _ = class_info c.coercion_target in - let value, ctx = Universes.fresh_global_instance env c.coercion_type in + let value, ctx = UnivGen.fresh_global_instance env c.coercion_type in let typ = Retyping.get_type_of env sigma (EConstr.of_constr value) in let typ = EConstr.Unsafe.to_constr typ in let xf = diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 56e5828918..7795084779 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -920,7 +920,7 @@ let rec subst_cases_pattern subst = DAst.map (function | PatVar _ as pat -> pat | PatCstr (((kn,i),j),cpl,n) as pat -> let kn' = subst_mind subst kn - and cpl' = List.smartmap (subst_cases_pattern subst) cpl in + and cpl' = List.Smart.map (subst_cases_pattern subst) cpl in if kn' == kn && cpl' == cpl then pat else PatCstr (((kn',i),j),cpl',n) ) @@ -940,7 +940,7 @@ let rec subst_glob_constr subst = DAst.map (function | GApp (r,rl) as raw -> let r' = subst_glob_constr subst r - and rl' = List.smartmap (subst_glob_constr subst) rl in + and rl' = List.Smart.map (subst_glob_constr subst) rl in if r' == r && rl' == rl then raw else GApp(r',rl') @@ -957,25 +957,25 @@ let rec subst_glob_constr subst = DAst.map (function | GLetIn (n,r1,t,r2) as raw -> let r1' = subst_glob_constr subst r1 in let r2' = subst_glob_constr subst r2 in - let t' = Option.smartmap (subst_glob_constr subst) t in + let t' = Option.Smart.map (subst_glob_constr subst) t in if r1' == r1 && t == t' && r2' == r2 then raw else GLetIn (n,r1',t',r2') | GCases (sty,rtno,rl,branches) as raw -> let open CAst in - let rtno' = Option.smartmap (subst_glob_constr subst) rtno - and rl' = List.smartmap (fun (a,x as y) -> + let rtno' = Option.Smart.map (subst_glob_constr subst) rtno + and rl' = List.Smart.map (fun (a,x as y) -> let a' = subst_glob_constr subst a in let (n,topt) = x in - let topt' = Option.smartmap + let topt' = Option.Smart.map (fun ({loc;v=((sp,i),y)} as t) -> let sp' = subst_mind subst sp in if sp == sp' then t else CAst.(make ?loc ((sp',i),y))) topt in if a == a' && topt == topt' then y else (a',(n,topt'))) rl - and branches' = List.smartmap + and branches' = List.Smart.map (fun ({loc;v=(idl,cpl,r)} as branch) -> let cpl' = - List.smartmap (subst_cases_pattern subst) cpl + List.Smart.map (subst_cases_pattern subst) cpl and r' = subst_glob_constr subst r in if cpl' == cpl && r' == r then branch else CAst.(make ?loc (idl,cpl',r'))) @@ -985,14 +985,14 @@ let rec subst_glob_constr subst = DAst.map (function GCases (sty,rtno',rl',branches') | GLetTuple (nal,(na,po),b,c) as raw -> - let po' = Option.smartmap (subst_glob_constr subst) po + let po' = Option.Smart.map (subst_glob_constr subst) po and b' = subst_glob_constr subst b and c' = subst_glob_constr subst c in if po' == po && b' == b && c' == c then raw else GLetTuple (nal,(na,po'),b',c') | GIf (c,(na,po),b1,b2) as raw -> - let po' = Option.smartmap (subst_glob_constr subst) po + let po' = Option.Smart.map (subst_glob_constr subst) po and b1' = subst_glob_constr subst b1 and b2' = subst_glob_constr subst b2 and c' = subst_glob_constr subst c in @@ -1000,12 +1000,12 @@ let rec subst_glob_constr subst = DAst.map (function GIf (c',(na,po'),b1',b2') | GRec (fix,ida,bl,ra1,ra2) as raw -> - let ra1' = Array.smartmap (subst_glob_constr subst) ra1 - and ra2' = Array.smartmap (subst_glob_constr subst) ra2 in - let bl' = Array.smartmap - (List.smartmap (fun (na,k,obd,ty as dcl) -> + let ra1' = Array.Smart.map (subst_glob_constr subst) ra1 + and ra2' = Array.Smart.map (subst_glob_constr subst) ra2 in + let bl' = Array.Smart.map + (List.Smart.map (fun (na,k,obd,ty as dcl) -> let ty' = subst_glob_constr subst ty in - let obd' = Option.smartmap (subst_glob_constr subst) obd in + let obd' = Option.Smart.map (subst_glob_constr subst) obd in if ty'==ty && obd'==obd then dcl else (na,k,obd',ty'))) bl in if ra1' == ra1 && ra2' == ra2 && bl'==bl then raw else @@ -1018,7 +1018,7 @@ let rec subst_glob_constr subst = DAst.map (function if nref == ref then knd else Evar_kinds.ImplicitArg (nref, i, b) | _ -> knd in - let nsolve = Option.smartmap (Hook.get f_subst_genarg subst) solve in + let nsolve = Option.Smart.map (Hook.get f_subst_genarg subst) solve in if nsolve == solve && nknd == knd then raw else GHole (nknd, naming, nsolve) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 49c429458a..062136ff52 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -49,7 +49,7 @@ let _ = Goptions.declare_bool_option { (* XXX: we would like to search for this with late binding "data.id.type" etc... *) let impossible_default_case () = - let c, ctx = Universes.fresh_global_instance (Global.env()) (Globnames.ConstRef Coqlib.id) in + let c, ctx = UnivGen.fresh_global_instance (Global.env()) (Globnames.ConstRef Coqlib.id) in let (_, u) = Constr.destConst c in Some (c, Constr.mkConstU (Coqlib.type_of_id, u), ctx) @@ -210,7 +210,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = else match (Stack.strip_n_app (l_us-1) sk2_effective) with | None -> raise Not_found | Some (l',el,s') -> (l'@Stack.append_app [|el|] Stack.empty,s') in - let u, ctx' = Universes.fresh_instance_from ctx None in + let u, ctx' = UnivGen.fresh_instance_from ctx None in let subst = Univ.make_inverse_instance_subst u in let c = EConstr.of_constr c in let c' = subst_univs_level_constr subst c in diff --git a/pretyping/extend.ml b/pretyping/extend.ml deleted file mode 100644 index 734b859f60..0000000000 --- a/pretyping/extend.ml +++ /dev/null @@ -1,134 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(** Entry keys for constr notations *) - -type 'a entry = 'a Grammar.GMake(CLexer).Entry.e - -type side = Left | Right - -type gram_assoc = NonA | RightA | LeftA - -type gram_position = - | First - | Last - | Before of string - | After of string - | Level of string - -type production_position = - | BorderProd of side * gram_assoc option - | InternalProd - -type production_level = - | NextLevel - | NumLevel of int - -type constr_as_binder_kind = - | AsIdent - | AsIdentOrPattern - | AsStrictPattern - -(** User-level types used to tell how to parse or interpret of the non-terminal *) - -type 'a constr_entry_key_gen = - | ETName - | ETReference - | ETBigint - | ETBinder of bool (* open list of binders if true, closed list of binders otherwise *) - | ETConstr of 'a - | ETConstrAsBinder of constr_as_binder_kind * 'a - | ETPattern of bool * int option (* true = strict pattern, i.e. not a single variable *) - | ETOther of string * string - -(** Entries level (left-hand side of grammar rules) *) - -type constr_entry_key = - (production_level * production_position) constr_entry_key_gen - -(** Entries used in productions, vernac side (e.g. "x bigint" or "x ident") *) - -type simple_constr_prod_entry_key = - production_level option constr_entry_key_gen - -(** Entries used in productions (in right-hand-side of grammar rules), to parse non-terminals *) - -type binder_entry_kind = ETBinderOpen | ETBinderClosed of Tok.t list - -type binder_target = ForBinder | ForTerm - -type constr_prod_entry_key = - | ETProdName (* Parsed as a name (ident or _) *) - | ETProdReference (* Parsed as a global reference *) - | ETProdBigint (* Parsed as an (unbounded) integer *) - | ETProdConstr of (production_level * production_position) (* Parsed as constr or pattern *) - | ETProdPattern of int (* Parsed as pattern as a binder (as subpart of a constr) *) - | ETProdOther of string * string (* Intended for embedding custom entries in constr or pattern *) - | ETProdConstrList of (production_level * production_position) * Tok.t list (* Parsed as non-empty list of constr *) - | ETProdBinderList of binder_entry_kind (* Parsed as non-empty list of local binders *) - -(** {5 AST for user-provided entries} *) - -type 'a user_symbol = -| Ulist1 of 'a user_symbol -| Ulist1sep of 'a user_symbol * string -| Ulist0 of 'a user_symbol -| Ulist0sep of 'a user_symbol * string -| Uopt of 'a user_symbol -| Uentry of 'a -| Uentryl of 'a * int - -type ('a,'b,'c) ty_user_symbol = -| TUlist1 : ('a,'b,'c) ty_user_symbol -> ('a list,'b list,'c list) ty_user_symbol -| TUlist1sep : ('a,'b,'c) ty_user_symbol * string -> ('a list,'b list,'c list) ty_user_symbol -| TUlist0 : ('a,'b,'c) ty_user_symbol -> ('a list,'b list,'c list) ty_user_symbol -| TUlist0sep : ('a,'b,'c) ty_user_symbol * string -> ('a list,'b list,'c list) ty_user_symbol -| TUopt : ('a,'b,'c) ty_user_symbol -> ('a option, 'b option, 'c option) ty_user_symbol -| TUentry : ('a, 'b, 'c) Genarg.ArgT.tag -> ('a,'b,'c) ty_user_symbol -| TUentryl : ('a, 'b, 'c) Genarg.ArgT.tag * int -> ('a,'b,'c) ty_user_symbol - -(** {5 Type-safe grammar extension} *) - -type ('self, 'a) symbol = -| Atoken : Tok.t -> ('self, string) symbol -| Alist1 : ('self, 'a) symbol -> ('self, 'a list) symbol -| Alist1sep : ('self, 'a) symbol * ('self, _) symbol -> ('self, 'a list) symbol -| Alist0 : ('self, 'a) symbol -> ('self, 'a list) symbol -| Alist0sep : ('self, 'a) symbol * ('self, _) symbol -> ('self, 'a list) symbol -| Aopt : ('self, 'a) symbol -> ('self, 'a option) symbol -| Aself : ('self, 'self) symbol -| Anext : ('self, 'self) symbol -| Aentry : 'a entry -> ('self, 'a) symbol -| Aentryl : 'a entry * int -> ('self, 'a) symbol -| Arules : 'a rules list -> ('self, 'a) symbol - -and ('self, _, 'r) rule = -| Stop : ('self, 'r, 'r) rule -| Next : ('self, 'a, 'r) rule * ('self, 'b) symbol -> ('self, 'b -> 'a, 'r) rule - -and ('a, 'r) norec_rule = { norec_rule : 's. ('s, 'a, 'r) rule } - -and 'a rules = -| Rules : ('act, Loc.t -> 'a) norec_rule * 'act -> 'a rules - -type 'a production_rule = -| Rule : ('a, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule - -type 'a single_extend_statment = - string option * - (** Level *) - gram_assoc option * - (** Associativity *) - 'a production_rule list - (** Symbol list with the interpretation function *) - -type 'a extend_statment = - gram_position option * - 'a single_extend_statment list diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 3ae04cd4fa..5056c0457e 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -331,19 +331,19 @@ let bound_glob_vars = (** Mapping of names in binders *) -(* spiwack: I used a smartmap-style kind of mapping here, because the +(* spiwack: I used a smart-style kind of mapping here, because the operation will be the identity almost all of the time (with any term outside of Ltac to begin with). But to be honest, there would probably be no significant penalty in doing reallocation as pattern-matching expressions are usually rather small. *) let map_inpattern_binders f ({loc;v=(id,nal)} as x) = - let r = CList.smartmap f nal in + let r = CList.Smart.map f nal in if r == nal then x else CAst.make ?loc (id,r) let map_tomatch_binders f ((c,(na,inp)) as x) : tomatch_tuple = - let r = Option.smartmap (fun p -> map_inpattern_binders f p) inp in + let r = Option.Smart.map (fun p -> map_inpattern_binders f p) inp in if r == inp then x else c,(f na, r) @@ -355,7 +355,7 @@ let rec map_case_pattern_binders f = DAst.map (function | PatCstr (c,ps,na) as x -> let rna = f na in let rps = - CList.smartmap (fun p -> map_case_pattern_binders f p) ps + CList.Smart.map (fun p -> map_case_pattern_binders f p) ps in if rna == na && rps == ps then x else PatCstr(c,rps,rna) @@ -366,13 +366,13 @@ let map_cases_branch_binders f ({CAst.loc;v=(il,cll,rhs)} as x) : cases_clause = It is intended to be a superset of the free variable of the right-hand side, if I understand correctly. But I'm not sure when or how they are used. *) - let r = List.smartmap (fun cl -> map_case_pattern_binders f cl) cll in + let r = List.Smart.map (fun cl -> map_case_pattern_binders f cl) cll in if r == cll then x else CAst.make ?loc (il,r,rhs) let map_pattern_binders f tomatch branches = - CList.smartmap (fun tm -> map_tomatch_binders f tm) tomatch, - CList.smartmap (fun br -> map_cases_branch_binders f br) branches + CList.Smart.map (fun tm -> map_tomatch_binders f tm) tomatch, + CList.Smart.map (fun br -> map_cases_branch_binders f br) branches (** /mapping of names in binders *) diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 3327c250d7..40f4d4ff89 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -86,7 +86,7 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind = if not (Sorts.List.mem kind (elim_sorts specif)) then raise (RecursionSchemeError - (NotAllowedCaseAnalysis (false, fst (Universes.fresh_sort_in_family env kind), pind))) + (NotAllowedCaseAnalysis (false, fst (UnivGen.fresh_sort_in_family env kind), pind))) in let ndepar = mip.mind_nrealdecls + 1 in @@ -550,7 +550,7 @@ let check_arities env listdepkind = let kelim = elim_sorts (mibi,mipi) in if not (Sorts.List.mem kind kelim) then raise (RecursionSchemeError - (NotAllowedCaseAnalysis (true, fst (Universes.fresh_sort_in_family env + (NotAllowedCaseAnalysis (true, fst (UnivGen.fresh_sort_in_family env kind),(mind,u)))) else if Int.List.mem ni ln then raise (RecursionSchemeError (NotMutualInScheme (mind,mind))) diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index ccfb7f9900..375ed10d0d 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -293,11 +293,11 @@ let rec subst_pattern subst pat = PProj(p',c') | PApp (f,args) -> let f' = subst_pattern subst f in - let args' = Array.smartmap (subst_pattern subst) args in + let args' = Array.Smart.map (subst_pattern subst) args in if f' == f && args' == args then pat else PApp (f',args') | PSoApp (i,args) -> - let args' = List.smartmap (subst_pattern subst) args in + let args' = List.Smart.map (subst_pattern subst) args in if args' == args then pat else PSoApp (i,args') | PLambda (name,c1,c2) -> @@ -312,7 +312,7 @@ let rec subst_pattern subst pat = PProd (name,c1',c2') | PLetIn (name,c1,t,c2) -> let c1' = subst_pattern subst c1 in - let t' = Option.smartmap (subst_pattern subst) t in + let t' = Option.Smart.map (subst_pattern subst) t in let c2' = subst_pattern subst c2 in if c1' == c1 && t' == t && c2' == c2 then pat else PLetIn (name,c1',t',c2') @@ -326,7 +326,7 @@ let rec subst_pattern subst pat = PIf (c',c1',c2') | PCase (cip,typ,c,branches) -> let ind = cip.cip_ind in - let ind' = Option.smartmap (subst_ind subst) ind in + let ind' = Option.Smart.map (subst_ind subst) ind in let cip' = if ind' == ind then cip else { cip with cip_ind = ind' } in let typ' = subst_pattern subst typ in let c' = subst_pattern subst c in @@ -334,18 +334,18 @@ let rec subst_pattern subst pat = let c' = subst_pattern subst c in if c' == c then br else (i,n,c') in - let branches' = List.smartmap subst_branch branches in + let branches' = List.Smart.map subst_branch branches in if cip' == cip && typ' == typ && c' == c && branches' == branches then pat else PCase(cip', typ', c', branches') | PFix (lni,(lna,tl,bl)) -> - let tl' = Array.smartmap (subst_pattern subst) tl in - let bl' = Array.smartmap (subst_pattern subst) bl in + let tl' = Array.Smart.map (subst_pattern subst) tl in + let bl' = Array.Smart.map (subst_pattern subst) bl in if bl' == bl && tl' == tl then pat else PFix (lni,(lna,tl',bl')) | PCoFix (ln,(lna,tl,bl)) -> - let tl' = Array.smartmap (subst_pattern subst) tl in - let bl' = Array.smartmap (subst_pattern subst) bl in + let tl' = Array.Smart.map (subst_pattern subst) tl in + let bl' = Array.Smart.map (subst_pattern subst) bl in if bl' == bl && tl' == tl then pat else PCoFix (ln,(lna,tl',bl')) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 616ccf0cfb..de72f94272 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -169,14 +169,6 @@ let _ = optread = is_strict_universe_declarations; optwrite = (:=) strict_universe_declarations }) -let _ = - Goptions.(declare_bool_option - { optdepr = false; - optname = "minimization to Set"; - optkey = ["Universe";"Minimization";"ToSet"]; - optread = Universes.is_set_minimization; - optwrite = (:=) Universes.set_minimization }) - (** Miscellaneous interpretation functions *) let interp_known_universe_level evd r = @@ -429,7 +421,7 @@ let ltac_interp_name_env k0 lvar env sigma = let n = Context.Rel.length (rel_context env) - k0 in let ctxt,_ = List.chop n (rel_context env) in let open Context.Rel.Declaration in - let ctxt' = List.smartmap (map_name (ltac_interp_name lvar)) ctxt in + let ctxt' = List.Smart.map (map_name (ltac_interp_name lvar)) ctxt in if List.equal (fun d1 d2 -> Name.equal (get_name d1) (get_name d2)) ctxt ctxt' then env else push_rel_context sigma ctxt' (pop_rel_context n env sigma) diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index d98026bc60..c48decdb08 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -27,8 +27,6 @@ Pattern Patternops Constr_matching Tacred -Extend -Vernacexpr Typeclasses_errors Typeclasses Classops diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 84aceeedd4..9eb410f06a 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -69,8 +69,8 @@ let subst_structure (subst,((kn,i),id,kl,projs as obj)) = let projs' = (* invariant: struc.s_PROJ is an evaluable reference. Thus we can take *) (* the first component of subst_con. *) - List.smartmap - (Option.smartmap (fun kn -> fst (subst_con_kn subst kn))) + List.Smart.map + (Option.Smart.map (fun kn -> fst (subst_con_kn subst kn))) projs in let id' = fst (subst_constructor subst id) in diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index a4d4479026..6fde868370 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -83,7 +83,7 @@ let declare_reduction_effect funkey f = (** A function to set the value of the print function *) let set_reduction_effect x funkey = - let termkey = Universes.constr_of_global x in + let termkey = UnivGen.constr_of_global x in Lib.add_anonymous_leaf (inReductionEffect (termkey,funkey)) @@ -701,18 +701,18 @@ let reducible_mind_case sigma c = match EConstr.kind sigma c with let magicaly_constant_of_fixbody env sigma reference bd = function | Name.Anonymous -> bd | Name.Name id -> - let open Universes in + let open UnivProblem in try let (cst_mod,cst_sect,_) = Constant.repr3 reference in let cst = Constant.make3 cst_mod cst_sect (Label.of_id id) in - let (cst, u), ctx = fresh_constant_instance env cst in + let (cst, u), ctx = UnivGen.fresh_constant_instance env cst in match constant_opt_value_in env (cst,u) with | None -> bd | Some t -> let csts = EConstr.eq_constr_universes env sigma (EConstr.of_constr t) bd in begin match csts with | Some csts -> - let subst = Constraints.fold (fun cst acc -> + let subst = Set.fold (fun cst acc -> let l, r = match cst with | ULub (u, v) | UWeak (u, v) -> u, v | UEq (u, v) | ULe (u, v) -> @@ -1404,7 +1404,7 @@ let plain_instance sigma s c = | Meta p -> (try lift n (Metamap.find p s) with Not_found -> u) | App (f,l) when isCast sigma f -> let (f,_,t) = destCast sigma f in - let l' = CArray.Fun1.smartmap irec n l in + let l' = Array.Fun1.Smart.map irec n l in (match EConstr.kind sigma f with | Meta p -> (* Don't flatten application nodes: this is used to extract a @@ -1413,7 +1413,7 @@ let plain_instance sigma s c = (try let g = Metamap.find p s in match EConstr.kind sigma g with | App _ -> - let l' = CArray.Fun1.smartmap lift 1 l' in + let l' = Array.Fun1.Smart.map lift 1 l' in mkLetIn (Name default_plain_instance_ident,g,t,mkApp(mkRel 1, l')) | _ -> mkApp (g,l') with Not_found -> mkApp (f,l')) diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 4386144fe2..12a944d322 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -180,12 +180,12 @@ let subst_class (subst,cl) = let do_subst_con c = Mod_subst.subst_constant subst c and do_subst c = Mod_subst.subst_mps subst c and do_subst_gr gr = fst (subst_global subst gr) in - let do_subst_ctx = List.smartmap (RelDecl.map_constr do_subst) in + let do_subst_ctx = List.Smart.map (RelDecl.map_constr do_subst) in let do_subst_context (grs,ctx) = - List.smartmap (Option.smartmap do_subst_gr) grs, + List.Smart.map (Option.Smart.map do_subst_gr) grs, do_subst_ctx ctx in - let do_subst_projs projs = List.smartmap (fun (x, y, z) -> - (x, y, Option.smartmap do_subst_con z)) projs in + let do_subst_projs projs = List.Smart.map (fun (x, y, z) -> + (x, y, Option.Smart.map do_subst_con z)) projs in { cl_univs = cl.cl_univs; cl_impl = do_subst_gr cl.cl_impl; cl_context = do_subst_context cl.cl_context; @@ -223,7 +223,7 @@ let discharge_class (_,cl) = | Some (_, ((tc,_), _)) -> Some tc.cl_impl) ctx' in - List.smartmap (Option.smartmap Lib.discharge_global) grs + List.Smart.map (Option.Smart.map Lib.discharge_global) grs @ newgrs in grs', discharge_rel_context subst 1 ctx @ ctx' in let cl_impl' = Lib.discharge_global cl.cl_impl in @@ -234,12 +234,12 @@ let discharge_class (_,cl) = let usubst, cl_univs' = Lib.discharge_abstract_universe_context info cl.cl_univs in let context = discharge_context ctx (subst, usubst) cl.cl_context in let props = discharge_rel_context (subst, usubst) (succ (List.length (fst cl.cl_context))) cl.cl_props in - let discharge_proj (x, y, z) = x, y, Option.smartmap Lib.discharge_con z in + let discharge_proj (x, y, z) = x, y, Option.Smart.map Lib.discharge_con z in { cl_univs = cl_univs'; cl_impl = cl_impl'; cl_context = context; cl_props = props; - cl_projs = List.smartmap discharge_proj cl.cl_projs; + cl_projs = List.Smart.map discharge_proj cl.cl_projs; cl_strict = cl.cl_strict; cl_unique = cl.cl_unique } @@ -281,7 +281,7 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } = Nameops.add_suffix _id ("_subinstance_" ^ string_of_int !i)) in let ty, ctx = Global.type_of_global_in_context env glob in - let inst, ctx = Universes.fresh_instance_from ctx None in + let inst, ctx = UnivGen.fresh_instance_from ctx None in let ty = Vars.subst_instance_constr inst ty in let ty = EConstr.of_constr ty in let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in @@ -321,7 +321,7 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } = hints @ (path', info, body) :: rest in List.fold_left declare_proj [] projs in - let term = Universes.constr_of_global_univ (glob, inst) in + let term = UnivGen.constr_of_global_univ (glob, inst) in (*FIXME subclasses should now get substituted for each particular instance of the polymorphic superclass *) aux pri term ty [glob] diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 1caa629ffb..62bee5a362 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -561,16 +561,16 @@ let is_rigid_head sigma flags t = | Proj (_, _) -> false (* Why aren't Prod, Sort rigid heads ? *) let force_eqs c = - let open Universes in - Constraints.fold + let open UnivProblem in + Set.fold (fun c acc -> let c' = match c with (* Should we be forcing weak constraints? *) | ULub (l, r) | UWeak (l, r) -> UEq (Univ.Universe.make l,Univ.Universe.make r) | ULe _ | UEq _ -> c in - Constraints.add c' acc) - c Constraints.empty + Set.add c' acc) + c Set.empty let constr_cmp pb env sigma flags t u = let cstrs = @@ -1504,8 +1504,7 @@ let indirectly_dependent sigma c d decls = let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env current_sigma (pending,c) = let sigma = Pretyping.solve_remaining_evars flags env current_sigma pending in - let sigma, subst = nf_univ_variables sigma in - (sigma, EConstr.of_constr (Universes.subst_univs_constr subst (EConstr.Unsafe.to_constr (nf_evar sigma c)))) + (sigma, nf_evar sigma c) let default_matching_core_flags sigma = let ts = Names.full_transparent_state in { @@ -1593,9 +1592,8 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) = (fun test -> match test.testing_state with | None -> None | Some (sigma,_,l) -> - let c = applist (nf_evar sigma (local_strong whd_meta sigma c), l) in - let univs, subst = nf_univ_variables sigma in - Some (sigma,EConstr.of_constr (Universes.subst_univs_constr subst (EConstr.Unsafe.to_constr c)))) + let c = applist (local_strong whd_meta sigma c, l) in + Some (sigma, c)) let make_eq_test env evd c = let out cstr = diff --git a/pretyping/vernacexpr.ml b/pretyping/vernacexpr.ml deleted file mode 100644 index e15c3ad042..0000000000 --- a/pretyping/vernacexpr.ml +++ /dev/null @@ -1,529 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Names -open Misctypes -open Constrexpr -open Libnames - -(** Vernac expressions, produced by the parser *) -type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation - -type goal_selector = Goal_select.t = - | SelectAlreadyFocused - | SelectNth of int - | SelectList of (int * int) list - | SelectId of Id.t - | SelectAll -[@@ocaml.deprecated "Use Goal_select.t"] - -type goal_identifier = string -type scope_name = string - -type goal_reference = - | OpenSubgoals - | NthGoal of int - | GoalId of Id.t - -type univ_name_list = Universes.univ_name_list -[@@ocaml.deprecated "Use [Universes.univ_name_list]"] - -type printable = - | PrintTables - | PrintFullContext - | PrintSectionContext of reference - | PrintInspect of int - | PrintGrammar of string - | PrintLoadPath of DirPath.t option - | PrintModules - | PrintModule of reference - | PrintModuleType of reference - | PrintNamespace of DirPath.t - | PrintMLLoadPath - | PrintMLModules - | PrintDebugGC - | PrintName of reference or_by_notation * Universes.univ_name_list option - | PrintGraph - | PrintClasses - | PrintTypeClasses - | PrintInstances of reference or_by_notation - | PrintCoercions - | PrintCoercionPaths of class_rawexpr * class_rawexpr - | PrintCanonicalConversions - | PrintUniverses of bool * string option - | PrintHint of reference or_by_notation - | PrintHintGoal - | PrintHintDbName of string - | PrintHintDb - | PrintScopes - | PrintScope of string - | PrintVisibility of string option - | PrintAbout of reference or_by_notation * Universes.univ_name_list option * Goal_select.t option - | PrintImplicit of reference or_by_notation - | PrintAssumptions of bool * bool * reference or_by_notation - | PrintStrategy of reference or_by_notation option - -type search_about_item = - | SearchSubPattern of constr_pattern_expr - | SearchString of string * scope_name option - -type searchable = - | SearchPattern of constr_pattern_expr - | SearchRewrite of constr_pattern_expr - | SearchHead of constr_pattern_expr - | SearchAbout of (bool * search_about_item) list - -type locatable = - | LocateAny of reference or_by_notation - | LocateTerm of reference or_by_notation - | LocateLibrary of reference - | LocateModule of reference - | LocateOther of string * reference - | LocateFile of string - -type showable = - | ShowGoal of goal_reference - | ShowProof - | ShowScript - | ShowExistentials - | ShowUniverses - | ShowProofNames - | ShowIntros of bool - | ShowMatch of reference - -type comment = - | CommentConstr of constr_expr - | CommentString of string - | CommentInt of int - -type reference_or_constr = - | HintsReference of reference - | HintsConstr of constr_expr - -type hint_mode = - | ModeInput (* No evars *) - | ModeNoHeadEvar (* No evar at the head *) - | ModeOutput (* Anything *) - -type 'a hint_info_gen = 'a Typeclasses.hint_info_gen = - { hint_priority : int option; - hint_pattern : 'a option } -[@@ocaml.deprecated "Please use [Typeclasses.hint_info_gen]"] - -type hint_info_expr = Typeclasses.hint_info_expr -[@@ocaml.deprecated "Please use [Typeclasses.hint_info_expr]"] - -type hints_expr = - | HintsResolve of (Typeclasses.hint_info_expr * bool * reference_or_constr) list - | HintsImmediate of reference_or_constr list - | HintsUnfold of reference list - | HintsTransparency of reference list * bool - | HintsMode of reference * hint_mode list - | HintsConstructors of reference list - | HintsExtern of int * constr_expr option * Genarg.raw_generic_argument - -type search_restriction = - | SearchInside of reference list - | SearchOutside of reference list - -type rec_flag = bool (* true = Rec; false = NoRec *) -type verbose_flag = bool (* true = Verbose; false = Silent *) -type opacity_flag = Opaque | Transparent -type coercion_flag = bool (* true = AddCoercion false = NoCoercion *) -type instance_flag = bool option - (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *) -type export_flag = bool (* true = Export; false = Import *) -type inductive_flag = Declarations.recursivity_kind -type onlyparsing_flag = Flags.compat_version option - (* Some v = Parse only; None = Print also. - If v<>Current, it contains the name of the coq version - which this notation is trying to be compatible with *) -type locality_flag = bool (* true = Local *) - -type option_value = Goptions.option_value = - | BoolValue of bool - | IntValue of int option - | StringValue of string - | StringOptValue of string option - -type option_ref_value = - | StringRefValue of string - | QualidRefValue of reference - -(** Identifier and optional list of bound universes and constraints. *) - -type sort_expr = Sorts.family - -type definition_expr = - | ProveBody of local_binder_expr list * constr_expr - | DefineBody of local_binder_expr list * Genredexpr.raw_red_expr option * constr_expr - * constr_expr option - -type fixpoint_expr = - ident_decl * (lident option * recursion_order_expr) * local_binder_expr list * constr_expr * constr_expr option - -type cofixpoint_expr = - ident_decl * local_binder_expr list * constr_expr * constr_expr option - -type local_decl_expr = - | AssumExpr of lname * constr_expr - | DefExpr of lname * constr_expr * constr_expr option - -type inductive_kind = Inductive_kw | CoInductive | Variant | Record | Structure | Class of bool (* true = definitional, false = inductive *) -type decl_notation = lstring * constr_expr * scope_name option -type simple_binder = lident list * constr_expr -type class_binder = lident * constr_expr list -type 'a with_coercion = coercion_flag * 'a -type 'a with_instance = instance_flag * 'a -type 'a with_notation = 'a * decl_notation list -type 'a with_priority = 'a * int option -type constructor_expr = (lident * constr_expr) with_coercion -type constructor_list_or_record_decl_expr = - | Constructors of constructor_expr list - | RecordDecl of lident option * local_decl_expr with_instance with_priority with_notation list -type inductive_expr = - ident_decl with_coercion * local_binder_expr list * constr_expr option * inductive_kind * - constructor_list_or_record_decl_expr - -type one_inductive_expr = - ident_decl * local_binder_expr list * constr_expr option * constructor_expr list - -type typeclass_constraint = name_decl * Decl_kinds.binding_kind * constr_expr -and typeclass_context = typeclass_constraint list - -type proof_expr = - ident_decl * (local_binder_expr list * constr_expr) - -type syntax_modifier = - | SetItemLevel of string list * Extend.production_level - | SetItemLevelAsBinder of string list * Extend.constr_as_binder_kind * Extend.production_level option - | SetLevel of int - | SetAssoc of Extend.gram_assoc - | SetEntryType of string * Extend.simple_constr_prod_entry_key - | SetOnlyParsing - | SetOnlyPrinting - | SetCompatVersion of Flags.compat_version - | SetFormat of string * lstring - -type proof_end = - | Admitted - (* name in `Save ident` when closing goal *) - | Proved of opacity_flag * lident option - -type scheme = - | InductionScheme of bool * reference or_by_notation * sort_expr - | CaseScheme of bool * reference or_by_notation * sort_expr - | EqualityScheme of reference or_by_notation - -type section_subset_expr = - | SsEmpty - | SsType - | SsSingl of lident - | SsCompl of section_subset_expr - | SsUnion of section_subset_expr * section_subset_expr - | SsSubstr of section_subset_expr * section_subset_expr - | SsFwdClose of section_subset_expr - -(** Extension identifiers for the VERNAC EXTEND mechanism. - - {b ("Extraction", 0} indicates {b Extraction {i qualid}} command. - - {b ("Extraction", 1} indicates {b Recursive Extraction {i qualid}} command. - - {b ("Extraction", 2)} indicates {b Extraction "{i filename}" {i qualid{_ 1}} ... {i qualid{_ n}}} command. - - {b ("ExtractionLibrary", 0)} indicates {b Extraction Library {i ident}} command. - - {b ("RecursiveExtractionLibrary", 0)} indicates {b Recursive Extraction Library {i ident}} command. - - {b ("SeparateExtraction", 0)} indicates {b Separate Extraction {i qualid{_ 1}} ... {i qualid{_ n}}} command. - - {b ("ExtractionLanguage", 0)} indicates {b Extraction Language Ocaml} or {b Extraction Language Haskell} or {b Extraction Language Scheme} or {b Extraction Language JSON} commands. - - {b ("ExtractionImplicit", 0)} indicates {b Extraction Implicit {i qualid} \[ {i ident{_1}} ... {i ident{_n} } \] } command. - - {b ("ExtractionConstant", 0)} indicates {b Extract Constant {i qualid} => {i string}} command. - - {b ("ExtractionInlinedConstant", 0)} indicates {b Extract Inlined Constant {i qualid} => {i string}} command. - - {b ("ExtractionInductive", 0)} indicates {b Extract Inductive {i qualid} => {i string} [ {i string} ... {string} ] {i optstring}} command. - - {b ("ExtractionBlacklist", 0)} indicates {b Extraction Blacklist {i ident{_1}} ... {i ident{_n}}} command. - *) -type extend_name = - (** Name of the vernac entry where the tactic is defined, typically found - after the VERNAC EXTEND statement in the source. *) - string * - (** Index of the extension in the VERNAC EXTEND statement. Each parsing branch - is given an offset, starting from zero. *) - int - -(* This type allows registering the inlining of constants in native compiler. - It will be extended with primitive inductive types and operators *) -type register_kind = - | RegisterInline - -type bullet = Proof_bullet.t -[@@ocaml.deprecated "Alias type, please use [Proof_bullet.t]"] - -(** {6 Types concerning the module layer} *) - -(** Rigid / flexible module signature *) - -type 'a module_signature = 'a Declaremods.module_signature = - | Enforce of 'a (** ... : T *) - | Check of 'a list (** ... <: T1 <: T2, possibly empty *) -[@@ocaml.deprecated "please use [Declaremods.module_signature]."] - -(** Which module inline annotations should we honor, - either None or the ones whose level is less or equal - to the given integer *) - -type inline = Declaremods.inline = - | NoInline - | DefaultInline - | InlineAt of int -[@@ocaml.deprecated "please use [Declaremods.inline]."] - -type module_ast_inl = module_ast * Declaremods.inline -type module_binder = bool option * lident list * module_ast_inl - -(** [Some b] if locally enabled/disabled according to [b], [None] if - we should use the global flag. *) -type vernac_cumulative = VernacCumulative | VernacNonCumulative - -(** {6 The type of vernacular expressions} *) - -type vernac_implicit_status = Implicit | MaximallyImplicit | NotImplicit - -type vernac_argument_status = { - name : Name.t; - recarg_like : bool; - notation_scope : string CAst.t option; - implicit_status : vernac_implicit_status; -} - -type nonrec vernac_expr = - - | VernacLoad of verbose_flag * string - (* Syntax *) - | VernacSyntaxExtension of bool * (lstring * syntax_modifier list) - | VernacOpenCloseScope of bool * scope_name - | VernacDelimiters of scope_name * string option - | VernacBindScope of scope_name * class_rawexpr list - | VernacInfix of (lstring * syntax_modifier list) * - constr_expr * scope_name option - | VernacNotation of - constr_expr * (lstring * syntax_modifier list) * - scope_name option - | VernacNotationAddFormat of string * string * string - - (* Gallina *) - | VernacDefinition of (Decl_kinds.discharge * Decl_kinds.definition_object_kind) * name_decl * definition_expr - | VernacStartTheoremProof of Decl_kinds.theorem_kind * proof_expr list - | VernacEndProof of proof_end - | VernacExactProof of constr_expr - | VernacAssumption of (Decl_kinds.discharge * Decl_kinds.assumption_object_kind) * - Declaremods.inline * (ident_decl list * constr_expr) with_coercion list - | VernacInductive of vernac_cumulative option * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list - | VernacFixpoint of Decl_kinds.discharge * (fixpoint_expr * decl_notation list) list - | VernacCoFixpoint of Decl_kinds.discharge * (cofixpoint_expr * decl_notation list) list - | VernacScheme of (lident option * scheme) list - | VernacCombinedScheme of lident * lident list - | VernacUniverse of lident list - | VernacConstraint of Glob_term.glob_constraint list - - (* Gallina extensions *) - | VernacBeginSection of lident - | VernacEndSegment of lident - | VernacRequire of - reference option * export_flag option * reference list - | VernacImport of export_flag * reference list - | VernacCanonical of reference or_by_notation - | VernacCoercion of reference or_by_notation * - class_rawexpr * class_rawexpr - | VernacIdentityCoercion of lident * class_rawexpr * class_rawexpr - | VernacNameSectionHypSet of lident * section_subset_expr - - (* Type classes *) - | VernacInstance of - bool * (* abstract instance *) - local_binder_expr list * (* super *) - typeclass_constraint * (* instance name, class name, params *) - (bool * constr_expr) option * (* props *) - Typeclasses.hint_info_expr - - | VernacContext of local_binder_expr list - - | VernacDeclareInstances of - (reference * Typeclasses.hint_info_expr) list (* instances names, priorities and patterns *) - - | VernacDeclareClass of reference (* inductive or definition name *) - - (* Modules and Module Types *) - | VernacDeclareModule of bool option * lident * - module_binder list * module_ast_inl - | VernacDefineModule of bool option * lident * module_binder list * - module_ast_inl Declaremods.module_signature * module_ast_inl list - | VernacDeclareModuleType of lident * - module_binder list * module_ast_inl list * module_ast_inl list - | VernacInclude of module_ast_inl list - - (* Solving *) - - | VernacSolveExistential of int * constr_expr - - (* Auxiliary file and library management *) - | VernacAddLoadPath of rec_flag * string * DirPath.t option - | VernacRemoveLoadPath of string - | VernacAddMLPath of rec_flag * string - | VernacDeclareMLModule of string list - | VernacChdir of string option - - (* State management *) - | VernacWriteState of string - | VernacRestoreState of string - - (* Resetting *) - | VernacResetName of lident - | VernacResetInitial - | VernacBack of int - | VernacBackTo of int - - (* Commands *) - | VernacCreateHintDb of string * bool - | VernacRemoveHints of string list * reference list - | VernacHints of string list * hints_expr - | VernacSyntacticDefinition of lident * (Id.t list * constr_expr) * - onlyparsing_flag - | VernacArguments of reference or_by_notation * - vernac_argument_status list (* Main arguments status list *) * - (Name.t * vernac_implicit_status) list list (* Extra implicit status lists *) * - int option (* Number of args to trigger reduction *) * - [ `ReductionDontExposeCase | `ReductionNeverUnfold | `Rename | - `ExtraScopes | `Assert | `ClearImplicits | `ClearScopes | - `DefaultImplicits ] list - | VernacReserve of simple_binder list - | VernacGeneralizable of (lident list) option - | VernacSetOpacity of (Conv_oracle.level * reference or_by_notation list) - | VernacSetStrategy of - (Conv_oracle.level * reference or_by_notation list) list - | VernacUnsetOption of export_flag * Goptions.option_name - | VernacSetOption of export_flag * Goptions.option_name * option_value - | VernacAddOption of Goptions.option_name * option_ref_value list - | VernacRemoveOption of Goptions.option_name * option_ref_value list - | VernacMemOption of Goptions.option_name * option_ref_value list - | VernacPrintOption of Goptions.option_name - | VernacCheckMayEval of Genredexpr.raw_red_expr option * Goal_select.t option * constr_expr - | VernacGlobalCheck of constr_expr - | VernacDeclareReduction of string * Genredexpr.raw_red_expr - | VernacPrint of printable - | VernacSearch of searchable * Goal_select.t option * search_restriction - | VernacLocate of locatable - | VernacRegister of lident * register_kind - | VernacComments of comment list - - (* Proof management *) - | VernacAbort of lident option - | VernacAbortAll - | VernacRestart - | VernacUndo of int - | VernacUndoTo of int - | VernacFocus of int option - | VernacUnfocus - | VernacUnfocused - | VernacBullet of Proof_bullet.t - | VernacSubproof of Goal_select.t option - | VernacEndSubproof - | VernacShow of showable - | VernacCheckGuard - | VernacProof of Genarg.raw_generic_argument option * section_subset_expr option - | VernacProofMode of string - - (* For extension *) - | VernacExtend of extend_name * Genarg.raw_generic_argument list - -type nonrec vernac_flag = - | VernacProgram - | VernacPolymorphic of bool - | VernacLocal of bool - -type vernac_control = - | VernacExpr of vernac_flag list * vernac_expr - (* boolean is true when the `-time` batch-mode command line flag was set. - the flag is used to print differently in `-time` vs `Time foo` *) - | VernacTime of bool * vernac_control CAst.t - | VernacRedirect of string * vernac_control CAst.t - | VernacTimeout of int * vernac_control - | VernacFail of vernac_control - -(* A vernac classifier provides information about the exectuion of a - command: - - - vernac_when: encodes if the vernac may alter the parser [thus - forcing immediate execution], or if indeed it is pure and parsing - can continue without its execution. - - - vernac_type: if it is starts, ends, continues a proof or - alters the global state or is a control command like BackTo or is - a query like Check. - - The classification works on the assumption that we have 3 states: - parsing, execution (global enviroment, etc...), and proof - state. For example, commands that only alter the proof state are - considered safe to delegate to a worker. - -*) -type vernac_type = - (* Start of a proof *) - | VtStartProof of vernac_start - (* Command altering the global state, bad for parallel - processing. *) - | VtSideff of vernac_sideff_type - (* End of a proof *) - | VtQed of vernac_qed_type - (* A proof step *) - | VtProofStep of proof_step - (* To be removed *) - | VtProofMode of string - (* Queries are commands assumed to be "pure", that is to say, they - don't modify the interpretation state. *) - | VtQuery - (* To be removed *) - | VtMeta - | VtUnknown -and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *) -and vernac_start = string * opacity_guarantee * Id.t list -and vernac_sideff_type = Id.t list -and opacity_guarantee = - | GuaranteesOpacity (** Only generates opaque terms at [Qed] *) - | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*) -and proof_step = { (* TODO: inline with OCaml 4.03 *) - parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ]; - proof_block_detection : proof_block_name option -} -and solving_tac = bool (* a terminator *) -and anon_abstracting_tac = bool (* abstracting anonymously its result *) -and proof_block_name = string (* open type of delimiters *) -type vernac_when = - | VtNow - | VtLater -type vernac_classification = vernac_type * vernac_when - - -(** Deprecated stuff *) -type universe_decl_expr = Constrexpr.universe_decl_expr -[@@ocaml.deprecated "alias of Constrexpr.universe_decl_expr"] - -type ident_decl = Constrexpr.ident_decl -[@@ocaml.deprecated "alias of Constrexpr.ident_decl"] - -type name_decl = Constrexpr.name_decl -[@@ocaml.deprecated "alias of Constrexpr.name_decl"] |