From 368a25e4ef14512b00f5799e26c3f615bc540201 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 22 May 2018 00:07:26 +0200 Subject: [api] Misctypes removal: several moves: - move_location to proofs/logic. - intro_pattern_naming to Namegen. --- dev/base_include | 2 - engine/evarutil.ml | 8 +-- engine/evarutil.mli | 15 +++--- engine/namegen.ml | 12 +++++ engine/namegen.mli | 10 ++++ interp/constrexpr.ml | 5 +- interp/constrexpr_ops.ml | 11 +++-- interp/constrexpr_ops.mli | 3 +- interp/constrextern.ml | 13 ++--- interp/constrintern.ml | 34 ++++++------- interp/notation_ops.ml | 22 ++++----- interp/notation_term.ml | 3 +- interp/tactypes.ml | 32 +++++++++++- library/misctypes.ml | 86 --------------------------------- parsing/g_constr.ml4 | 2 +- plugins/cc/cctac.ml | 2 +- plugins/firstorder/instances.ml | 5 +- plugins/funind/g_indfun.ml4 | 2 +- plugins/funind/glob_term_to_relation.ml | 1 - plugins/funind/glob_termops.ml | 11 ++--- plugins/funind/indfun.ml | 4 +- plugins/funind/indfun.mli | 2 +- plugins/funind/invfun.ml | 6 +-- plugins/funind/invfun.mli | 2 +- plugins/funind/recdef.ml | 2 +- plugins/ltac/coretactics.ml4 | 2 + plugins/ltac/evar_tactics.ml | 2 +- plugins/ltac/extratactics.ml4 | 9 ++-- plugins/ltac/g_ltac.ml4 | 2 + plugins/ltac/g_rewrite.ml4 | 2 +- plugins/ltac/g_tactic.ml4 | 2 + plugins/ltac/pltac.mli | 1 + plugins/ltac/pptactic.ml | 3 +- plugins/ltac/pptactic.mli | 1 + plugins/ltac/rewrite.ml | 4 +- plugins/ltac/rewrite.mli | 4 +- plugins/ltac/tacarg.mli | 2 +- plugins/ltac/taccoerce.ml | 2 + plugins/ltac/taccoerce.mli | 3 +- plugins/ltac/tacexpr.ml | 7 +-- plugins/ltac/tacexpr.mli | 7 +-- plugins/ltac/tacintern.ml | 2 + plugins/ltac/tacintern.mli | 2 +- plugins/ltac/tacinterp.ml | 2 + plugins/ltac/tacinterp.mli | 1 + plugins/ltac/tacsubst.ml | 1 + plugins/ltac/tacsubst.mli | 2 +- plugins/ltac/tauto.ml | 4 +- plugins/micromega/coq_micromega.ml | 5 +- plugins/omega/coq_omega.ml | 2 +- plugins/ssr/ssrcommon.ml | 8 +-- plugins/ssr/ssrelim.ml | 2 +- plugins/ssr/ssrfwd.ml | 1 - plugins/ssr/ssrparser.ml4 | 18 +++---- plugins/ssr/ssrview.ml | 2 +- plugins/ssrmatching/ssrmatching.ml4 | 2 +- pretyping/cases.ml | 2 +- pretyping/detyping.ml | 3 +- pretyping/glob_ops.ml | 35 +++++++++++--- pretyping/glob_ops.mli | 9 +++- pretyping/glob_term.ml | 11 ++++- pretyping/miscops.ml | 55 --------------------- pretyping/miscops.mli | 30 ------------ pretyping/misctypes.ml | 37 ++++++++++++++ pretyping/patternops.ml | 5 +- pretyping/pretyping.ml | 1 - printing/ppconstr.ml | 17 ++++--- proofs/clenv.ml | 2 +- proofs/clenv.mli | 2 +- proofs/logic.ml | 19 +++++++- proofs/logic.mli | 15 +++++- proofs/miscprint.ml | 12 +---- proofs/miscprint.mli | 7 +-- tactics/contradiction.ml | 3 +- tactics/contradiction.mli | 2 +- tactics/eqdecide.ml | 10 ++-- tactics/equality.ml | 1 + tactics/hipattern.ml | 2 +- tactics/inv.ml | 14 +++--- tactics/inv.mli | 1 - tactics/leminv.mli | 2 +- tactics/tacticals.ml | 4 +- tactics/tactics.ml | 1 + tactics/tactics.mli | 12 ++--- vernac/auto_ind_decl.ml | 3 +- vernac/classes.ml | 4 +- vernac/g_proofs.ml4 | 2 +- vernac/g_vernac.ml4 | 8 +-- vernac/ppvernac.ml | 2 +- vernac/record.ml | 2 +- 90 files changed, 359 insertions(+), 378 deletions(-) delete mode 100644 library/misctypes.ml delete mode 100644 pretyping/miscops.ml delete mode 100644 pretyping/miscops.mli create mode 100644 pretyping/misctypes.ml diff --git a/dev/base_include b/dev/base_include index fc38305cc..574bc097e 100644 --- a/dev/base_include +++ b/dev/base_include @@ -108,8 +108,6 @@ open Inductiveops open Locusops open Find_subterm open Unification -open Miscops -open Miscops open Nativenorm open Typeclasses open Typeclasses_errors diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 648f96035..82be4791f 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -436,12 +436,12 @@ let new_pure_evar_full evd evi = (evd, evk) let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) sign evd typ = - let default_naming = Misctypes.IntroAnonymous in + let default_naming = IntroAnonymous in let naming = Option.default default_naming naming in let name = match naming with - | Misctypes.IntroAnonymous -> None - | Misctypes.IntroIdentifier id -> Some id - | Misctypes.IntroFresh id -> + | IntroAnonymous -> None + | IntroIdentifier id -> Some id + | IntroFresh id -> let has_name id = try let _ = Evd.evar_key id evd in true with Not_found -> false in let id = Namegen.next_ident_away_from id has_name in Some id diff --git a/engine/evarutil.mli b/engine/evarutil.mli index f83f262b4..c17f3d168 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -12,6 +12,7 @@ open Names open Constr open Evd open Environ +open Namegen open EConstr (** This module provides useful higher-level functions for evar manipulation. *) @@ -27,7 +28,7 @@ val mk_new_meta : unit -> constr val new_evar_from_context : ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> + ?naming:intro_pattern_naming_expr -> ?principal:bool -> named_context_val -> evar_map -> types -> evar_map * EConstr.t @@ -40,14 +41,14 @@ type naming_mode = val new_evar : ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> + ?naming:intro_pattern_naming_expr -> ?principal:bool -> ?hypnaming:naming_mode -> env -> evar_map -> types -> evar_map * EConstr.t val new_pure_evar : ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> + ?naming:intro_pattern_naming_expr -> ?principal:bool -> named_context_val -> evar_map -> types -> evar_map * Evar.t @@ -57,7 +58,7 @@ val new_pure_evar_full : evar_map -> evar_info -> evar_map * Evar.t them during type-checking and unification. *) val new_type_evar : ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> + ?naming:intro_pattern_naming_expr -> ?principal:bool -> ?hypnaming:naming_mode -> env -> evar_map -> rigid -> evar_map * (constr * Sorts.t) @@ -79,7 +80,7 @@ val new_global : evar_map -> GlobRef.t -> evar_map * constr as a telescope) is [sign] *) val new_evar_instance : ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> - ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> + ?store:Store.t -> ?naming:intro_pattern_naming_expr -> ?principal:bool -> named_context_val -> evar_map -> types -> constr list -> evar_map * constr @@ -262,13 +263,13 @@ val meta_counter_summary_tag : int Summary.Dyn.tag val e_new_evar : env -> evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> + ?naming:intro_pattern_naming_expr -> ?principal:bool -> ?hypnaming:naming_mode -> types -> constr [@@ocaml.deprecated "Use [Evarutil.new_evar]"] val e_new_type_evar : env -> evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> + ?naming:intro_pattern_naming_expr -> ?principal:bool -> ?hypnaming:naming_mode -> rigid -> constr * Sorts.t [@@ocaml.deprecated "Use [Evarutil.new_type_evar]"] diff --git a/engine/namegen.ml b/engine/namegen.ml index c069ec5a0..23c691139 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -29,6 +29,18 @@ open Context.Rel.Declaration module RelDecl = Context.Rel.Declaration +(** General evar naming using intro patterns *) +type intro_pattern_naming_expr = + | IntroIdentifier of Id.t + | IntroFresh of Id.t + | IntroAnonymous + +let intro_pattern_naming_eq nam1 nam2 = match nam1, nam2 with +| IntroAnonymous, IntroAnonymous -> true +| IntroIdentifier id1, IntroIdentifier id2 -> Names.Id.equal id1 id2 +| IntroFresh id1, IntroFresh id2 -> Names.Id.equal id1 id2 +| _ -> false + (**********************************************************************) (* Conventional names *) diff --git a/engine/namegen.mli b/engine/namegen.mli index 1b70ef68d..a53c3a0d1 100644 --- a/engine/namegen.mli +++ b/engine/namegen.mli @@ -15,6 +15,16 @@ open Environ open Evd open EConstr +(** General evar naming using intro patterns *) +type intro_pattern_naming_expr = + | IntroIdentifier of Id.t + | IntroFresh of Id.t + | IntroAnonymous + +(** Equalities on [intro_pattern_naming] *) +val intro_pattern_naming_eq : + intro_pattern_naming_expr -> intro_pattern_naming_expr -> bool + (********************************************************************* Conventional default names *) diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml index d6b395e01..60f2c683a 100644 --- a/interp/constrexpr.ml +++ b/interp/constrexpr.ml @@ -10,7 +10,6 @@ open Names open Libnames -open Misctypes open Decl_kinds (** {6 Concrete syntax for terms } *) @@ -94,11 +93,11 @@ and constr_expr_r = constr_expr * constr_expr | CIf of constr_expr * (lname option * constr_expr option) * constr_expr * constr_expr - | CHole of Evar_kinds.t option * intro_pattern_naming_expr * Genarg.raw_generic_argument option + | CHole of Evar_kinds.t option * Namegen.intro_pattern_naming_expr * Genarg.raw_generic_argument option | CPatVar of Pattern.patvar | CEvar of Glob_term.existential_name * (Id.t * constr_expr) list | CSort of Glob_term.glob_sort - | CCast of constr_expr * constr_expr cast_type + | CCast of constr_expr * constr_expr Glob_term.cast_type | CNotation of notation * constr_notation_substitution | CGeneralization of binding_kind * abstraction_kind option * constr_expr | CPrim of prim_token diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 1be1dd96c..d626630ef 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -14,8 +14,9 @@ open CAst open Names open Nameops open Libnames +open Namegen +open Glob_term open Constrexpr -open Misctypes open Decl_kinds (***********************) @@ -161,7 +162,7 @@ let rec constr_expr_eq e1 e2 = | CEvar (id1, c1), CEvar (id2, c2) -> Id.equal id1 id2 && List.equal instance_eq c1 c2 | CSort s1, CSort s2 -> - Miscops.glob_sort_eq s1 s2 + Glob_ops.glob_sort_eq s1 s2 | CCast(t1,c1), CCast(t2,c2) -> constr_expr_eq t1 t2 && cast_expr_eq c1 c2 | CNotation(n1, s1), CNotation(n2, s2) -> @@ -395,7 +396,7 @@ let map_constr_expr_with_binders g f e = CAst.map (function let (e,bl) = map_local_binders f g e bl in CLambdaN (bl,f e b) | CLetIn (na,a,t,b) -> CLetIn (na,f e a,Option.map (f e) t,f (Name.fold_right g (na.CAst.v) e) b) - | CCast (a,c) -> CCast (f e a, Miscops.map_cast_type (f e) c) + | CCast (a,c) -> CCast (f e a, Glob_ops.map_cast_type (f e) c) | CNotation (n,(l,ll,bl,bll)) -> (* This is an approximation because we don't know what binds what *) CNotation (n,(List.map (f e) l,List.map (List.map (f e)) ll, bl, @@ -545,7 +546,7 @@ let coerce_to_id = function let coerce_to_name = function | { CAst.loc; v = CRef ({v=Ident id},None) } -> CAst.make ?loc @@ Name id - | { CAst.loc; v = CHole (None,Misctypes.IntroAnonymous,None) } -> CAst.make ?loc Anonymous + | { CAst.loc; v = CHole (None,IntroAnonymous,None) } -> CAst.make ?loc Anonymous | { CAst.loc; _ } -> CErrors.user_err ?loc ~hdr:"coerce_to_name" (str "This expression should be a name.") @@ -569,7 +570,7 @@ let mkAppPattern ?loc p lp = let rec coerce_to_cases_pattern_expr c = CAst.map_with_loc (fun ?loc -> function | CRef (r,None) -> CPatAtom (Some r) - | CHole (None,Misctypes.IntroAnonymous,None) -> + | CHole (None,IntroAnonymous,None) -> CPatAtom None | CLetIn ({CAst.loc;v=Name id},b,None,{ CAst.v = CRef ({v=Ident id'},None) }) when Id.equal id id' -> CPatAlias (coerce_to_cases_pattern_expr b, CAst.(make ?loc @@ Name id)) diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index b4f0886ac..1c2348457 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -10,7 +10,6 @@ open Names open Libnames -open Misctypes open Constrexpr (** Constrexpr_ops: utilities on [constr_expr] *) @@ -44,7 +43,7 @@ val local_binders_loc : local_binder_expr list -> Loc.t option val mkIdentC : Id.t -> constr_expr val mkRefC : reference -> constr_expr val mkAppC : constr_expr * constr_expr list -> constr_expr -val mkCastC : constr_expr * constr_expr cast_type -> constr_expr +val mkCastC : constr_expr * constr_expr Glob_term.cast_type -> constr_expr val mkLambdaC : lname list * binder_kind * constr_expr * constr_expr -> constr_expr val mkLetInC : lname * constr_expr * constr_expr option * constr_expr -> constr_expr val mkProdC : lname list * binder_kind * constr_expr * constr_expr -> constr_expr diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 86f6ce9ae..c613effcd 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -17,6 +17,7 @@ open Nameops open Termops open Libnames open Globnames +open Namegen open Impargs open CAst open Constrexpr @@ -719,7 +720,7 @@ let extended_glob_local_binder_of_decl loc = function | (p,bk,None,t) -> GLocalAssum (p,bk,t) | (p,bk,Some x, t) -> match DAst.get t with - | GHole (_, Misctypes.IntroAnonymous, None) -> GLocalDef (p,bk,x,None) + | GHole (_, IntroAnonymous, None) -> GLocalDef (p,bk,x,None) | _ -> GLocalDef (p,bk,x,Some t) let extended_glob_local_binder_of_decl ?loc u = DAst.make ?loc (extended_glob_local_binder_of_decl loc u) @@ -754,13 +755,13 @@ let rec extern inctx scopes vars r = | GVar id -> CRef (make ?loc @@ Ident id,None) - | GEvar (n,[]) when !print_meta_as_hole -> CHole (None, Misctypes.IntroAnonymous, None) + | GEvar (n,[]) when !print_meta_as_hole -> CHole (None, IntroAnonymous, None) | GEvar (n,l) -> extern_evar n (List.map (on_snd (extern false scopes vars)) l) | GPatVar kind -> - if !print_meta_as_hole then CHole (None, Misctypes.IntroAnonymous, None) else + if !print_meta_as_hole then CHole (None, IntroAnonymous, None) else (match kind with | Evar_kinds.SecondOrderPatVar n -> CPatVar n | Evar_kinds.FirstOrderPatVar n -> CEvar (n,[])) @@ -916,7 +917,7 @@ let rec extern inctx scopes vars r = | GCast (c, c') -> CCast (sub_extern true scopes vars c, - Miscops.map_cast_type (extern_typ scopes vars) c') + map_cast_type (extern_typ scopes vars) c') | GProj (p, c) -> let pr = extern_reference ?loc Id.Set.empty (ConstRef (Projection.constant p)) in CProj (pr, sub_extern inctx scopes vars c) @@ -1159,7 +1160,7 @@ let extern_closed_glob ?lax goal_concl_style env sigma t = let any_any_branch = (* | _ => _ *) - CAst.make ([],[DAst.make @@ PatVar Anonymous], DAst.make @@ GHole (Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None)) + CAst.make ([],[DAst.make @@ PatVar Anonymous], DAst.make @@ GHole (Evar_kinds.InternalHole,IntroAnonymous,None)) let compute_displayed_name_in_pattern sigma avoid na c = let open Namegen in @@ -1183,7 +1184,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with anomaly ~label:"glob_constr_of_pattern" (Pp.str "index to an anonymous variable.") with Not_found -> Id.of_string ("_UNBOUND_REL_"^(string_of_int n)) in GVar id - | PMeta None -> GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous,None) + | PMeta None -> GHole (Evar_kinds.InternalHole, IntroAnonymous,None) | PMeta (Some n) -> GPatVar (Evar_kinds.FirstOrderPatVar n) | PProj (p,c) -> GApp (DAst.make @@ GRef (ConstRef (Projection.constant p),None), [glob_of_pat avoid env sigma c]) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 057e10c00..d7345b701 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -14,8 +14,8 @@ open Util open CAst open Names open Nameops -open Constr open Namegen +open Constr open Libnames open Globnames open Impargs @@ -394,7 +394,7 @@ let intern_generalized_binder ?(global_level=false) intern_type ntnvars env fvs in let bl = List.map CAst.(map (fun id -> - (Name id, b, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None)))) + (Name id, b, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None)))) fvs in let na = match na with @@ -431,7 +431,7 @@ let glob_local_binder_of_extended = DAst.with_loc_val (fun ?loc -> function | GLocalAssum (na,bk,t) -> (na,bk,None,t) | GLocalDef (na,bk,c,Some t) -> (na,bk,Some c,t) | GLocalDef (na,bk,c,None) -> - let t = DAst.make ?loc @@ GHole(Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None) in + let t = DAst.make ?loc @@ GHole(Evar_kinds.BinderType na,IntroAnonymous,None) in (na,bk,Some c,t) | GLocalPattern (_,_,_,_) -> Loc.raise ?loc (Stream.Error "pattern with quote not allowed here") @@ -472,7 +472,7 @@ let intern_local_binder_aux ?(global_level=false) intern ntnvars (env,bl) = func let tyc = match ty with | Some ty -> ty - | None -> CAst.make ?loc @@ CHole(None,Misctypes.IntroAnonymous,None) + | None -> CAst.make ?loc @@ CHole(None,IntroAnonymous,None) in let env, ((disjpat,il),id),na = intern_cases_pattern_as_binder ?loc ntnvars env p in let bk = Default Explicit in @@ -502,11 +502,11 @@ let intern_generalization intern env ntnvars loc bk ak c = if pi then (fun {loc=loc';v=id} acc -> DAst.make ?loc:(Loc.merge_opt loc' loc) @@ - GProd (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc)) + GProd (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None), acc)) else (fun {loc=loc';v=id} acc -> DAst.make ?loc:(Loc.merge_opt loc' loc) @@ - GLambda (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc)) + GLambda (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None), acc)) in List.fold_right (fun ({loc;v=id} as lid) (env, acc) -> let env' = push_name_env ntnvars (Variable,[],[],[]) env CAst.(make @@ Name id) in @@ -564,7 +564,7 @@ let term_of_name = function | Name id -> DAst.make (GVar id) | Anonymous -> let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in - DAst.make (GHole (Evar_kinds.QuestionMark (st,Anonymous), Misctypes.IntroAnonymous, None)) + DAst.make (GHole (Evar_kinds.QuestionMark (st,Anonymous), IntroAnonymous, None)) let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renaming,env) = function | Anonymous -> (renaming,env), None, Anonymous @@ -626,7 +626,7 @@ let terms_of_binders bl = | PatVar (Anonymous) -> error_cannot_coerce_wildcard_term ?loc () | PatCstr (c,l,_) -> let r = make ?loc @@ Qualid (qualid_of_path (path_of_global (ConstructRef c))) in - let hole = CAst.make ?loc @@ CHole (None,Misctypes.IntroAnonymous,None) in + let hole = CAst.make ?loc @@ CHole (None,IntroAnonymous,None) in let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in CAppExpl ((None,r,None),params @ List.map term_of_pat l)) pt in let rec extract_variables l = match l with @@ -1725,15 +1725,15 @@ let get_implicit_name n imps = let set_hole_implicit i b c = let loc = c.CAst.loc in match DAst.get c with - | GRef (r, _) -> Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),Misctypes.IntroAnonymous,None) + | GRef (r, _) -> Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),IntroAnonymous,None) | GApp (r, _) -> let loc = r.CAst.loc in begin match DAst.get r with | GRef (r, _) -> - Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),Misctypes.IntroAnonymous,None) + Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),IntroAnonymous,None) | _ -> anomaly (Pp.str "Only refs have implicits.") end - | GVar id -> Loc.tag ?loc (Evar_kinds.ImplicitArg (VarRef id,i,b),Misctypes.IntroAnonymous,None) + | GVar id -> Loc.tag ?loc (Evar_kinds.ImplicitArg (VarRef id,i,b),IntroAnonymous,None) | _ -> anomaly (Pp.str "Only refs have implicits.") let exists_implicit_name id = @@ -1919,13 +1919,13 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let fields = sort_fields ~complete:true loc fs (fun _idx -> CAst.make ?loc @@ CHole (Some (Evar_kinds.QuestionMark (st,Anonymous)), - Misctypes.IntroAnonymous, None)) + IntroAnonymous, None)) in begin match fields with | None -> user_err ?loc ~hdr:"intern" (str"No constructor inference.") | Some (n, constrname, args) -> - let pars = List.make n (CAst.make ?loc @@ CHole (None, Misctypes.IntroAnonymous, None)) in + let pars = List.make n (CAst.make ?loc @@ CHole (None, IntroAnonymous, None)) in let app = CAst.make ?loc @@ CAppExpl ((None, constrname,None), List.rev_append pars args) in intern env app end @@ -1965,12 +1965,12 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let main_sub_eqn = CAst.make @@ ([],thepats, (* "|p1,..,pn" *) Option.cata (intern_type env') - (DAst.make ?loc @@ GHole(Evar_kinds.CasesType false,Misctypes.IntroAnonymous,None)) + (DAst.make ?loc @@ GHole(Evar_kinds.CasesType false,IntroAnonymous,None)) rtnpo) (* "=> P" if there were a return predicate P, and "=> _" otherwise *) in let catch_all_sub_eqn = if List.for_all (irrefutable globalenv) thepats then [] else [CAst.make @@ ([],List.make (List.length thepats) (DAst.make @@ PatVar Anonymous), (* "|_,..,_" *) - DAst.make @@ GHole(Evar_kinds.ImpossibleCase,Misctypes.IntroAnonymous,None))] (* "=> _" *) in + DAst.make @@ GHole(Evar_kinds.ImpossibleCase,IntroAnonymous,None))] (* "=> _" *) in Some (DAst.make @@ GCases(RegularStyle,sub_rtn,sub_tms,main_sub_eqn::catch_all_sub_eqn)) in let eqns' = List.map (intern_eqn (List.length tms) env) eqns in @@ -2001,7 +2001,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = | None -> let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in (match naming with - | Misctypes.IntroIdentifier id -> Evar_kinds.NamedHole id + | IntroIdentifier id -> Evar_kinds.NamedHole id | _ -> Evar_kinds.QuestionMark (st,Anonymous)) | Some k -> k in @@ -2046,7 +2046,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = GSort s | CCast (c1, c2) -> DAst.make ?loc @@ - GCast (intern env c1, Miscops.map_cast_type (intern_type env) c2) + GCast (intern env c1, map_cast_type (intern_type env) c2) | CProj (pr, c) -> match intern_reference pr with | ConstRef p -> diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index f208b23fb..ab0bf9c6f 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -16,7 +16,7 @@ open Nameops open Constr open Globnames open Decl_kinds -open Misctypes +open Namegen open Glob_term open Glob_ops open Mod_subst @@ -86,7 +86,7 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with Array.equal (eq_notation_constr vars) us1 us2 && Array.equal (eq_notation_constr vars) rs1 rs2 | NSort s1, NSort s2 -> - Miscops.glob_sort_eq s1 s2 + glob_sort_eq s1 s2 | NCast (t1, c1), NCast (t2, c2) -> (eq_notation_constr vars) t1 t2 && cast_type_eq (eq_notation_constr vars) c1 c2 | NProj (p1, c1), NProj (p2, c2) -> @@ -158,7 +158,7 @@ let protect g e na = let apply_cases_pattern ?loc ((ids,disjpat),id) c = let tm = DAst.make ?loc (GVar id) in let eqns = List.map (fun pat -> (CAst.make ?loc (ids,[pat],c))) disjpat in - DAst.make ?loc @@ GCases (LetPatternStyle, None, [tm,(Anonymous,None)], eqns) + DAst.make ?loc @@ GCases (Constr.LetPatternStyle, None, [tm,(Anonymous,None)], eqns) let glob_constr_of_notation_constr_with_binders ?loc g f e nc = let lt x = DAst.make ?loc x in lt @@ match nc with @@ -216,7 +216,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc = (e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in let e',idl = Array.fold_left_map (to_id (protect g)) e idl in GRec (fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl) - | NCast (c,k) -> GCast (f e c,Miscops.map_cast_type (f e) k) + | NCast (c,k) -> GCast (f e c,map_cast_type (f e) k) | NSort x -> GSort x | NHole (x, naming, arg) -> GHole (x, naming, arg) | NRef x -> GRef (x,None) @@ -434,7 +434,7 @@ let notation_constr_and_vars_of_glob_constr recvars a = user_err Pp.(str "Binders marked as implicit not allowed in notations."); add_name found na; (na,Option.map aux oc,aux b))) dll in NRec (fk,idl,dll,Array.map aux tl,Array.map aux bl) - | GCast (c,k) -> NCast (aux c,Miscops.map_cast_type aux k) + | GCast (c,k) -> NCast (aux c,map_cast_type aux k) | GSort s -> NSort s | GHole (w,naming,arg) -> if arg != None then has_ltac := true; @@ -637,7 +637,7 @@ let rec subst_notation_constr subst bound raw = | NCast (r1,k) -> let r1' = subst_notation_constr subst bound r1 in - let k' = Miscops.smartmap_cast_type (subst_notation_constr subst bound) k in + let k' = smartmap_cast_type (subst_notation_constr subst bound) k in if r1' == r1 && k' == k then raw else NCast(r1',k') | NProj (p, c) -> @@ -666,11 +666,11 @@ let abstract_return_type_context pi mklam tml rtno = let abstract_return_type_context_glob_constr tml rtn = abstract_return_type_context (fun {CAst.v=(_,nal)} -> nal) (fun na c -> DAst.make @@ - GLambda(na,Explicit,DAst.make @@ GHole(Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None),c)) tml rtn + GLambda(na,Explicit,DAst.make @@ GHole(Evar_kinds.InternalHole,IntroAnonymous,None),c)) tml rtn let abstract_return_type_context_notation_constr tml rtn = abstract_return_type_context snd - (fun na c -> NLambda(na,NHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None),c)) tml rtn + (fun na c -> NLambda(na,NHole (Evar_kinds.InternalHole, IntroAnonymous, None),c)) tml rtn let is_term_meta id metas = try match Id.List.assoc id metas with _,(NtnTypeConstr | NtnTypeConstrList) -> true | _ -> false @@ -1194,7 +1194,7 @@ let rec match_ inner u alp metas sigma a1 a2 = | GCast(t1, c1), NCast(t2, c2) -> match_cast (match_in u alp metas) (match_in u alp metas sigma t1 t2) c1 c2 | GSort (GType _), NSort (GType _) when not u -> sigma - | GSort s1, NSort s2 when Miscops.glob_sort_eq s1 s2 -> sigma + | GSort s1, NSort s2 when glob_sort_eq s1 s2 -> sigma | GPatVar _, NHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match | a, NHole _ -> sigma @@ -1208,7 +1208,7 @@ let rec match_ inner u alp metas sigma a1 a2 = let avoid = Id.Set.union (free_glob_vars a1) (* as in Namegen: *) (glob_visible_short_qualid a1) in let id' = Namegen.next_ident_away id avoid in - let t1 = DAst.make @@ GHole(Evar_kinds.BinderType (Name id'),Misctypes.IntroAnonymous,None) in + let t1 = DAst.make @@ GHole(Evar_kinds.BinderType (Name id'),IntroAnonymous,None) in let sigma = match t2 with | NHole _ -> sigma | NVar id2 -> bind_term_env alp sigma id2 t1 @@ -1241,7 +1241,7 @@ and match_extended_binders ?loc isprod u alp metas na1 na2 bk t sigma b1 b2 = let store, get = set_temporary_memory () in match na1, DAst.get b1, na2 with (* Matching individual binders as part of a recursive pattern *) - | Name p, GCases (LetPatternStyle,None,[(e,_)],(_::_ as eqns)), Name id + | Name p, GCases (Constr.LetPatternStyle,None,[(e,_)],(_::_ as eqns)), Name id when is_gvar p e && is_bindinglist_meta id metas && List.length (store (Detyping.factorize_eqns eqns)) = 1 -> (match get () with | [{CAst.v=(ids,disj_of_patl,b1)}] -> diff --git a/interp/notation_term.ml b/interp/notation_term.ml index 52a6354a0..6d9effcef 100644 --- a/interp/notation_term.ml +++ b/interp/notation_term.ml @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Misctypes open Glob_term (** [notation_constr] *) @@ -25,7 +24,7 @@ type notation_constr = | NRef of GlobRef.t | NVar of Id.t | NApp of notation_constr * notation_constr list - | NHole of Evar_kinds.t * Misctypes.intro_pattern_naming_expr * Genarg.glob_generic_argument option + | NHole of Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option | NList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool (** Part only in [glob_constr] *) | NLambda of Name.t * notation_constr * notation_constr diff --git a/interp/tactypes.ml b/interp/tactypes.ml index 83e42be89..f19abefee 100644 --- a/interp/tactypes.ml +++ b/interp/tactypes.ml @@ -15,7 +15,35 @@ open Names open Constrexpr open Pattern -open Misctypes + +(** Introduction patterns *) + +type 'constr intro_pattern_expr = + | IntroForthcoming of bool + | IntroNaming of Namegen.intro_pattern_naming_expr + | IntroAction of 'constr intro_pattern_action_expr +and 'constr intro_pattern_action_expr = + | IntroWildcard + | IntroOrAndPattern of 'constr or_and_intro_pattern_expr + | IntroInjection of ('constr intro_pattern_expr) CAst.t list + | IntroApplyOn of 'constr CAst.t * 'constr intro_pattern_expr CAst.t + | IntroRewrite of bool +and 'constr or_and_intro_pattern_expr = + | IntroOrPattern of ('constr intro_pattern_expr) CAst.t list list + | IntroAndPattern of ('constr intro_pattern_expr) CAst.t list + +(** Bindings *) + +type quantified_hypothesis = AnonHyp of int | NamedHyp of Id.t + +type 'a explicit_bindings = (quantified_hypothesis * 'a) CAst.t list + +type 'a bindings = + | ImplicitBindings of 'a list + | ExplicitBindings of 'a explicit_bindings + | NoBindings + +type 'a with_bindings = 'a * 'a bindings (** In globalize tactics, we need to keep the initial [constr_expr] to recompute in the environment by the effective calls to Intro, Inversion, etc @@ -31,4 +59,4 @@ type delayed_open_constr_with_bindings = EConstr.constr with_bindings delayed_op type intro_pattern = delayed_open_constr intro_pattern_expr CAst.t type intro_patterns = delayed_open_constr intro_pattern_expr CAst.t list type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr CAst.t -type intro_pattern_naming = intro_pattern_naming_expr CAst.t +type intro_pattern_naming = Namegen.intro_pattern_naming_expr CAst.t diff --git a/library/misctypes.ml b/library/misctypes.ml deleted file mode 100644 index 7cd1a83be..000000000 --- a/library/misctypes.ml +++ /dev/null @@ -1,86 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* + | GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),IntroAnonymous,s) -> decr occref; if Int.equal !occref 0 then tc else (incr locref; DAst.make ~loc:(Loc.make_loc (!locref,0)) @@ - GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),Misctypes.IntroAnonymous,s)) + GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),IntroAnonymous,s)) | _ -> map_glob_constr_left_to_right substrec c in substrec t diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index ed54320a5..de9ff2875 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -12,9 +12,11 @@ DECLARE PLUGIN "ltac_plugin" open Util open Pp +open Glob_term open Constrexpr open Tacexpr open Misctypes +open Namegen open Genarg open Genredexpr open Tok (* necessary for camlp5 *) diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index 079001ee4..2189e224f 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -11,7 +11,6 @@ (* Syntax for rewriting with strategies *) open Names -open Misctypes open Locus open Constrexpr open Glob_term @@ -20,6 +19,7 @@ open Extraargs open Tacmach open Rewrite open Stdarg +open Tactypes open Pcoq.Prim open Pcoq.Constr open Pvernac.Vernac_ diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index 038d55e4b..c91c160f0 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -12,12 +12,14 @@ open Pp open CErrors open Util open Names +open Namegen open Tacexpr open Genredexpr open Constrexpr open Libnames open Tok open Misctypes +open Tactypes open Locus open Decl_kinds diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli index de23d2f8e..a75ca8ecb 100644 --- a/plugins/ltac/pltac.mli +++ b/plugins/ltac/pltac.mli @@ -16,6 +16,7 @@ open Constrexpr open Tacexpr open Genredexpr open Misctypes +open Tactypes val open_constr : constr_expr Gram.entry val constr_with_bindings : constr_expr with_bindings Gram.entry diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 894d91258..7b72a4bf9 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -20,6 +20,7 @@ open Stdarg open Libnames open Notation_gram open Misctypes +open Tactypes open Locus open Decl_kinds open Genredexpr @@ -749,7 +750,7 @@ let pr_goal_selector ~toplevel s = | TacIntroPattern (ev,(_::_ as p)) -> hov 1 (primitive (if ev then "eintros" else "intros") ++ (match p with - | [{CAst.v=Misctypes.IntroForthcoming false}] -> mt () + | [{CAst.v=IntroForthcoming false}] -> mt () | _ -> spc () ++ prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p)) | TacApply (a,ev,cb,inhyp) -> hov 1 ( diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 5d2a99618..c14874d6c 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -19,6 +19,7 @@ open Environ open Constrexpr open Notation_gram open Tacexpr +open Tactypes type 'a grammar_tactic_prod_item_expr = | TacTerm of string diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index b91315aca..cd04f4ae9 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -26,7 +26,7 @@ open Classes open Constrexpr open Globnames open Evd -open Misctypes +open Tactypes open Locus open Locusops open Decl_kinds @@ -1846,7 +1846,7 @@ let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans = (CAst.make @@ Ident (Id.of_string "Equivalence_Symmetric"), lemma2); (CAst.make @@ Ident (Id.of_string "Equivalence_Transitive"), lemma3)]) -let cHole = CAst.make @@ CHole (None, Misctypes.IntroAnonymous, None) +let cHole = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None) let proper_projection sigma r ty = let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i)) in diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index 1e3d4733b..0d014a0bf 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -12,9 +12,9 @@ open Names open Environ open EConstr open Constrexpr -open Tacexpr -open Misctypes open Evd +open Tactypes +open Tacexpr open Tacinterp (** TODO: document and clean me! *) diff --git a/plugins/ltac/tacarg.mli b/plugins/ltac/tacarg.mli index 59473a5e5..1abe7cd6f 100644 --- a/plugins/ltac/tacarg.mli +++ b/plugins/ltac/tacarg.mli @@ -11,7 +11,7 @@ open Genarg open Tacexpr open Constrexpr -open Misctypes +open Tactypes (** Generic arguments based on Ltac. *) diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index 3812a2ba2..27acbb629 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -13,6 +13,8 @@ open Names open Constr open EConstr open Misctypes +open Namegen +open Tactypes open Genarg open Stdarg open Geninterp diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli index 5185217cd..31bce197b 100644 --- a/plugins/ltac/taccoerce.mli +++ b/plugins/ltac/taccoerce.mli @@ -14,6 +14,7 @@ open EConstr open Misctypes open Genarg open Geninterp +open Tactypes (** Coercions from highest level generic arguments to actual data used by Ltac interpretation. Those functions examinate dynamic types and try to return @@ -56,7 +57,7 @@ val coerce_to_ident_not_fresh : Environ.env -> Evd.evar_map -> Value.t -> Id.t val coerce_to_intro_pattern : Environ.env -> Evd.evar_map -> Value.t -> Tacexpr.delayed_open_constr intro_pattern_expr val coerce_to_intro_pattern_naming : - Environ.env -> Evd.evar_map -> Value.t -> intro_pattern_naming_expr + Environ.env -> Evd.evar_map -> Value.t -> Namegen.intro_pattern_naming_expr val coerce_to_hint_base : Value.t -> string diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index d6f7a461b..289434d8a 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -16,6 +16,7 @@ open Genredexpr open Genarg open Pattern open Misctypes +open Tactypes open Locus type ltac_constant = KerName.t @@ -75,7 +76,7 @@ type 'id message_token = type ('dconstr,'id) induction_clause = 'dconstr with_bindings Tactics.destruction_arg * - (intro_pattern_naming_expr CAst.t option (* eqn:... *) + (Namegen.intro_pattern_naming_expr CAst.t option (* eqn:... *) * 'dconstr or_and_intro_pattern_expr CAst.t or_var option) (* as ... *) * 'id clause_expr option (* in ... *) @@ -134,7 +135,7 @@ type delayed_open_constr = EConstr.constr delayed_open type intro_pattern = delayed_open_constr intro_pattern_expr CAst.t type intro_patterns = delayed_open_constr intro_pattern_expr CAst.t list type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr CAst.t -type intro_pattern_naming = intro_pattern_naming_expr CAst.t +type intro_pattern_naming = Namegen.intro_pattern_naming_expr CAst.t (** Generic expressions for atomic tactics *) @@ -152,7 +153,7 @@ type 'a gen_atomic_tactic_expr = 'dtrm intro_pattern_expr CAst.t option * 'trm | TacGeneralize of ('trm with_occurrences * Name.t) list | TacLetTac of evars_flag * Name.t * 'trm * 'nam clause_expr * letin_flag * - intro_pattern_naming_expr CAst.t option + Namegen.intro_pattern_naming_expr CAst.t option (* Derived basic tactics *) | TacInductionDestruct of diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index d6f7a461b..42f6883b4 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -17,6 +17,7 @@ open Genarg open Pattern open Misctypes open Locus +open Tactypes type ltac_constant = KerName.t @@ -75,7 +76,7 @@ type 'id message_token = type ('dconstr,'id) induction_clause = 'dconstr with_bindings Tactics.destruction_arg * - (intro_pattern_naming_expr CAst.t option (* eqn:... *) + (Namegen.intro_pattern_naming_expr CAst.t option (* eqn:... *) * 'dconstr or_and_intro_pattern_expr CAst.t or_var option) (* as ... *) * 'id clause_expr option (* in ... *) @@ -134,7 +135,7 @@ type delayed_open_constr = EConstr.constr delayed_open type intro_pattern = delayed_open_constr intro_pattern_expr CAst.t type intro_patterns = delayed_open_constr intro_pattern_expr CAst.t list type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr CAst.t -type intro_pattern_naming = intro_pattern_naming_expr CAst.t +type intro_pattern_naming = Namegen.intro_pattern_naming_expr CAst.t (** Generic expressions for atomic tactics *) @@ -152,7 +153,7 @@ type 'a gen_atomic_tactic_expr = 'dtrm intro_pattern_expr CAst.t option * 'trm | TacGeneralize of ('trm with_occurrences * Name.t) list | TacLetTac of evars_flag * Name.t * 'trm * 'nam clause_expr * letin_flag * - intro_pattern_naming_expr CAst.t option + Namegen.intro_pattern_naming_expr CAst.t option (* Derived basic tactics *) | TacInductionDestruct of diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 9ad9e1520..2a5c38024 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -28,6 +28,8 @@ open Genarg open Stdarg open Tacarg open Misctypes +open Namegen +open Tactypes open Locus (** Globalization of tactic expressions : diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli index fb32508cc..9146fced2 100644 --- a/plugins/ltac/tacintern.mli +++ b/plugins/ltac/tacintern.mli @@ -12,7 +12,7 @@ open Names open Tacexpr open Genarg open Constrexpr -open Misctypes +open Tactypes (** Globalization of tactic expressions : Conversion from [raw_tactic_expr] to [glob_tactic_expr] *) diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index a93cf5ae7..04c93eae3 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -12,6 +12,7 @@ open Constrintern open Patternops open Pp open CAst +open Namegen open Genredexpr open Glob_term open Glob_ops @@ -36,6 +37,7 @@ open Tacarg open Printer open Pretyping open Misctypes +open Tactypes open Locus open Tacintern open Taccoerce diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index bd44bdbea..e18f6ab19 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -15,6 +15,7 @@ open Tacexpr open Genarg open Redexpr open Misctypes +open Tactypes val ltac_trace_info : ltac_trace Exninfo.t diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index 50bf687b1..0b86a68b0 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -15,6 +15,7 @@ open Genarg open Stdarg open Tacarg open Misctypes +open Tactypes open Globnames open Genredexpr open Patternops diff --git a/plugins/ltac/tacsubst.mli b/plugins/ltac/tacsubst.mli index 0a894791b..d406686c5 100644 --- a/plugins/ltac/tacsubst.mli +++ b/plugins/ltac/tacsubst.mli @@ -11,7 +11,7 @@ open Tacexpr open Mod_subst open Genarg -open Misctypes +open Tactypes (** Substitution of tactics at module closing time *) diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index 8eeb8903e..368c20469 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -94,7 +94,7 @@ let clear id = Tactics.clear [id] let assumption = Tactics.assumption -let split = Tactics.split_with_bindings false [Misctypes.NoBindings] +let split = Tactics.split_with_bindings false [Tactypes.NoBindings] (** Test *) @@ -175,7 +175,7 @@ let flatten_contravariant_disj _ ist = | Some (_,args) -> let map i arg = let typ = mkArrow arg c in - let ci = Tactics.constructor_tac false None (succ i) Misctypes.NoBindings in + let ci = Tactics.constructor_tac false None (succ i) Tactypes.NoBindings in let by = tclTHENLIST [intro; apply hyp; ci; assumption] in assert_ ~by typ in diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 68620dbfc..f22147f8b 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -23,6 +23,7 @@ open Names open Goptions open Mutils open Constr +open Tactypes (** * Debug flag @@ -1727,7 +1728,7 @@ let micromega_gen let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in - let ipat_of_name id = Some (CAst.make @@ Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in + let ipat_of_name id = Some (CAst.make @@ IntroNaming (Namegen.IntroIdentifier id)) in let goal_name = fresh_id Id.Set.empty (Names.Id.of_string "__arith") gl in let env' = List.map (fun (id,i) -> EConstr.mkVar id,i) vars in @@ -1842,7 +1843,7 @@ let micromega_genr prover tac = let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in - let ipat_of_name id = Some (CAst.make @@ Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in + let ipat_of_name id = Some (CAst.make @@ IntroNaming (Namegen.IntroIdentifier id)) in let goal_name = fresh_id Id.Set.empty (Names.Id.of_string "__arith") gl in let env' = List.map (fun (id,i) -> EConstr.mkVar id,i) vars in diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index c615cf278..6f4138828 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -29,7 +29,7 @@ open Libnames open Globnames open Nametab open Contradiction -open Misctypes +open Tactypes open Context.Named.Declaration module NamedDecl = Context.Named.Declaration diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 3f6503e73..ea7216832 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -184,7 +184,7 @@ open Globnames open Misctypes open Decl_kinds -let mkRHole = DAst.make @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None) +let mkRHole = DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None) let rec mkRHoles n = if n > 0 then mkRHole :: mkRHoles (n - 1) else [] let rec isRHoles cl = match cl with @@ -254,7 +254,7 @@ let interp_refine ist gl rc = let interp_open_constr ist gl gc = - let (sigma, (c, _)) = Tacinterp.interp_open_constr_with_bindings ist (pf_env gl) (project gl) (gc, Misctypes.NoBindings) in + let (sigma, (c, _)) = Tacinterp.interp_open_constr_with_bindings ist (pf_env gl) (project gl) (gc, Tactypes.NoBindings) in (project gl, (sigma, c)) let interp_term ist gl (_, c) = snd (interp_open_constr ist gl c) @@ -861,8 +861,8 @@ let mkCProp loc = CAst.make ?loc @@ CSort GProp let mkCType loc = CAst.make ?loc @@ CSort (GType []) let mkCVar ?loc id = CAst.make ?loc @@ CRef (CAst.make ?loc @@ Ident id, None) let rec mkCHoles ?loc n = - if n <= 0 then [] else (CAst.make ?loc @@ CHole (None, IntroAnonymous, None)) :: mkCHoles ?loc (n - 1) -let mkCHole loc = CAst.make ?loc @@ CHole (None, IntroAnonymous, None) + if n <= 0 then [] else (CAst.make ?loc @@ CHole (None, Namegen.IntroAnonymous, None)) :: mkCHoles ?loc (n - 1) +let mkCHole loc = CAst.make ?loc @@ CHole (None, Namegen.IntroAnonymous, None) let mkCLambda ?loc name ty t = CAst.make ?loc @@ CLambdaN ([CLocalAssum([CAst.make ?loc name], Default Explicit, ty)], t) let mkCArrow ?loc ty t = CAst.make ?loc @@ diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 83b4d6562..fbe3b000f 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -17,7 +17,7 @@ open Term open Constr open Termops open Globnames -open Misctypes +open Tactypes open Tacmach open Ssrmatching_plugin diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index c6beb08c5..2c046190f 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -86,7 +86,6 @@ let _ = open Constrexpr open Glob_term -open Misctypes let combineCG t1 t2 f g = match t1, t2 with | (x, (t1, None)), (_, (t2, None)) -> x, (g t1 t2, None) diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index fbfbdb110..9d7fc254c 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -29,6 +29,8 @@ open Extraargs open Ppconstr open Misctypes +open Namegen +open Tactypes open Decl_kinds open Constrexpr open Constrexpr_ops @@ -543,7 +545,7 @@ END let remove_loc x = x.CAst.v -let ipat_of_intro_pattern p = Misctypes.( +let ipat_of_intro_pattern p = Tactypes.( let rec ipat_of_intro_pattern = function | IntroNaming (IntroIdentifier id) -> IPatId id | IntroAction IntroWildcard -> IPatAnon Drop @@ -595,16 +597,15 @@ let intern_ipats ist = List.map (intern_ipat ist) let interp_intro_pattern = interp_wit wit_intro_pattern -let interp_introid ist gl id = Misctypes.( +let interp_introid ist gl id = try IntroNaming (IntroIdentifier (hyp_id (snd (interp_hyp ist gl (SsrHyp (Loc.tag id)))))) with _ -> (snd (interp_intro_pattern ist gl (CAst.make @@ IntroNaming (IntroIdentifier id)))).CAst.v -) let get_intro_id = function | IntroNaming (IntroIdentifier id) -> id | _ -> assert false -let rec add_intro_pattern_hyps ipat hyps = Misctypes.( +let rec add_intro_pattern_hyps ipat hyps = let {CAst.loc=loc;v=ipat} = ipat in match ipat with | IntroNaming (IntroIdentifier id) -> @@ -623,7 +624,6 @@ let rec add_intro_pattern_hyps ipat hyps = Misctypes.( | IntroForthcoming _ -> (* As in ipat_of_intro_pattern, was unable to determine which kind of ipat interp_introid could return [HH] *) assert false -) (* We interp the ipat using the standard ltac machinery for ids, since * we have no clue what a name could be bound to (maybe another ipat) *) @@ -1064,7 +1064,7 @@ let rec format_constr_expr h0 c0 = let open CAst in match h0, c0 with | BFdef :: h, { v = CLetIn({CAst.v=x}, v, oty, c) } -> let bs, c' = format_constr_expr h c in Bdef (x, oty, v) :: bs, c' - | [BFcast], { v = CCast (c, CastConv t) } -> + | [BFcast], { v = CCast (c, Glob_term.CastConv t) } -> [Bcast t], c | BFrec (has_str, has_cast) :: h, { v = CFix ( _, [_, (Some locn, CStructRec), bl, t, c]) } -> @@ -1093,7 +1093,7 @@ let wit_ssrfwdfmt = add_genarg "ssrfwdfmt" pr_fwdfmt let mkFwdVal fk c = ((fk, []), c) let mkssrFwdVal fk c = ((fk, []), (c,None)) -let dC t = CastConv t +let dC t = Glob_term.CastConv t let same_ist { interp_env = x } { interp_env = y } = match x,y with @@ -1210,8 +1210,8 @@ let push_binders c2 bs = | [] -> c | _ -> anomaly "binder not a lambda nor a let in" in match c2 with - | { loc; v = CCast (ct, CastConv cty) } -> - CAst.make ?loc @@ (CCast (loop false ct bs, CastConv (loop true cty bs))) + | { loc; v = CCast (ct, Glob_term.CastConv cty) } -> + CAst.make ?loc @@ (CCast (loop false ct bs, Glob_term.CastConv (loop true cty bs))) | ct -> loop false ct bs let rec fix_binders = let open CAst in function diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index 29a936381..faebe3179 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -157,7 +157,7 @@ let tclINJ_CONSTR_IST ist p = let mkGHole = DAst.make - (Glob_term.GHole(Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None)) + (Glob_term.GHole(Evar_kinds.InternalHole, Namegen.IntroAnonymous, None)) let rec mkGHoles n = if n > 0 then mkGHole :: mkGHoles (n - 1) else [] let mkGApp f args = if args = [] then f diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index b1c5e131f..69d944fa1 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -40,7 +40,7 @@ open Pretyping open Ppconstr open Printer open Globnames -open Misctypes +open Namegen open Decl_kinds open Evar_kinds open Constrexpr diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 1edce17bd..aa1c23f52 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -2103,7 +2103,7 @@ let mk_JMeq_refl evdref typ x = let hole na = DAst.make @@ GHole (Evar_kinds.QuestionMark (Evar_kinds.Define false,na), - Misctypes.IntroAnonymous, None) + IntroAnonymous, None) let constr_of_pat env evdref arsign pat avoid = let rec typ env (ty, realargs) pat avoid = diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index e6cfe1f76..df89d9eac 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -27,7 +27,6 @@ open Libnames open Globnames open Nametab open Mod_subst -open Misctypes open Decl_kinds open Context.Named.Declaration open Ltac_pretype @@ -1027,7 +1026,7 @@ let rec subst_glob_constr subst = DAst.map (function | GCast (r1,k) as raw -> let r1' = subst_glob_constr subst r1 in - let k' = Miscops.smartmap_cast_type (subst_glob_constr subst) k in + let k' = smartmap_cast_type (subst_glob_constr subst) k in if r1' == r1 && k' == k then raw else GCast (r1',k') | GProj (p,c) as raw -> diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 63618c918..71a457280 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -11,10 +11,8 @@ open Util open CAst open Names -open Constr open Nameops open Globnames -open Misctypes open Glob_term open Evar_kinds open Ltac_pretype @@ -48,12 +46,20 @@ let map_glob_decl_left_to_right f (na,k,obd,ty) = let comp2 = f ty in (na,k,comp1,comp2) + +let glob_sort_eq g1 g2 = let open Glob_term in match g1, g2 with +| GProp, GProp -> true +| GSet, GSet -> true +| GType l1, GType l2 -> + List.equal (Option.equal (fun (x,m) (y,n) -> Libnames.eq_reference x y && Int.equal m n)) l1 l2 +| _ -> false + let binding_kind_eq bk1 bk2 = match bk1, bk2 with | Decl_kinds.Explicit, Decl_kinds.Explicit -> true | Decl_kinds.Implicit, Decl_kinds.Implicit -> true | (Decl_kinds.Explicit | Decl_kinds.Implicit), _ -> false -let case_style_eq s1 s2 = match s1, s2 with +let case_style_eq s1 s2 = let open Constr in match s1, s2 with | LetStyle, LetStyle -> true | IfStyle, IfStyle -> true | LetPatternStyle, LetPatternStyle -> true @@ -141,10 +147,10 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with fix_kind_eq f kn1 kn2 && Array.equal Id.equal id1 id2 && Array.equal (fun l1 l2 -> List.equal (glob_decl_eq f) l1 l2) decl1 decl2 && Array.equal f c1 c2 && Array.equal f t1 t2 - | GSort s1, GSort s2 -> Miscops.glob_sort_eq s1 s2 + | GSort s1, GSort s2 -> glob_sort_eq s1 s2 | GHole (kn1, nam1, gn1), GHole (kn2, nam2, gn2) -> Option.equal (==) gn1 gn2 (** Only thing sensible *) && - Miscops.intro_pattern_naming_eq nam1 nam2 + Namegen.intro_pattern_naming_eq nam1 nam2 | GCast (c1, t1), GCast (c2, t2) -> f c1 c2 && cast_type_eq f t1 t2 | GProj (p1, t1), GProj (p2, t2) -> @@ -154,6 +160,21 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with let rec glob_constr_eq c = mk_glob_constr_eq glob_constr_eq c +(** Mapping [cast_type] *) + +let map_cast_type f = function + | CastConv a -> CastConv (f a) + | CastVM a -> CastVM (f a) + | CastCoerce -> CastCoerce + | CastNative a -> CastNative (f a) + +let smartmap_cast_type f c = + match c with + | CastConv a -> let a' = f a in if a' == a then c else CastConv a' + | CastVM a -> let a' = f a in if a' == a then c else CastVM a' + | CastCoerce -> CastCoerce + | CastNative a -> let a' = f a in if a' == a then c else CastNative a' + let map_glob_constr_left_to_right f = DAst.map (function | GApp (g,args) -> let comp1 = f g in @@ -194,7 +215,7 @@ let map_glob_constr_left_to_right f = DAst.map (function GRec (fk,idl,comp1,comp2,comp3) | GCast (c,k) -> let comp1 = f c in - let comp2 = Miscops.map_cast_type f k in + let comp2 = map_cast_type f k in GCast (comp1,comp2) | GProj (p,c) -> GProj (p, f c) @@ -539,7 +560,7 @@ let rec glob_constr_of_cases_pattern_aux isclosed x = DAst.map_with_loc (fun ?lo | PatVar (Name id) when not isclosed -> GVar id | PatVar Anonymous when not isclosed -> - GHole (Evar_kinds.QuestionMark (Define false,Anonymous),Misctypes.IntroAnonymous,None) + GHole (Evar_kinds.QuestionMark (Define false,Anonymous),Namegen.IntroAnonymous,None) | _ -> raise Not_found ) x diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 124440f5d..c967f4e88 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -13,6 +13,8 @@ open Glob_term (** Equalities *) +val glob_sort_eq : Glob_term.glob_sort -> Glob_term.glob_sort -> bool + val cases_pattern_eq : 'a cases_pattern_g -> 'a cases_pattern_g -> bool val alias_of_pat : 'a cases_pattern_g -> Name.t @@ -20,10 +22,15 @@ val alias_of_pat : 'a cases_pattern_g -> Name.t val set_pat_alias : Id.t -> 'a cases_pattern_g -> 'a cases_pattern_g val cast_type_eq : ('a -> 'a -> bool) -> - 'a Misctypes.cast_type -> 'a Misctypes.cast_type -> bool + 'a cast_type -> 'a cast_type -> bool val glob_constr_eq : 'a glob_constr_g -> 'a glob_constr_g -> bool +(** Mapping [cast_type] *) + +val map_cast_type : ('a -> 'b) -> 'a cast_type -> 'b cast_type +val smartmap_cast_type : ('a -> 'a) -> 'a cast_type -> 'a cast_type + (** Operations on [glob_constr] *) val cases_pattern_loc : 'a cases_pattern_g -> Loc.t option diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index 6ecb479e6..54fa5328f 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -18,7 +18,6 @@ open Names open Decl_kinds -open Misctypes type existential_name = Id.t @@ -41,6 +40,14 @@ type glob_constraint = glob_level * Univ.constraint_type * glob_level type sort_info = (Libnames.reference * int) option list type glob_sort = sort_info glob_sort_gen +(** Casts *) + +type 'a cast_type = + | CastConv of 'a + | CastVM of 'a + | CastCoerce (** Cast to a base type (eg, an underlying inductive type) *) + | CastNative of 'a + (** The kind of patterns that occurs in "match ... with ... end" locs here refers to the ident's location, not whole pat *) @@ -73,7 +80,7 @@ type 'a glob_constr_r = | GRec of 'a fix_kind_g * Id.t array * 'a glob_decl_g list array * 'a glob_constr_g array * 'a glob_constr_g array | GSort of glob_sort - | GHole of Evar_kinds.t * intro_pattern_naming_expr * Genarg.glob_generic_argument option + | GHole of Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option | GCast of 'a glob_constr_g * 'a glob_constr_g cast_type | GProj of Projection.t * 'a glob_constr_g and 'a glob_constr_g = ('a glob_constr_r, 'a) DAst.t diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml deleted file mode 100644 index 1697e54ab..000000000 --- a/pretyping/miscops.ml +++ /dev/null @@ -1,55 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* CastConv (f a) - | CastVM a -> CastVM (f a) - | CastCoerce -> CastCoerce - | CastNative a -> CastNative (f a) - -let smartmap_cast_type f c = - match c with - | CastConv a -> let a' = f a in if a' == a then c else CastConv a' - | CastVM a -> let a' = f a in if a' == a then c else CastVM a' - | CastCoerce -> CastCoerce - | CastNative a -> let a' = f a in if a' == a then c else CastNative a' - -(** Equalities on [glob_sort] *) - -let glob_sort_eq g1 g2 = let open Glob_term in match g1, g2 with -| GProp, GProp -> true -| GSet, GSet -> true -| GType l1, GType l2 -> - List.equal (Option.equal (fun (x,m) (y,n) -> Libnames.eq_reference x y && Int.equal m n)) l1 l2 -| _ -> false - -let intro_pattern_naming_eq nam1 nam2 = match nam1, nam2 with -| IntroAnonymous, IntroAnonymous -> true -| IntroIdentifier id1, IntroIdentifier id2 -> Names.Id.equal id1 id2 -| IntroFresh id1, IntroFresh id2 -> Names.Id.equal id1 id2 -| _ -> false - -(** Mapping bindings *) - -let map_explicit_bindings f l = - let map = CAst.map (fun (hyp, x) -> (hyp, f x)) in - List.map map l - -let map_bindings f = function -| ImplicitBindings l -> ImplicitBindings (List.map f l) -| ExplicitBindings expl -> ExplicitBindings (map_explicit_bindings f expl) -| NoBindings -> NoBindings - -let map_with_bindings f (x, bl) = (f x, map_bindings f bl) diff --git a/pretyping/miscops.mli b/pretyping/miscops.mli deleted file mode 100644 index 6a84fb9eb..000000000 --- a/pretyping/miscops.mli +++ /dev/null @@ -1,30 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* 'b) -> 'a cast_type -> 'b cast_type -val smartmap_cast_type : ('a -> 'a) -> 'a cast_type -> 'a cast_type - -(** Equalities on [glob_sort] *) - -val glob_sort_eq : Glob_term.glob_sort -> Glob_term.glob_sort -> bool - -(** Equalities on [intro_pattern_naming] *) - -val intro_pattern_naming_eq : - intro_pattern_naming_expr -> intro_pattern_naming_expr -> bool - -(** Mapping bindings *) - -val map_bindings : ('a -> 'b) -> 'a bindings -> 'b bindings -val map_with_bindings : ('a -> 'b) -> 'a with_bindings -> 'b with_bindings diff --git a/pretyping/misctypes.ml b/pretyping/misctypes.ml new file mode 100644 index 000000000..c66c9b1b8 --- /dev/null +++ b/pretyping/misctypes.ml @@ -0,0 +1,37 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* + | CHole (_,IntroIdentifier id,_) -> return (str "?[" ++ pr_id id ++ str "]", latom) - | CHole (_,Misctypes.IntroFresh id,_) -> + | CHole (_,IntroFresh id,_) -> return (str "?[?" ++ pr_id id ++ str "]", latom) | CHole (_,_,_) -> return (str "_", latom) diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 450fcddfd..79b7e1599 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -26,7 +26,7 @@ open Tacred open Pretype_errors open Evarutil open Unification -open Misctypes +open Tactypes (******************************************************************) (* Clausal environments *) diff --git a/proofs/clenv.mli b/proofs/clenv.mli index b85c4fc51..f9506290a 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -18,7 +18,7 @@ open Environ open Evd open EConstr open Unification -open Misctypes +open Tactypes (** {6 The Type of Constructions clausale environments.} *) diff --git a/proofs/logic.ml b/proofs/logic.ml index 95c30d815..e8ca71993 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -23,7 +23,6 @@ open Typing open Proof_type open Type_errors open Retyping -open Misctypes module NamedDecl = Context.Named.Declaration @@ -185,6 +184,22 @@ let check_decl_position env sigma sign d = * on the right side [right] if [toleft=false]. * If [with_dep] then dependent hypotheses are moved accordingly. *) +(** Move destination for hypothesis *) + +type 'id move_location = + | MoveAfter of 'id + | MoveBefore of 'id + | MoveFirst + | MoveLast (** can be seen as "no move" when doing intro *) + +(** Printing of [move_location] *) + +let pr_move_location pr_id = function + | MoveAfter id -> brk(1,1) ++ str "after " ++ pr_id id + | MoveBefore id -> brk(1,1) ++ str "before " ++ pr_id id + | MoveFirst -> str " at top" + | MoveLast -> str " at bottom" + let move_location_eq m1 m2 = match m1, m2 with | MoveAfter id1, MoveAfter id2 -> Id.equal id1 id2 | MoveBefore id1, MoveBefore id2 -> Id.equal id1 id2 @@ -236,7 +251,7 @@ let move_hyp sigma toleft (left,declfrom,right) hto = (first, d::middle) else user_err ~hdr:"move_hyp" (str "Cannot move " ++ Id.print (NamedDecl.get_id declfrom) ++ - Miscprint.pr_move_location Id.print hto ++ + pr_move_location Id.print hto ++ str (if toleft then ": it occurs in the type of " else ": it depends on ") ++ Id.print hyp ++ str ".") else diff --git a/proofs/logic.mli b/proofs/logic.mli index dc471bb5f..9db54732b 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -58,12 +58,23 @@ val error_no_such_hypothesis : Environ.env -> evar_map -> Id.t -> 'a val catchable_exception : exn -> bool +(** Move destination for hypothesis *) + +type 'id move_location = + | MoveAfter of 'id + | MoveBefore of 'id + | MoveFirst + | MoveLast (** can be seen as "no move" when doing intro *) + +val pr_move_location : + ('a -> Pp.t) -> 'a move_location -> Pp.t + val convert_hyp : bool -> Environ.named_context_val -> evar_map -> EConstr.named_declaration -> Environ.named_context_val -val move_hyp_in_named_context : Environ.env -> Evd.evar_map -> Id.t -> Id.t Misctypes.move_location -> +val move_hyp_in_named_context : Environ.env -> Evd.evar_map -> Id.t -> Id.t move_location -> Environ.named_context_val -> Environ.named_context_val val insert_decl_in_named_context : Evd.evar_map -> - EConstr.named_declaration -> Id.t Misctypes.move_location -> + EConstr.named_declaration -> Id.t move_location -> Environ.named_context_val -> Environ.named_context_val diff --git a/proofs/miscprint.ml b/proofs/miscprint.ml index 1a63ff673..ec17b8076 100644 --- a/proofs/miscprint.ml +++ b/proofs/miscprint.ml @@ -10,7 +10,7 @@ open Pp open Names -open Misctypes +open Tactypes (** Printing of [intro_pattern] *) @@ -20,7 +20,7 @@ let rec pr_intro_pattern prc {CAst.v=pat} = match pat with | IntroNaming p -> pr_intro_pattern_naming p | IntroAction p -> pr_intro_pattern_action prc p -and pr_intro_pattern_naming = function +and pr_intro_pattern_naming = let open Namegen in function | IntroIdentifier id -> Id.print id | IntroFresh id -> str "?" ++ Id.print id | IntroAnonymous -> str "?" @@ -43,14 +43,6 @@ and pr_or_and_intro_pattern prc = function hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc (pr_intro_pattern prc)) pll) ++ str "]" -(** Printing of [move_location] *) - -let pr_move_location pr_id = function - | MoveAfter id -> brk(1,1) ++ str "after " ++ pr_id id - | MoveBefore id -> brk(1,1) ++ str "before " ++ pr_id id - | MoveFirst -> str " at top" - | MoveLast -> str " at bottom" - (** Printing of bindings *) let pr_binding prc = let open CAst in function | {loc;v=(NamedHyp id, c)} -> hov 1 (Names.Id.print id ++ str " := " ++ cut () ++ prc c) diff --git a/proofs/miscprint.mli b/proofs/miscprint.mli index 79790a277..f4e2e683d 100644 --- a/proofs/miscprint.mli +++ b/proofs/miscprint.mli @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Misctypes +open Tactypes (** Printing of [intro_pattern] *) @@ -18,13 +18,10 @@ val pr_intro_pattern : val pr_or_and_intro_pattern : ('a -> Pp.t) -> 'a or_and_intro_pattern_expr -> Pp.t -val pr_intro_pattern_naming : intro_pattern_naming_expr -> Pp.t +val pr_intro_pattern_naming : Namegen.intro_pattern_naming_expr -> Pp.t (** Printing of [move_location] *) -val pr_move_location : - ('a -> Pp.t) -> 'a move_location -> Pp.t - val pr_bindings : ('a -> Pp.t) -> ('a -> Pp.t) -> 'a bindings -> Pp.t diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index b92bc75bc..e12063fd4 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -14,7 +14,6 @@ open Hipattern open Tactics open Coqlib open Reductionops -open Misctypes open Proofview.Notations module NamedDecl = Context.Named.Declaration @@ -120,7 +119,7 @@ let contradiction_term (c,lbind as cl) = else Proofview.tclORELSE begin - if lbind = NoBindings then + if lbind = Tactypes.NoBindings then filter_hyp (fun c -> is_negation_of env sigma typ c) (fun id -> simplest_elim (mkApp (mkVar id,[|c|]))) else diff --git a/tactics/contradiction.mli b/tactics/contradiction.mli index 2b3a94758..4bb3263fb 100644 --- a/tactics/contradiction.mli +++ b/tactics/contradiction.mli @@ -9,7 +9,7 @@ (************************************************************************) open EConstr -open Misctypes +open Tactypes val absurd : constr -> unit Proofview.tactic val contradiction : constr with_bindings option -> unit Proofview.tactic diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index 176701d99..832014a61 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -24,11 +24,11 @@ open Tactics open Tacticals.New open Auto open Constr_matching -open Misctypes open Hipattern open Proofview.Notations open Tacmach.New open Coqlib +open Tactypes (* This file containts the implementation of the tactics ``Decide Equality'' and ``Compare''. They can be used to decide the @@ -58,14 +58,14 @@ let clear_last = let choose_eq eqonleft = if eqonleft then - left_with_bindings false Misctypes.NoBindings + left_with_bindings false NoBindings else - right_with_bindings false Misctypes.NoBindings + right_with_bindings false NoBindings let choose_noteq eqonleft = if eqonleft then - right_with_bindings false Misctypes.NoBindings + right_with_bindings false NoBindings else - left_with_bindings false Misctypes.NoBindings + left_with_bindings false NoBindings (* A surgical generalize which selects the right occurrences by hand *) (* This prevents issues where c2 is also a subterm of c1 (see e.g. #5449) *) diff --git a/tactics/equality.ml b/tactics/equality.ml index c91758787..1033c56c9 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -43,6 +43,7 @@ open Eqschemes open Locus open Locusops open Misctypes +open Tactypes open Proofview.Notations open Unification open Context.Named.Declaration diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 5d264058a..f9c4bed35 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -263,7 +263,7 @@ open Evar_kinds let mkPattern c = snd (Patternops.pattern_of_glob_constr c) let mkGApp f args = DAst.make @@ GApp (f, args) let mkGHole = DAst.make @@ - GHole (QuestionMark (Define false,Anonymous), Misctypes.IntroAnonymous, None) + GHole (QuestionMark (Define false,Anonymous), Namegen.IntroAnonymous, None) let mkGProd id c1 c2 = DAst.make @@ GProd (Name (Id.of_string id), Explicit, c1, c2) let mkGArrow c1 c2 = DAst.make @@ diff --git a/tactics/inv.ml b/tactics/inv.ml index 102b8e54d..755494c2d 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -26,7 +26,7 @@ open Tacticals.New open Tactics open Elim open Equality -open Misctypes +open Tactypes open Proofview.Notations module NamedDecl = Context.Named.Declaration @@ -332,7 +332,7 @@ let rec tclMAP_i allow_conj n tacfun = function (tacfun (get_names allow_conj a)) (tclMAP_i allow_conj (n-1) tacfun l) -let remember_first_eq id x = if !x == MoveLast then x := MoveAfter id +let remember_first_eq id x = if !x == Logic.MoveLast then x := Logic.MoveAfter id (* invariant: ProjectAndApply is responsible for erasing the clause which it is given as input @@ -375,7 +375,7 @@ let projectAndApply as_mode thin avoid id eqname names depids = [if as_mode then clear [id] else tclIDTAC; (tclMAP_i (false,false) neqns (function (idopt,_) -> tclTRY (tclTHEN - (intro_move_avoid idopt avoid MoveLast) + (intro_move_avoid idopt avoid Logic.MoveLast) (* try again to substitute and if still not a variable after *) (* decomposition, arbitrarily try to rewrite RL !? *) (tclTRY (onLastHypId (substHypIfVariable (fun id -> subst_hyp false id)))))) @@ -404,7 +404,7 @@ let nLastDecls i tac = let rewrite_equations as_mode othin neqns names ba = Proofview.Goal.enter begin fun gl -> let (depids,nodepids) = split_dep_and_nodep ba.Tacticals.assums gl in - let first_eq = ref MoveLast in + let first_eq = ref Logic.MoveLast in let avoid = if as_mode then Id.Set.of_list (List.map NamedDecl.get_id nodepids) else Id.Set.empty in match othin with | Some thin -> @@ -416,20 +416,20 @@ let rewrite_equations as_mode othin neqns names ba = (nLastDecls neqns (fun ctx -> clear (ids_of_named_context ctx))); tclMAP_i (true,false) neqns (fun (idopt,names) -> (tclTHEN - (intro_move_avoid idopt avoid MoveLast) + (intro_move_avoid idopt avoid Logic.MoveLast) (onLastHypId (fun id -> tclTRY (projectAndApply as_mode thin avoid id first_eq names depids))))) names; tclMAP (fun d -> tclIDTAC >>= fun () -> (* delay for [first_eq]. *) let idopt = if as_mode then Some (NamedDecl.get_id d) else None in - intro_move idopt (if thin then MoveLast else !first_eq)) + intro_move idopt (if thin then Logic.MoveLast else !first_eq)) nodepids; (tclMAP (fun d -> tclTRY (clear [NamedDecl.get_id d])) depids)] | None -> (* simple inversion *) if as_mode then tclMAP_i (false,true) neqns (fun (idopt,_) -> - intro_move idopt MoveLast) names + intro_move idopt Logic.MoveLast) names else (tclTHENLIST [tclDO neqns intro; diff --git a/tactics/inv.mli b/tactics/inv.mli index 9d4ffdd7b..bbd1f3352 100644 --- a/tactics/inv.mli +++ b/tactics/inv.mli @@ -10,7 +10,6 @@ open Names open EConstr -open Misctypes open Tactypes type inversion_status = Dep of constr option | NoDep diff --git a/tactics/leminv.mli b/tactics/leminv.mli index 2337a7901..f42e5a8b0 100644 --- a/tactics/leminv.mli +++ b/tactics/leminv.mli @@ -11,7 +11,7 @@ open Names open EConstr open Constrexpr -open Misctypes +open Tactypes val lemInv_clause : quantified_hypothesis -> constr -> Id.t list -> unit Proofview.tactic diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 732d06f8a..53a02f89b 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -159,8 +159,6 @@ type branch_assumptions = { ba : branch_args; (* the branch args *) assums : named_context} (* the list of assumptions introduced *) -open Misctypes - let fix_empty_or_and_pattern nv l = (* 1- The syntax does not distinguish between "[ ]" for one clause with no names and "[ ]" for no clause at all *) @@ -194,7 +192,7 @@ let check_or_and_pattern_size ?loc check_and names branchsigns = if not (Int.equal p p1 || Int.equal p p2) then err1 p1 p2; if Int.equal p p1 then IntroAndPattern - (List.extend branchsigns.(0) (CAst.make @@ IntroNaming IntroAnonymous) l) + (List.extend branchsigns.(0) (CAst.make @@ IntroNaming Namegen.IntroAnonymous) l) else names else diff --git a/tactics/tactics.ml b/tactics/tactics.ml index b571b347d..cf07532c0 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -44,6 +44,7 @@ open Unification open Locus open Locusops open Misctypes +open Tactypes open Proofview.Notations open Context.Named.Declaration diff --git a/tactics/tactics.mli b/tactics/tactics.mli index b17330f13..086442e42 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -56,8 +56,8 @@ val find_intro_names : rel_context -> goal sigma -> Id.t list val intro : unit Proofview.tactic val introf : unit Proofview.tactic -val intro_move : Id.t option -> Id.t move_location -> unit Proofview.tactic -val intro_move_avoid : Id.t option -> Id.Set.t -> Id.t move_location -> unit Proofview.tactic +val intro_move : Id.t option -> Id.t Logic.move_location -> unit Proofview.tactic +val intro_move_avoid : Id.t option -> Id.Set.t -> Id.t Logic.move_location -> unit Proofview.tactic (** [intro_avoiding idl] acts as intro but prevents the new Id.t to belong to [idl] *) @@ -117,11 +117,11 @@ val use_clear_hyp_by_default : unit -> bool (** {6 Introduction tactics with eliminations. } *) val intro_patterns : evars_flag -> intro_patterns -> unit Proofview.tactic -val intro_patterns_to : evars_flag -> Id.t move_location -> intro_patterns -> +val intro_patterns_to : evars_flag -> Id.t Logic.move_location -> intro_patterns -> unit Proofview.tactic -val intro_patterns_bound_to : evars_flag -> int -> Id.t move_location -> intro_patterns -> +val intro_patterns_bound_to : evars_flag -> int -> Id.t Logic.move_location -> intro_patterns -> unit Proofview.tactic -val intro_pattern_to : evars_flag -> Id.t move_location -> delayed_open_constr intro_pattern_expr -> +val intro_pattern_to : evars_flag -> Id.t Logic.move_location -> delayed_open_constr intro_pattern_expr -> unit Proofview.tactic (** Implements user-level "intros", with [] standing for "**" *) @@ -188,7 +188,7 @@ val apply_clear_request : clear_flag -> bool -> constr -> unit Proofview.tactic val specialize : constr with_bindings -> intro_pattern option -> unit Proofview.tactic -val move_hyp : Id.t -> Id.t move_location -> unit Proofview.tactic +val move_hyp : Id.t -> Id.t Logic.move_location -> unit Proofview.tactic val rename_hyp : (Id.t * Id.t) list -> unit Proofview.tactic val revert : Id.t list -> unit Proofview.tactic diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 8b56275c7..ee578669c 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -24,7 +24,8 @@ open Globnames open Inductiveops open Tactics open Ind_tables -open Misctypes +open Namegen +open Tactypes open Proofview.Notations module RelDecl = Context.Rel.Declaration diff --git a/vernac/classes.ml b/vernac/classes.ml index 946a7bb32..8cf3895fb 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -145,7 +145,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) (fun avoid (clname, _) -> match clname with | Some cl -> - let t = CAst.make @@ CHole (None, Misctypes.IntroAnonymous, None) in + let t = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None) in t, avoid | None -> failwith ("new instance: under-applied typeclass")) cl @@ -255,7 +255,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) k.cl_projs; c :: props, rest' with Not_found -> - ((CAst.make @@ CHole (None(* Some Evar_kinds.GoalEvar *), Misctypes.IntroAnonymous, None)) :: props), rest + ((CAst.make @@ CHole (None(* Some Evar_kinds.GoalEvar *), Namegen.IntroAnonymous, None)) :: props), rest else props, rest) ([], props) k.cl_props in diff --git a/vernac/g_proofs.ml4 b/vernac/g_proofs.ml4 index a3806ff68..4b11276af 100644 --- a/vernac/g_proofs.ml4 +++ b/vernac/g_proofs.ml4 @@ -8,10 +8,10 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +open Glob_term open Constrexpr open Vernacexpr open Proof_global -open Misctypes open Pcoq open Pcoq.Prim diff --git a/vernac/g_vernac.ml4 b/vernac/g_vernac.ml4 index b6523981c..59449d07a 100644 --- a/vernac/g_vernac.ml4 +++ b/vernac/g_vernac.ml4 @@ -12,6 +12,7 @@ open Pp open CErrors open Util open Names +open Glob_term open Vernacexpr open Constrexpr open Constrexpr_ops @@ -20,6 +21,7 @@ open Decl_kinds open Declaremods open Declarations open Misctypes +open Namegen open Tok (* necessary for camlp5 *) open Pcoq @@ -338,7 +340,7 @@ GEXTEND Gram ; type_cstr: [ [ ":"; c=lconstr -> c - | -> CAst.make ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None) ] ] + | -> CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None) ] ] ; (* Inductive schemes *) scheme: @@ -394,7 +396,7 @@ GEXTEND Gram (None,DefExpr(id,mkCLambdaN ~loc:!@loc l b,None)) ] ] ; record_binder: - [ [ id = name -> (None,AssumExpr(id, CAst.make ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None))) + [ [ id = name -> (None,AssumExpr(id, CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None))) | id = name; f = record_binder_body -> f id ] ] ; assum_list: @@ -413,7 +415,7 @@ GEXTEND Gram t= [ coe = of_type_with_opt_coercion; c = lconstr -> fun l id -> (not (Option.is_empty coe),(id,mkCProdN ~loc:!@loc l c)) | -> - fun l id -> (false,(id,mkCProdN ~loc:!@loc l (CAst.make ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None)))) ] + fun l id -> (false,(id,mkCProdN ~loc:!@loc l (CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None)))) ] -> t l ]] ; diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 5490b9ce5..d0c423650 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -286,7 +286,7 @@ open Pputils prlist_strict (pr_module_vardecls pr_c) l let pr_type_option pr_c = function - | { v = CHole (k, Misctypes.IntroAnonymous, _) } -> mt() + | { v = CHole (k, Namegen.IntroAnonymous, _) } -> mt() | _ as c -> brk(0,2) ++ str" :" ++ pr_c c let pr_decl_notation prc ({loc; v=ntn},c,scopt) = diff --git a/vernac/record.ml b/vernac/record.ml index e6a3afe4e..940859723 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -96,7 +96,7 @@ let binder_of_decl = function | Vernacexpr.AssumExpr(n,t) -> (n,None,t) | Vernacexpr.DefExpr(n,c,t) -> (n,Some c, match t with Some c -> c - | None -> CAst.make ?loc:n.CAst.loc @@ CHole (None, Misctypes.IntroAnonymous, None)) + | None -> CAst.make ?loc:n.CAst.loc @@ CHole (None, Namegen.IntroAnonymous, None)) let binders_of_decls = List.map binder_of_decl -- cgit v1.2.3