aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrexpr.ml32
-rw-r--r--interp/constrexpr_ops.ml67
-rw-r--r--interp/constrexpr_ops.mli7
-rw-r--r--interp/constrextern.ml25
-rw-r--r--interp/constrextern.mli6
-rw-r--r--interp/constrintern.ml156
-rw-r--r--interp/constrintern.mli5
-rw-r--r--interp/declare.ml44
-rw-r--r--interp/declare.mli2
-rw-r--r--interp/discharge.ml7
-rw-r--r--interp/dumpglob.ml2
-rw-r--r--interp/dumpglob.mli4
-rw-r--r--interp/genintern.ml8
-rw-r--r--interp/genintern.mli8
-rw-r--r--interp/genredexpr.ml5
-rw-r--r--interp/implicit_quantifiers.ml17
-rw-r--r--interp/implicit_quantifiers.mli8
-rw-r--r--interp/modintern.ml10
-rw-r--r--interp/modintern.mli3
-rw-r--r--interp/notation_ops.ml22
-rw-r--r--interp/notation_term.ml3
-rw-r--r--interp/reserve.mli2
-rw-r--r--interp/smartlocate.ml19
-rw-r--r--interp/smartlocate.mli11
-rw-r--r--interp/stdarg.ml15
-rw-r--r--interp/stdarg.mli37
-rw-r--r--interp/tactypes.ml34
27 files changed, 267 insertions, 292 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index ca6ea94f09..521eeb8e96 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 } *)
@@ -23,6 +22,15 @@ type name_decl = lname * universe_decl_expr option
type notation = string
+type 'a or_by_notation_r =
+ | AN of 'a
+ | ByNotation of (string * string option)
+
+type 'a or_by_notation = 'a or_by_notation_r CAst.t
+
+(* NB: the last string in [ByNotation] is actually a [Notation.delimiters],
+ but this formulation avoids a useless dependency. *)
+
type explicitation =
| ExplByPos of int * Id.t option (* a reference to the n-th product starting from left *)
| ExplByName of Id.t
@@ -53,17 +61,17 @@ type instance_expr = Glob_term.glob_level list
type cases_pattern_expr_r =
| CPatAlias of cases_pattern_expr * lname
- | CPatCstr of reference
+ | CPatCstr of qualid
* cases_pattern_expr list option * cases_pattern_expr list
(** [CPatCstr (_, c, Some l1, l2)] represents [(@ c l1) l2] *)
- | CPatAtom of reference option
+ | CPatAtom of qualid option
| CPatOr of cases_pattern_expr list
| CPatNotation of notation * cases_pattern_notation_substitution
* cases_pattern_expr list (** CPatNotation (_, n, l1 ,l2) represents
(notation n applied with substitution l1)
applied to arguments l2 *)
| CPatPrim of prim_token
- | CPatRecord of (reference * cases_pattern_expr) list
+ | CPatRecord of (qualid * cases_pattern_expr) list
| CPatDelimiters of string * cases_pattern_expr
| CPatCast of cases_pattern_expr * constr_expr
and cases_pattern_expr = cases_pattern_expr_r CAst.t
@@ -73,16 +81,16 @@ and cases_pattern_notation_substitution =
cases_pattern_expr list list (** for recursive notations *)
and constr_expr_r =
- | CRef of reference * instance_expr option
+ | CRef of qualid * instance_expr option
| CFix of lident * fix_expr list
| CCoFix of lident * cofix_expr list
| CProdN of local_binder_expr list * constr_expr
| CLambdaN of local_binder_expr list * constr_expr
| CLetIn of lname * constr_expr * constr_expr option * constr_expr
- | CAppExpl of (proj_flag * reference * instance_expr option) * constr_expr list
+ | CAppExpl of (proj_flag * qualid * instance_expr option) * constr_expr list
| CApp of (proj_flag * constr_expr) *
(constr_expr * explicitation CAst.t option) list
- | CRecord of (reference * constr_expr) list
+ | CRecord of (qualid * constr_expr) list
(* representation of the "let" and "match" constructs *)
| CCases of Constr.case_style (* determines whether this value represents "let" or "match" construct *)
@@ -94,16 +102,16 @@ 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
- | CPatVar of patvar
+ | 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
| CDelimiters of string * constr_expr
- | CProj of reference * constr_expr
+ | CProj of qualid * constr_expr
and constr_expr = constr_expr_r CAst.t
and case_expr = constr_expr (* expression that is being matched *)
@@ -142,7 +150,7 @@ type constr_pattern_expr = constr_expr
(** Concrete syntax for modules and module types *)
type with_declaration_ast =
- | CWith_Module of Id.t list CAst.t * qualid CAst.t
+ | CWith_Module of Id.t list CAst.t * qualid
| CWith_Definition of Id.t list CAst.t * universe_decl_expr option * constr_expr
type module_ast_r =
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 1be1dd96cb..4b1af9147c 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -10,12 +10,12 @@
open Pp
open Util
-open CAst
open Names
open Nameops
open Libnames
+open Namegen
+open Glob_term
open Constrexpr
-open Misctypes
open Decl_kinds
(***********************)
@@ -72,11 +72,11 @@ let rec cases_pattern_expr_eq p1 p2 =
| CPatAlias(a1,i1), CPatAlias(a2,i2) ->
eq_ast Name.equal i1 i2 && cases_pattern_expr_eq a1 a2
| CPatCstr(c1,a1,b1), CPatCstr(c2,a2,b2) ->
- eq_reference c1 c2 &&
+ qualid_eq c1 c2 &&
Option.equal (List.equal cases_pattern_expr_eq) a1 a2 &&
List.equal cases_pattern_expr_eq b1 b2
| CPatAtom(r1), CPatAtom(r2) ->
- Option.equal eq_reference r1 r2
+ Option.equal qualid_eq r1 r2
| CPatOr a1, CPatOr a2 ->
List.equal cases_pattern_expr_eq a1 a2
| CPatNotation (n1, s1, l1), CPatNotation (n2, s2, l2) ->
@@ -87,7 +87,7 @@ let rec cases_pattern_expr_eq p1 p2 =
prim_token_eq i1 i2
| CPatRecord l1, CPatRecord l2 ->
let equal (r1, e1) (r2, e2) =
- eq_reference r1 r2 && cases_pattern_expr_eq e1 e2
+ qualid_eq r1 r2 && cases_pattern_expr_eq e1 e2
in
List.equal equal l1 l2
| CPatDelimiters(s1,e1), CPatDelimiters(s2,e2) ->
@@ -107,7 +107,7 @@ let eq_universes u1 u2 =
let rec constr_expr_eq e1 e2 =
if CAst.(e1.v == e2.v) then true
else match CAst.(e1.v, e2.v) with
- | CRef (r1,u1), CRef (r2,u2) -> eq_reference r1 r2 && eq_universes u1 u2
+ | CRef (r1,u1), CRef (r2,u2) -> qualid_eq r1 r2 && eq_universes u1 u2
| CFix(id1,fl1), CFix(id2,fl2) ->
eq_ast Id.equal id1 id2 &&
List.equal fix_expr_eq fl1 fl2
@@ -127,7 +127,7 @@ let rec constr_expr_eq e1 e2 =
constr_expr_eq b1 b2
| CAppExpl((proj1,r1,_),al1), CAppExpl((proj2,r2,_),al2) ->
Option.equal Int.equal proj1 proj2 &&
- eq_reference r1 r2 &&
+ qualid_eq r1 r2 &&
List.equal constr_expr_eq al1 al2
| CApp((proj1,e1),al1), CApp((proj2,e2),al2) ->
Option.equal Int.equal proj1 proj2 &&
@@ -135,7 +135,7 @@ let rec constr_expr_eq e1 e2 =
List.equal args_eq al1 al2
| CRecord l1, CRecord l2 ->
let field_eq (r1, e1) (r2, e2) =
- eq_reference r1 r2 && constr_expr_eq e1 e2
+ qualid_eq r1 r2 && constr_expr_eq e1 e2
in
List.equal field_eq l1 l2
| CCases(_,r1,a1,brl1), CCases(_,r2,a2,brl2) ->
@@ -161,7 +161,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) ->
@@ -177,7 +177,7 @@ let rec constr_expr_eq e1 e2 =
String.equal s1 s2 &&
constr_expr_eq e1 e2
| CProj(p1,c1), CProj(p2,c2) ->
- eq_reference p1 p2 && constr_expr_eq c1 c2
+ qualid_eq p1 p2 && constr_expr_eq c1 c2
| (CRef _ | CFix _ | CCoFix _ | CProdN _ | CLambdaN _ | CLetIn _ | CAppExpl _
| CApp _ | CRecord _ | CCases _ | CLetTuple _ | CIf _ | CHole _
| CPatVar _ | CEvar _ | CSort _ | CCast _ | CNotation _ | CPrim _
@@ -279,7 +279,9 @@ let rec cases_pattern_fold_names f a pt = match CAst.(pt.v) with
List.fold_left (cases_pattern_fold_names f)
(List.fold_left (cases_pattern_fold_names f) a (patl@List.flatten patll)) patl'
| CPatDelimiters (_,pat) -> cases_pattern_fold_names f a pat
- | CPatAtom (Some {v=Ident id}) when not (is_constructor id) -> f id a
+ | CPatAtom (Some qid)
+ when qualid_is_ident qid && not (is_constructor @@ qualid_basename qid) ->
+ f (qualid_basename qid) a
| CPatPrim _ | CPatAtom _ -> a
| CPatCast ({CAst.loc},_) ->
CErrors.user_err ?loc ~hdr:"cases_pattern_fold_names"
@@ -362,7 +364,9 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function
let free_vars_of_constr_expr c =
let rec aux bdvars l = function
- | { CAst.v = CRef ({v=Ident id},_) } -> if Id.List.mem id bdvars then l else Id.Set.add id l
+ | { CAst.v = CRef (qid, _) } when qualid_is_ident qid ->
+ let id = qualid_basename qid in
+ if Id.List.mem id bdvars then l else Id.Set.add id l
| c -> fold_constr_expr_with_binders (fun a l -> a::l) aux bdvars l c
in aux [] Id.Set.empty c
@@ -395,7 +399,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,
@@ -439,11 +443,13 @@ let map_constr_expr_with_binders g f e = CAst.map (function
)
(* Used in constrintern *)
-let rec replace_vars_constr_expr l = function
- | { CAst.loc; v = CRef ({v=Ident id},us) } as x ->
- (try CAst.make ?loc @@ CRef (make ?loc @@ Ident (Id.Map.find id l),us) with Not_found -> x)
- | c -> map_constr_expr_with_binders Id.Map.remove
- replace_vars_constr_expr l c
+let rec replace_vars_constr_expr l r =
+ match r with
+ | { CAst.loc; v = CRef (qid,us) } as x when qualid_is_ident qid ->
+ let id = qualid_basename qid in
+ (try CAst.make ?loc @@ CRef (qualid_of_ident ?loc (Id.Map.find id l),us)
+ with Not_found -> x)
+ | cn -> map_constr_expr_with_binders Id.Map.remove replace_vars_constr_expr l cn
(* Returns the ranges of locs of the notation that are not occupied by args *)
(* and which are then occupied by proper symbols of the notation (or spaces) *)
@@ -512,7 +518,7 @@ let split_at_annot bl na =
(** Pseudo-constructors *)
-let mkIdentC id = CAst.make @@ CRef (make @@ Ident id,None)
+let mkIdentC id = CAst.make @@ CRef (qualid_of_ident id,None)
let mkRefC r = CAst.make @@ CRef (r,None)
let mkCastC (a,k) = CAst.make @@ CCast (a,k)
let mkLambdaC (idl,bk,a,b) = CAst.make @@ CLambdaN ([CLocalAssum (idl,bk,a)],b)
@@ -531,21 +537,23 @@ let mkCProdN ?loc bll c =
let mkCLambdaN ?loc bll c =
CAst.make ?loc @@ CLambdaN (bll,c)
-let coerce_reference_to_id = CAst.with_loc_val (fun ?loc -> function
- | Ident id -> id
- | Qualid _ ->
- CErrors.user_err ?loc ~hdr:"coerce_reference_to_id"
- (str "This expression should be a simple identifier."))
+let coerce_reference_to_id qid =
+ if qualid_is_ident qid then qualid_basename qid
+ else
+ CErrors.user_err ?loc:qid.CAst.loc ~hdr:"coerce_reference_to_id"
+ (str "This expression should be a simple identifier.")
let coerce_to_id = function
- | { CAst.loc; v = CRef ({v=Ident id},None) } -> CAst.make ?loc id
+ | { CAst.loc; v = CRef (qid,None) } when qualid_is_ident qid ->
+ CAst.make ?loc @@ qualid_basename qid
| { CAst.loc; _ } -> CErrors.user_err ?loc
~hdr:"coerce_to_id"
(str "This expression should be a simple identifier.")
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 = CRef (qid,None) } when qualid_is_ident qid ->
+ CAst.make ?loc @@ Name (qualid_basename qid)
+ | { 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,9 +577,10 @@ 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' ->
+ | CLetIn ({CAst.loc;v=Name id},b,None,{ CAst.v = CRef (qid,None) })
+ when qualid_is_ident qid && Id.equal id (qualid_basename qid) ->
CPatAlias (coerce_to_cases_pattern_expr b, CAst.(make ?loc @@ Name id))
| CApp ((None,p),args) when List.for_all (fun (_,e) -> e=None) args ->
(mkAppPattern (coerce_to_cases_pattern_expr p) (List.map (fun (a,_) -> coerce_to_cases_pattern_expr a) args)).CAst.v
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index b4f0886acf..46aef1c788 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] *)
@@ -42,9 +41,9 @@ val local_binders_loc : local_binder_expr list -> Loc.t option
(** {6 Constructors}*)
val mkIdentC : Id.t -> constr_expr
-val mkRefC : reference -> constr_expr
+val mkRefC : qualid -> 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
@@ -62,7 +61,7 @@ val mkAppPattern : ?loc:Loc.t -> cases_pattern_expr -> cases_pattern_expr list -
(** {6 Destructors}*)
-val coerce_reference_to_id : reference -> Id.t
+val coerce_reference_to_id : qualid -> Id.t
(** FIXME: nothing to do here *)
val coerce_to_id : constr_expr -> lident
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 86f6ce9ae8..2538c77722 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
@@ -269,7 +270,7 @@ let extern_evar n l = CEvar (n,l)
may be inaccurate *)
let default_extern_reference ?loc vars r =
- make @@ Qualid (shortest_qualid_of_global vars r)
+ shortest_qualid_of_global ?loc vars r
let my_extern_reference = ref default_extern_reference
@@ -387,7 +388,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
(uninterp_cases_pattern_notations pat)
with No_match ->
lift (fun ?loc -> function
- | PatVar (Name id) -> CPatAtom (Some (make ?loc @@ Ident id))
+ | PatVar (Name id) -> CPatAtom (Some (qualid_of_ident ?loc id))
| PatVar (Anonymous) -> CPatAtom None
| PatCstr(cstrsp,args,na) ->
let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
@@ -456,7 +457,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
(make_pat_notation ?loc ntn (l,ll) l2') key
end
| SynDefRule kn ->
- let qid = make ?loc @@ Qualid (shortest_qualid_of_syndef vars kn) in
+ let qid = shortest_qualid_of_syndef ?loc vars kn in
let l1 =
List.rev_map (fun (c,(scopt,scl)) ->
extern_cases_pattern_in_scope (scopt,scl@scopes) vars c)
@@ -483,7 +484,7 @@ and extern_notation_pattern (tmp_scope,scopes as allscopes) vars t = function
(match_notation_constr_cases_pattern t pat) allscopes vars keyrule in
insert_pat_alias ?loc p na
| PatVar Anonymous -> CAst.make ?loc @@ CPatAtom None
- | PatVar (Name id) -> CAst.make ?loc @@ CPatAtom (Some (make ?loc @@ Ident id))
+ | PatVar (Name id) -> CAst.make ?loc @@ CPatAtom (Some (qualid_of_ident ?loc id))
with
No_match -> extern_notation_pattern allscopes vars t rules
@@ -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)
@@ -752,15 +753,15 @@ let rec extern inctx scopes vars r =
extern_global (select_stronger_impargs (implicits_of_global ref))
(extern_reference vars ref) (extern_universes us)
- | GVar id -> CRef (make ?loc @@ Ident id,None)
+ | GVar id -> CRef (qualid_of_ident ?loc 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)
@@ -1094,7 +1095,7 @@ and extern_notation (tmp_scope,scopes as allscopes) vars t = function
List.map (fun (c,(scopt,scl)) ->
extern true (scopt,scl@scopes) vars c, None)
terms in
- let a = CRef (make ?loc @@ Qualid (shortest_qualid_of_syndef vars kn),None) in
+ let a = CRef (shortest_qualid_of_syndef ?loc vars kn,None) in
CAst.make ?loc @@ if List.is_empty l then a else CApp ((None, CAst.make a),l) in
if List.is_empty args then e
else
@@ -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/constrextern.mli b/interp/constrextern.mli
index 73c108319f..f09b316cd6 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -38,7 +38,7 @@ val extern_closed_glob : ?lax:bool -> bool -> env -> Evd.evar_map -> closed_glob
val extern_constr : ?lax:bool -> bool -> env -> Evd.evar_map -> constr -> constr_expr
val extern_constr_in_scope : bool -> scope_name -> env -> Evd.evar_map -> constr -> constr_expr
-val extern_reference : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> reference
+val extern_reference : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid
val extern_type : bool -> env -> Evd.evar_map -> types -> constr_expr
val extern_sort : Evd.evar_map -> Sorts.t -> glob_sort
val extern_rel_context : constr option -> env -> Evd.evar_map ->
@@ -56,9 +56,9 @@ val print_projections : bool ref
(** Customization of the global_reference printer *)
val set_extern_reference :
- (?loc:Loc.t -> Id.Set.t -> GlobRef.t -> reference) -> unit
+ (?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid) -> unit
val get_extern_reference :
- unit -> (?loc:Loc.t -> Id.Set.t -> GlobRef.t -> reference)
+ unit -> (?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid)
(** WARNING: The following functions are evil due to
side-effects. Think of the following case as used in the printer:
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 848180743f..4e217b2cdd 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
@@ -96,8 +96,8 @@ let is_global id =
with Not_found ->
false
-let global_reference_of_reference ref =
- locate_reference (qualid_of_reference ref).CAst.v
+let global_reference_of_reference qid =
+ locate_reference qid
let global_reference id =
locate_reference (qualid_of_ident id)
@@ -117,7 +117,7 @@ let global_reference_in_absolute_module dir id =
type internalization_error =
| VariableCapture of Id.t * Id.t
| IllegalMetavariable
- | NotAConstructor of reference
+ | NotAConstructor of qualid
| UnboundFixName of bool * Id.t
| NonLinearPattern of Id.t
| BadPatternsNumber of int * int
@@ -131,8 +131,8 @@ let explain_variable_capture id id' =
let explain_illegal_metavariable =
str "Metavariables allowed only in patterns"
-let explain_not_a_constructor ref =
- str "Unknown constructor: " ++ pr_reference ref
+let explain_not_a_constructor qid =
+ str "Unknown constructor: " ++ pr_qualid qid
let explain_unbound_fix_name is_cofix id =
str "The name" ++ spc () ++ Id.print id ++
@@ -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
@@ -404,7 +404,8 @@ let intern_generalized_binder ?(global_level=false) intern_type ntnvars
let name =
let id =
match ty with
- | { v = CApp ((_, { v = CRef ({v=Ident id},_) } ), _) } -> id
+ | { v = CApp ((_, { v = CRef (qid,_) } ), _) } when qualid_is_ident qid ->
+ qualid_basename qid
| _ -> default_non_dependent_ident
in Implicit_quantifiers.make_fresh ids' (Global.env ()) id
in Name name
@@ -431,7 +432,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 +473,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 +503,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
@@ -556,7 +557,8 @@ let is_var store pat =
let out_var pat =
match pat.v with
- | CPatAtom (Some ({v=Ident id})) -> Name id
+ | CPatAtom (Some qid) when qualid_is_ident qid ->
+ Name (qualid_basename qid)
| CPatAtom None -> Anonymous
| _ -> assert false
@@ -564,7 +566,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
@@ -606,7 +608,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam
(renaming',env), None, Name id'
type binder_action =
-| AddLetIn of Misctypes.lname * constr_expr * constr_expr option
+| AddLetIn of lname * constr_expr * constr_expr option
| AddTermIter of (constr_expr * subscopes) Names.Id.Map.t
| AddPreBinderIter of Id.t * local_binder_expr (* A binder to be internalized *)
| AddBinderIter of Id.t * extended_glob_local_binder (* A binder already internalized - used for generalized binders *)
@@ -622,18 +624,18 @@ let error_cannot_coerce_disjunctive_pattern_term ?loc () =
let terms_of_binders bl =
let rec term_of_pat pt = dmap_with_loc (fun ?loc -> function
- | PatVar (Name id) -> CRef (make @@ Ident id, None)
+ | PatVar (Name id) -> CRef (qualid_of_ident id, None)
| 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 qid = qualid_of_path ?loc (path_of_global (ConstructRef c)) 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
+ CAppExpl ((None,qid,None),params @ List.map term_of_pat l)) pt in
let rec extract_variables l = match l with
| bnd :: l ->
let loc = bnd.loc in
begin match DAst.get bnd with
- | GLocalAssum (Name id,_,_) -> (CAst.make ?loc @@ CRef (make ?loc @@ Ident id, None)) :: extract_variables l
+ | GLocalAssum (Name id,_,_) -> (CAst.make ?loc @@ CRef (qualid_of_ident ?loc id, None)) :: extract_variables l
| GLocalDef (Name id,_,_,_) -> extract_variables l
| GLocalDef (Anonymous,_,_,_)
| GLocalAssum (Anonymous,_,_) -> user_err Pp.(str "Cannot turn \"_\" into a term.")
@@ -806,7 +808,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
distinction *)
let cases_pattern_of_name {loc;v=na} =
- let atom = match na with Name id -> Some (make ?loc @@ Ident id) | Anonymous -> None in
+ let atom = match na with Name id -> Some (qualid_of_ident ?loc id) | Anonymous -> None in
CAst.make ?loc (CPatAtom atom)
let split_by_type ids subst =
@@ -903,7 +905,7 @@ let intern_var env (ltacvars,ntnvars) namedctx loc id us =
try
let ty,expl_impls,impls,argsc = Id.Map.find id env.impls in
let expl_impls = List.map
- (fun id -> CAst.make ?loc @@ CRef (make ?loc @@ Ident id,None), Some (make ?loc @@ ExplByName id)) expl_impls in
+ (fun id -> CAst.make ?loc @@ CRef (qualid_of_ident ?loc id,None), Some (make ?loc @@ ExplByName id)) expl_impls in
let tys = string_of_ty ty in
Dumpglob.dump_reference ?loc "<>" (Id.to_string id) tys;
gvar (loc,id) us, make_implicits_list impls, argsc, expl_impls
@@ -970,18 +972,17 @@ let dump_extended_global loc = function
| TrueGlobal ref -> (*feedback_global loc ref;*) Dumpglob.add_glob ?loc ref
| SynDef sp -> Dumpglob.add_glob_kn ?loc sp
-let intern_extended_global_of_qualid {loc;v=qid} =
- let r = Nametab.locate_extended qid in dump_extended_global loc r; r
+let intern_extended_global_of_qualid qid =
+ let r = Nametab.locate_extended qid in dump_extended_global qid.CAst.loc r; r
-let intern_reference ref =
- let qid = qualid_of_reference ref in
+let intern_reference qid =
let r =
try intern_extended_global_of_qualid qid
with Not_found -> error_global_not_found qid
in
Smartlocate.global_of_extended_global r
-let sort_info_of_level_info (info: level_info) : (Libnames.reference * int) option =
+let sort_info_of_level_info (info: level_info) : (Libnames.qualid * int) option =
match info with
| UAnonymous -> None
| UUnknown -> None
@@ -994,9 +995,12 @@ let glob_sort_of_level (level: glob_level) : glob_sort =
| GType info -> GType [sort_info_of_level_info info]
(* Is it a global reference or a syntactic definition? *)
-let intern_qualid qid intern env ntnvars us args =
+let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args =
let loc = qid.loc in
match intern_extended_global_of_qualid qid with
+ | TrueGlobal (VarRef _) when no_secvar ->
+ (* Rule out section vars since these should have been found by intern_var *)
+ raise Not_found
| TrueGlobal ref -> (DAst.make ?loc @@ GRef (ref, us)), true, args
| SynDef sp ->
let (ids,c) = Syntax_def.search_syntactic_definition ?loc sp in
@@ -1011,7 +1015,7 @@ let intern_qualid qid intern env ntnvars us args =
let c = instantiate_notation_constr loc intern intern_cases_pattern_as_binder ntnvars subst infos c in
let loc = c.loc in
let err () =
- user_err ?loc (str "Notation " ++ pr_qualid qid.v
+ user_err ?loc (str "Notation " ++ pr_qualid qid
++ str " cannot have a universe instance,"
++ str " its expanded head does not start with a reference")
in
@@ -1028,41 +1032,32 @@ let intern_qualid qid intern env ntnvars us args =
| Some [s], GSort (GType []) -> DAst.make ?loc @@ GSort (glob_sort_of_level s)
| Some [_old_level], GSort _new_sort ->
(* TODO: add old_level and new_sort to the error message *)
- user_err ?loc (str "Cannot change universe level of notation " ++ pr_qualid qid.v)
+ user_err ?loc (str "Cannot change universe level of notation " ++ pr_qualid qid)
| Some _, _ -> err ()
in
c, projapp, args2
-(* Rule out section vars since these should have been found by intern_var *)
-let intern_non_secvar_qualid qid intern env ntnvars us args =
- let c, _, _ as r = intern_qualid qid intern env ntnvars us args in
- match DAst.get c with
- | GRef (VarRef _, _) -> raise Not_found
- | _ -> r
-
-let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args =
-function
- | {loc; v=Qualid qid} ->
- let qid = make ?loc qid in
- let r,projapp,args2 =
- try intern_qualid qid intern env ntnvars us args
- with Not_found -> error_global_not_found qid
- in
- let x, imp, scopes, l = find_appl_head_data r in
- (x,imp,scopes,l), args2
- | {loc; v=Ident id} ->
- try intern_var env lvar namedctx loc id us, args
+let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args qid =
+ let loc = qid.CAst.loc in
+ if qualid_is_ident qid then
+ try intern_var env lvar namedctx loc (qualid_basename qid) us, args
with Not_found ->
- let qid = make ?loc @@ qualid_of_ident id in
try
- let r, projapp, args2 = intern_non_secvar_qualid qid intern env ntnvars us args in
+ let r, projapp, args2 = intern_qualid ~no_secvar:true qid intern env ntnvars us args in
let x, imp, scopes, l = find_appl_head_data r in
(x,imp,scopes,l), args2
with Not_found ->
- (* Extra allowance for non globalizing functions *)
- if !interning_grammar || env.unb then
- (gvar (loc,id) us, [], [], []), args
+ (* Extra allowance for non globalizing functions *)
+ if !interning_grammar || env.unb then
+ (gvar (loc,qualid_basename qid) us, [], [], []), args
else error_global_not_found qid
+ else
+ let r,projapp,args2 =
+ try intern_qualid qid intern env ntnvars us args
+ with Not_found -> error_global_not_found qid
+ in
+ let x, imp, scopes, l = find_appl_head_data r in
+ (x,imp,scopes,l), args2
let interp_reference vars r =
let (r,_,_,_),_ =
@@ -1077,11 +1072,11 @@ let interp_reference vars r =
(** Private internalization patterns *)
type 'a raw_cases_pattern_expr_r =
- | RCPatAlias of 'a raw_cases_pattern_expr * Misctypes.lname
+ | RCPatAlias of 'a raw_cases_pattern_expr * lname
| RCPatCstr of GlobRef.t
* 'a raw_cases_pattern_expr list * 'a raw_cases_pattern_expr list
(** [RCPatCstr (loc, c, l1, l2)] represents [((@ c l1) l2)] *)
- | RCPatAtom of (Misctypes.lident * (Notation_term.tmp_scope_name option * Notation_term.scope_name list)) option
+ | RCPatAtom of (lident * (Notation_term.tmp_scope_name option * Notation_term.scope_name list)) option
| RCPatOr of 'a raw_cases_pattern_expr list
and 'a raw_cases_pattern_expr = ('a raw_cases_pattern_expr_r, 'a) DAst.t
@@ -1266,18 +1261,18 @@ let find_constructor loc add_params ref =
List.make nb ([], [(Id.Map.empty, DAst.make @@ PatVar Anonymous)])
| None -> []
-let find_pattern_variable = function
- | {v=Ident id} -> id
- | {loc;v=Qualid _} as x -> raise (InternalizationError(loc,NotAConstructor x))
+let find_pattern_variable qid =
+ if qualid_is_ident qid then qualid_basename qid
+ else raise (InternalizationError(qid.CAst.loc,NotAConstructor qid))
let check_duplicate loc fields =
- let eq (ref1, _) (ref2, _) = eq_reference ref1 ref2 in
+ let eq (ref1, _) (ref2, _) = qualid_eq ref1 ref2 in
let dups = List.duplicates eq fields in
match dups with
| [] -> ()
| (r, _) :: _ ->
user_err ?loc (str "This record defines several times the field " ++
- pr_reference r ++ str ".")
+ pr_qualid r ++ str ".")
(** [sort_fields ~complete loc fields completer] expects a list
[fields] of field assignments [f = e1; g = e2; ...], where [f, g]
@@ -1302,14 +1297,14 @@ let sort_fields ~complete loc fields completer =
(gr, Recordops.find_projection gr)
with Not_found ->
user_err ?loc ~hdr:"intern"
- (pr_reference first_field_ref ++ str": Not a projection")
+ (pr_qualid first_field_ref ++ str": Not a projection")
in
(* the number of parameters *)
let nparams = record.Recordops.s_EXPECTEDPARAM in
(* the reference constructor of the record *)
let base_constructor =
let global_record_id = ConstructRef record.Recordops.s_CONST in
- try make ?loc @@ Qualid (shortest_qualid_of_global Id.Set.empty global_record_id)
+ try shortest_qualid_of_global ?loc Id.Set.empty global_record_id
with Not_found ->
anomaly (str "Environment corruption for records.") in
let () = check_duplicate loc fields in
@@ -1317,7 +1312,7 @@ let sort_fields ~complete loc fields completer =
first_field_index, (* index of the first field of the record *)
proj_list) (* list of projections *)
=
- (* elimitate the first field from the projections,
+ (* eliminate the first field from the projections,
but keep its index *)
let rec build_proj_list projs proj_kinds idx ~acc_first_idx acc =
match projs with
@@ -1360,7 +1355,7 @@ let sort_fields ~complete loc fields completer =
let field_glob_ref = try global_reference_of_reference field_ref
with Not_found ->
user_err ?loc ~hdr:"intern"
- (str "The field \"" ++ pr_reference field_ref ++ str "\" does not exist.") in
+ (str "The field \"" ++ pr_qualid field_ref ++ str "\" does not exist.") in
let remaining_projs, (field_index, _) =
let the_proj (idx, glob_id) = GlobRef.equal field_glob_ref (ConstRef glob_id) in
try CList.extract_first the_proj remaining_projs
@@ -1389,7 +1384,7 @@ let sort_fields ~complete loc fields completer =
(** {6 Manage multiple aliases} *)
type alias = {
- alias_ids : Misctypes.lident list;
+ alias_ids : lident list;
alias_map : Id.t Id.Map.t;
}
@@ -1487,10 +1482,9 @@ let drop_notations_pattern looked_for genv =
end
| _ -> CErrors.anomaly Pp.(str "Invalid return pattern from Notation.interp_prim_token_cases_pattern_expr."))) x
in
- let rec drop_syndef top scopes re pats =
- let qid = qualid_of_reference re in
+ let rec drop_syndef top scopes qid pats =
try
- match locate_extended qid.v with
+ match locate_extended qid with
| SynDef sp ->
let (vars,a) = Syntax_def.search_syntactic_definition sp in
(match a with
@@ -1546,10 +1540,10 @@ let drop_notations_pattern looked_for genv =
| Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr(a, b, c)
| None -> raise (InternalizationError (loc,NotAConstructor head))
end
- | CPatCstr (r, Some expl_pl, pl) ->
- let g = try locate (qualid_of_reference r).v
+ | CPatCstr (qid, Some expl_pl, pl) ->
+ let g = try locate qid
with Not_found ->
- raise (InternalizationError (loc,NotAConstructor r)) in
+ raise (InternalizationError (loc,NotAConstructor qid)) in
if expl_pl == [] then
(* Convention: (@r) deactivates all further implicit arguments and scopes *)
DAst.make ?loc @@ RCPatCstr (g, List.map (in_pat false scopes) pl, [])
@@ -1729,15 +1723,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 =
@@ -1923,13 +1917,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
@@ -1969,12 +1963,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
@@ -2005,7 +1999,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
@@ -2050,7 +2044,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/constrintern.mli b/interp/constrintern.mli
index 4dd719e1f3..dd0944cc48 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -11,7 +11,6 @@
open Names
open Evd
open Environ
-open Misctypes
open Libnames
open Glob_term
open Pattern
@@ -142,10 +141,10 @@ val intern_constr_pattern :
constr_pattern_expr -> patvar list * constr_pattern
(** Raise Not_found if syndef not bound to a name and error if unexisting ref *)
-val intern_reference : reference -> GlobRef.t
+val intern_reference : qualid -> GlobRef.t
(** Expands abbreviations (syndef); raise an error if not existing *)
-val interp_reference : ltac_sign -> reference -> glob_constr
+val interp_reference : ltac_sign -> qualid -> glob_constr
(** Interpret binders *)
diff --git a/interp/declare.ml b/interp/declare.ml
index bc2d2068a2..e79cc60798 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -382,19 +382,39 @@ let inInductive : inductive_obj -> obj =
discharge_function = discharge_inductive;
rebuild_function = infer_inductive_subtyping }
-let declare_projections mind =
- let spec,_ = Inductive.lookup_mind_specif (Global.env ()) (mind,0) in
+let declare_projections univs mind =
+ (** FIXME: handle mutual records *)
+ let mind = (mind, 0) in
+ let env = Global.env () in
+ let spec,_ = Inductive.lookup_mind_specif env mind in
match spec.mind_record with
- | Some (Some (_, kns, pjs)) ->
- Array.iteri (fun i kn ->
+ | PrimRecord info ->
+ let _, kns, _ = info.(0) in
+ let projs = Inductiveops.compute_projections env mind in
+ Array.iter2 (fun kn (term, types) ->
let id = Label.to_id (Constant.label kn) in
- let entry = {proj_entry_ind = mind; proj_entry_arg = i} in
- let kn' = declare_constant id (ProjectionEntry entry,
- IsDefinition StructureComponent)
- in
- assert(Constant.equal kn kn')) kns; true,true
- | Some None -> true,false
- | None -> false,false
+ let univs = match univs with
+ | Monomorphic_ind_entry _ ->
+ (** Global constraints already defined through the inductive *)
+ Monomorphic_const_entry Univ.ContextSet.empty
+ | Polymorphic_ind_entry ctx ->
+ Polymorphic_const_entry ctx
+ | Cumulative_ind_entry ctx ->
+ Polymorphic_const_entry (Univ.CumulativityInfo.univ_context ctx)
+ in
+ let term, types = match univs with
+ | Monomorphic_const_entry _ -> term, types
+ | Polymorphic_const_entry ctx ->
+ let u = Univ.UContext.instance ctx in
+ Vars.subst_instance_constr u term, Vars.subst_instance_constr u types
+ in
+ let entry = definition_entry ~types ~univs term in
+ let kn' = declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent) in
+ assert (Constant.equal kn kn')
+ ) kns projs;
+ true, true
+ | FakeRecord -> true,false
+ | NotRecord -> false,false
(* for initial declaration *)
let declare_mind mie =
@@ -403,7 +423,7 @@ let declare_mind mie =
| [] -> anomaly (Pp.str "cannot declare an empty list of inductives.") in
let (sp,kn as oname) = add_leaf id (inInductive ([],mie)) in
let mind = Global.mind_of_delta_kn kn in
- let isrecord,isprim = declare_projections mind in
+ let isrecord,isprim = declare_projections mie.mind_entry_universes mind in
declare_mib_implicits mind;
declare_inductive_argument_scopes mind mie;
oname, isprim
diff --git a/interp/declare.mli b/interp/declare.mli
index 4a9f542783..02e73cd66c 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -87,6 +87,6 @@ val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit
val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit
-val do_universe : polymorphic -> Misctypes.lident list -> unit
+val do_universe : polymorphic -> lident list -> unit
val do_constraint : polymorphic -> (Glob_term.glob_level * Univ.constraint_type * Glob_term.glob_level) list ->
unit
diff --git a/interp/discharge.ml b/interp/discharge.ml
index e16a955d96..0e44a8b467 100644
--- a/interp/discharge.ml
+++ b/interp/discharge.ml
@@ -111,9 +111,10 @@ let process_inductive info modlist mib =
let section_decls' = Context.Named.map discharge section_decls in
let (params',inds') = abstract_inductive section_decls' nparamdecls inds in
let record = match mib.mind_record with
- | Some (Some (id, _, _)) -> Some (Some id)
- | Some None -> Some None
- | None -> None
+ | PrimRecord info ->
+ Some (Some (Array.map pi1 info))
+ | FakeRecord -> Some None
+ | NotRecord -> None
in
{ mind_entry_record = record;
mind_entry_finite = mib.mind_finite;
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 74618a2905..5bf46282fd 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -113,7 +113,7 @@ let type_of_global_ref gr =
"var" ^ type_of_logical_kind (Decls.variable_kind v)
| Globnames.IndRef ind ->
let (mib,oib) = Inductive.lookup_mind_specif (Global.env ()) ind in
- if mib.Declarations.mind_record <> None then
+ if mib.Declarations.mind_record <> Declarations.NotRecord then
begin match mib.Declarations.mind_finite with
| Finite -> "indrec"
| BiFinite -> "rec"
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index bf83d2df40..931d05a975 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -27,7 +27,7 @@ val continue : unit -> unit
val add_glob : ?loc:Loc.t -> Names.GlobRef.t -> unit
val add_glob_kn : ?loc:Loc.t -> Names.KerName.t -> unit
-val dump_definition : Misctypes.lident -> bool -> string -> unit
+val dump_definition : Names.lident -> bool -> string -> unit
val dump_moddef : ?loc:Loc.t -> Names.ModPath.t -> string -> unit
val dump_modref : ?loc:Loc.t -> Names.ModPath.t -> string -> unit
val dump_reference : ?loc:Loc.t -> string -> string -> string -> unit
@@ -39,7 +39,7 @@ val dump_notation :
(Constrexpr.notation * Notation.notation_location) Loc.located ->
Notation_term.scope_name option -> bool -> unit
-val dump_constraint : Misctypes.lname -> bool -> string -> unit
+val dump_constraint : Names.lname -> bool -> string -> unit
val dump_string : string -> unit
diff --git a/interp/genintern.ml b/interp/genintern.ml
index 161201c448..d9a0db040a 100644
--- a/interp/genintern.ml
+++ b/interp/genintern.ml
@@ -26,9 +26,15 @@ let empty_glob_sign env = {
extra = Store.empty;
}
+(** In globalize tactics, we need to keep the initial [constr_expr] to recompute
+ in the environment by the effective calls to Intro, Inversion, etc
+ The [constr_expr] field is [None] in TacDef though *)
+type glob_constr_and_expr = Glob_term.glob_constr * Constrexpr.constr_expr option
+type glob_constr_pattern_and_expr = Id.Set.t * glob_constr_and_expr * Pattern.constr_pattern
+
type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb
type 'glb subst_fun = substitution -> 'glb -> 'glb
-type 'glb ntn_subst_fun = Tactypes.glob_constr_and_expr Id.Map.t -> 'glb -> 'glb
+type 'glb ntn_subst_fun = glob_constr_and_expr Id.Map.t -> 'glb -> 'glb
module InternObj =
struct
diff --git a/interp/genintern.mli b/interp/genintern.mli
index d818713fcf..f4f064bcac 100644
--- a/interp/genintern.mli
+++ b/interp/genintern.mli
@@ -22,6 +22,12 @@ type glob_sign = {
val empty_glob_sign : Environ.env -> glob_sign
+(** In globalize tactics, we need to keep the initial [constr_expr] to recompute
+ in the environment by the effective calls to Intro, Inversion, etc
+ The [constr_expr] field is [None] in TacDef though *)
+type glob_constr_and_expr = Glob_term.glob_constr * Constrexpr.constr_expr option
+type glob_constr_pattern_and_expr = Id.Set.t * glob_constr_and_expr * Pattern.constr_pattern
+
(** {5 Internalization functions} *)
type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb
@@ -42,7 +48,7 @@ val generic_substitute : glob_generic_argument subst_fun
(** {5 Notation functions} *)
-type 'glb ntn_subst_fun = Tactypes.glob_constr_and_expr Id.Map.t -> 'glb -> 'glb
+type 'glb ntn_subst_fun = glob_constr_and_expr Id.Map.t -> 'glb -> 'glb
val substitute_notation : ('raw, 'glb, 'top) genarg_type -> 'glb ntn_subst_fun
diff --git a/interp/genredexpr.ml b/interp/genredexpr.ml
index 80697461a6..607f2258fd 100644
--- a/interp/genredexpr.ml
+++ b/interp/genredexpr.ml
@@ -52,15 +52,14 @@ type ('a,'b,'c) red_expr_gen =
type ('a,'b,'c) may_eval =
| ConstrTerm of 'a
| ConstrEval of ('a,'b,'c) red_expr_gen * 'a
- | ConstrContext of Misctypes.lident * 'a
+ | ConstrContext of Names.lident * 'a
| ConstrTypeOf of 'a
open Libnames
open Constrexpr
-open Misctypes
type r_trm = constr_expr
type r_pat = constr_pattern_expr
-type r_cst = reference or_by_notation
+type r_cst = qualid or_by_notation
type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index b48db9ac54..83ad9af338 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -53,7 +53,7 @@ let cache_generalizable_type (_,(local,cmd)) =
let load_generalizable_type _ (_,(local,cmd)) =
generalizable_table := add_generalizable cmd !generalizable_table
-let in_generalizable : bool * Misctypes.lident list option -> obj =
+let in_generalizable : bool * lident list option -> obj =
declare_object {(default_object "GENERALIZED-IDENT") with
load_function = load_generalizable_type;
cache_function = cache_generalizable_type;
@@ -96,9 +96,11 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l =
else l
in
let rec aux bdvars l c = match CAst.(c.v) with
- | CRef ({CAst.v=Ident id},_) -> found c.CAst.loc id bdvars l
- | CNotation ("{ _ : _ | _ }", ({ CAst.v = CRef ({CAst.v=Ident id},_) } :: _, [], [], [])) when not (Id.Set.mem id bdvars) ->
- Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add id bdvars) l c
+ | CRef (qid,_) when qualid_is_ident qid ->
+ found c.CAst.loc (qualid_basename qid) bdvars l
+ | CNotation ("{ _ : _ | _ }", ({ CAst.v = CRef (qid,_) } :: _, [], [], [])) when
+ qualid_is_ident qid && not (Id.Set.mem (qualid_basename qid) bdvars) ->
+ Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add (qualid_basename qid) bdvars) l c
| _ -> Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c
in aux bound l c
@@ -196,7 +198,7 @@ let combine_params avoid fn applied needed =
let combine_params_freevar =
fun avoid (_, decl) ->
let id' = next_name_away_from (RelDecl.get_name decl) avoid in
- (CAst.make @@ CRef (CAst.make @@ Ident id',None), Id.Set.add id' avoid)
+ (CAst.make @@ CRef (qualid_of_ident id',None), Id.Set.add id' avoid)
let destClassApp cl =
let open CAst in
@@ -218,9 +220,8 @@ let destClassAppExpl cl =
let implicit_application env ?(allow_partial=true) f ty =
let is_class =
try
- let ({CAst.v=(r, _, _)} as clapp) = destClassAppExpl ty in
- let qid = qualid_of_reference r in
- let gr = Nametab.locate qid.CAst.v in
+ let ({CAst.v=(qid, _, _)} as clapp) = destClassAppExpl ty in
+ let gr = Nametab.locate qid in
if Typeclasses.is_class gr then Some (clapp, gr) else None
with Not_found -> None
in
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index e64c5c5427..a8492095ec 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -13,11 +13,11 @@ open Glob_term
open Constrexpr
open Libnames
-val declare_generalizable : local:bool -> Misctypes.lident list option -> unit
+val declare_generalizable : local:bool -> lident list option -> unit
val ids_of_list : Id.t list -> Id.Set.t
-val destClassApp : constr_expr -> (reference * constr_expr list * instance_expr option) CAst.t
-val destClassAppExpl : constr_expr -> (reference * (constr_expr * explicitation CAst.t option) list * instance_expr option) CAst.t
+val destClassApp : constr_expr -> (qualid * constr_expr list * instance_expr option) CAst.t
+val destClassAppExpl : constr_expr -> (qualid * (constr_expr * explicitation CAst.t option) list * instance_expr option) CAst.t
(** Fragile, should be used only for construction a set of identifiers to avoid *)
@@ -31,7 +31,7 @@ val free_vars_of_binders :
order with the location of their first occurrence *)
val generalizable_vars_of_glob_constr : ?bound:Id.Set.t -> ?allowed:Id.Set.t ->
- glob_constr -> Misctypes.lident list
+ glob_constr -> lident list
val make_fresh : Id.Set.t -> Environ.env -> Id.t -> Id.t
diff --git a/interp/modintern.ml b/interp/modintern.ml
index fefd2ab6f5..c27cc9cc07 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -12,7 +12,7 @@ open Declarations
open Libnames
open Constrexpr
open Constrintern
-open Misctypes
+open Declaremods
type module_internalization_error =
| NotAModuleNorModtype of string
@@ -23,7 +23,7 @@ exception ModuleInternalizationError of module_internalization_error
let error_not_a_module_loc kind loc qid =
let s = string_of_qualid qid in
- let e = match kind with
+ let e = let open Declaremods in match kind with
| Module -> Modops.ModuleTypingError (Modops.NotAModule s)
| ModType -> Modops.ModuleTypingError (Modops.NotAModuleType s)
| ModAny -> ModuleInternalizationError (NotAModuleNorModtype s)
@@ -45,7 +45,9 @@ let error_application_to_module_type loc =
or both are searched. The returned kind is never ModAny, and
it is equal to the input kind when this one isn't ModAny. *)
-let lookup_module_or_modtype kind {CAst.loc;v=qid} =
+let lookup_module_or_modtype kind qid =
+ let open Declaremods in
+ let loc = qid.CAst.loc in
try
if kind == ModType then raise Not_found;
let mp = Nametab.locate_module qid in
@@ -83,7 +85,7 @@ let loc_of_module l = l.CAst.loc
let rec interp_module_ast env kind m cst = match m with
| {CAst.loc;v=CMident qid} ->
- let (mp,kind) = lookup_module_or_modtype kind CAst.(make ?loc qid) in
+ let (mp,kind) = lookup_module_or_modtype kind qid in
(MEident mp, kind, cst)
| {CAst.loc;v=CMapply (me1,me2)} ->
let me1',kind1, cst = interp_module_ast env kind me1 cst in
diff --git a/interp/modintern.mli b/interp/modintern.mli
index ef37aead8a..529c438c1a 100644
--- a/interp/modintern.mli
+++ b/interp/modintern.mli
@@ -11,7 +11,6 @@
open Environ
open Entries
open Constrexpr
-open Misctypes
(** Module internalization errors *)
@@ -30,4 +29,4 @@ exception ModuleInternalizationError of module_internalization_error
isn't ModAny. *)
val interp_module_ast :
- env -> module_kind -> module_ast -> module_struct_entry * module_kind * Univ.ContextSet.t
+ env -> Declaremods.module_kind -> module_ast -> module_struct_entry * Declaremods.module_kind * Univ.ContextSet.t
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index f208b23fb6..ab0bf9c6fe 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 52a6354a0c..6d9effcef4 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/reserve.mli b/interp/reserve.mli
index daee58639f..a10858e71f 100644
--- a/interp/reserve.mli
+++ b/interp/reserve.mli
@@ -11,5 +11,5 @@
open Names
open Notation_term
-val declare_reserved_type : Misctypes.lident list -> notation_constr -> unit
+val declare_reserved_type : lident list -> notation_constr -> unit
val find_reserved_type : Id.t -> notation_constr
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index 1f4a93a6f3..91491bdf8d 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -18,7 +18,6 @@ open Pp
open CErrors
open Libnames
open Globnames
-open Misctypes
open Syntax_def
open Notation_term
@@ -42,36 +41,34 @@ let global_of_extended_global = function
| [],NApp (NRef ref,[]) -> ref
| _ -> raise Not_found
-let locate_global_with_alias ?(head=false) {CAst.loc; v=qid} =
+let locate_global_with_alias ?(head=false) qid =
let ref = Nametab.locate_extended qid in
try
if head then global_of_extended_global_head ref
else global_of_extended_global ref
with Not_found ->
- user_err ?loc (pr_qualid qid ++
+ user_err ?loc:qid.CAst.loc (pr_qualid qid ++
str " is bound to a notation that does not denote a reference.")
-let global_inductive_with_alias ({CAst.loc} as lr) =
- let qid = qualid_of_reference lr in
+let global_inductive_with_alias qid =
try match locate_global_with_alias qid with
| IndRef ind -> ind
| ref ->
- user_err ?loc ~hdr:"global_inductive"
- (pr_reference lr ++ spc () ++ str "is not an inductive type.")
+ user_err ?loc:qid.CAst.loc ~hdr:"global_inductive"
+ (pr_qualid qid ++ spc () ++ str "is not an inductive type.")
with Not_found -> Nametab.error_global_not_found qid
-let global_with_alias ?head r =
- let qid = qualid_of_reference r in
+let global_with_alias ?head qid =
try locate_global_with_alias ?head qid
with Not_found -> Nametab.error_global_not_found qid
-let smart_global ?head = CAst.with_loc_val (fun ?loc -> function
+let smart_global ?head = let open Constrexpr in CAst.with_loc_val (fun ?loc -> function
| AN r ->
global_with_alias ?head r
| ByNotation (ntn,sc) ->
Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc)
-let smart_global_inductive = CAst.with_loc_val (fun ?loc -> function
+let smart_global_inductive = let open Constrexpr in CAst.with_loc_val (fun ?loc -> function
| AN r ->
global_inductive_with_alias r
| ByNotation (ntn,sc) ->
diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli
index 45037b8b36..e41ef78913 100644
--- a/interp/smartlocate.mli
+++ b/interp/smartlocate.mli
@@ -11,14 +11,13 @@
open Names
open Libnames
open Globnames
-open Misctypes
(** [locate_global_with_alias] locates global reference possibly following
a notation if this notation has a role of aliasing; raise [Not_found]
if not bound in the global env; raise a [UserError] if bound to a
syntactic def that does not denote a reference *)
-val locate_global_with_alias : ?head:bool -> qualid CAst.t -> GlobRef.t
+val locate_global_with_alias : ?head:bool -> qualid -> GlobRef.t
(** Extract a global_reference from a reference that can be an "alias" *)
val global_of_extended_global : extended_global_reference -> GlobRef.t
@@ -27,13 +26,13 @@ val global_of_extended_global : extended_global_reference -> GlobRef.t
May raise [Nametab.GlobalizationError _] for an unknown reference,
or a [UserError] if bound to a syntactic def that does not denote
a reference. *)
-val global_with_alias : ?head:bool -> reference -> GlobRef.t
+val global_with_alias : ?head:bool -> qualid -> GlobRef.t
(** The same for inductive types *)
-val global_inductive_with_alias : reference -> inductive
+val global_inductive_with_alias : qualid -> inductive
(** Locate a reference taking into account notations and "aliases" *)
-val smart_global : ?head:bool -> reference or_by_notation -> GlobRef.t
+val smart_global : ?head:bool -> qualid Constrexpr.or_by_notation -> GlobRef.t
(** The same for inductive types *)
-val smart_global_inductive : reference or_by_notation -> inductive
+val smart_global_inductive : qualid Constrexpr.or_by_notation -> inductive
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index e5ed58be6b..7b01b6dc1c 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -11,6 +11,8 @@
open Genarg
open Geninterp
+type 'a and_short_name = 'a * Names.lident option
+
let make0 ?dyn name =
let wit = Genarg.make0 name in
let () = register_val0 wit dyn in
@@ -34,9 +36,6 @@ let wit_pre_ident : string uniform_genarg_type =
let wit_int_or_var =
make0 ~dyn:(val_tag (topwit wit_int)) "int_or_var"
-let wit_intro_pattern =
- make0 "intropattern"
-
let wit_ident =
make0 "ident"
@@ -45,8 +44,6 @@ let wit_var =
let wit_ref = make0 "ref"
-let wit_quant_hyp = make0 "quant_hyp"
-
let wit_sort_family = make0 "sort_family"
let wit_constr =
@@ -56,12 +53,6 @@ let wit_uconstr = make0 "uconstr"
let wit_open_constr = make0 ~dyn:(val_tag (topwit wit_constr)) "open_constr"
-let wit_constr_with_bindings = make0 "constr_with_bindings"
-
-let wit_open_constr_with_bindings = make0 "open_constr_with_bindings"
-
-let wit_bindings = make0 "bindings"
-
let wit_red_expr = make0 "redexpr"
let wit_clause_dft_concl =
@@ -74,6 +65,4 @@ let wit_preident = wit_pre_ident
let wit_reference = wit_ref
let wit_global = wit_ref
let wit_clause = wit_clause_dft_concl
-let wit_quantified_hypothesis = wit_quant_hyp
-let wit_intropattern = wit_intro_pattern
let wit_redexpr = wit_red_expr
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index dc9c370a1b..5e5e43ed38 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -17,9 +17,11 @@ open Libnames
open Genredexpr
open Pattern
open Constrexpr
-open Misctypes
-open Tactypes
open Genarg
+open Genintern
+open Locus
+
+type 'a and_short_name = 'a * lident option
val wit_unit : unit uniform_genarg_type
@@ -35,15 +37,11 @@ val wit_pre_ident : string uniform_genarg_type
val wit_int_or_var : (int or_var, int or_var, int) genarg_type
-val wit_intro_pattern : (constr_expr intro_pattern_expr CAst.t, glob_constr_and_expr intro_pattern_expr CAst.t, intro_pattern) genarg_type
-
val wit_ident : Id.t uniform_genarg_type
val wit_var : (lident, lident, Id.t) genarg_type
-val wit_ref : (reference, GlobRef.t located or_var, GlobRef.t) genarg_type
-
-val wit_quant_hyp : quantified_hypothesis uniform_genarg_type
+val wit_ref : (qualid, GlobRef.t located or_var, GlobRef.t) genarg_type
val wit_sort_family : (Sorts.family, unit, unit) genarg_type
@@ -54,23 +52,8 @@ val wit_uconstr : (constr_expr , glob_constr_and_expr, Ltac_pretype.closed_glob_
val wit_open_constr :
(constr_expr, glob_constr_and_expr, constr) genarg_type
-val wit_constr_with_bindings :
- (constr_expr with_bindings,
- glob_constr_and_expr with_bindings,
- constr with_bindings delayed_open) genarg_type
-
-val wit_open_constr_with_bindings :
- (constr_expr with_bindings,
- glob_constr_and_expr with_bindings,
- constr with_bindings delayed_open) genarg_type
-
-val wit_bindings :
- (constr_expr bindings,
- glob_constr_and_expr bindings,
- constr bindings delayed_open) genarg_type
-
val wit_red_expr :
- ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,
+ ((constr_expr,qualid or_by_notation,constr_expr) red_expr_gen,
(glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
(constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type
@@ -80,12 +63,10 @@ val wit_clause_dft_concl : (lident Locus.clause_expr, lident Locus.clause_expr,
val wit_integer : int uniform_genarg_type
val wit_preident : string uniform_genarg_type
-val wit_reference : (reference, GlobRef.t located or_var, GlobRef.t) genarg_type
-val wit_global : (reference, GlobRef.t located or_var, GlobRef.t) genarg_type
+val wit_reference : (qualid, GlobRef.t located or_var, GlobRef.t) genarg_type
+val wit_global : (qualid, GlobRef.t located or_var, GlobRef.t) genarg_type
val wit_clause : (lident Locus.clause_expr, lident Locus.clause_expr, Names.Id.t Locus.clause_expr) genarg_type
-val wit_quantified_hypothesis : quantified_hypothesis uniform_genarg_type
-val wit_intropattern : (constr_expr intro_pattern_expr CAst.t, glob_constr_and_expr intro_pattern_expr CAst.t, intro_pattern) genarg_type
val wit_redexpr :
- ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,
+ ((constr_expr,qualid or_by_notation,constr_expr) red_expr_gen,
(glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
(constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type
diff --git a/interp/tactypes.ml b/interp/tactypes.ml
deleted file mode 100644
index 83e42be89f..0000000000
--- a/interp/tactypes.ml
+++ /dev/null
@@ -1,34 +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) *)
-(************************************************************************)
-
-(** Tactic-related types that are not totally Ltac specific and still used in
- lower API. It's not clear whether this is a temporary API or if this is
- meant to stay. *)
-
-open Names
-open Constrexpr
-open Pattern
-open Misctypes
-
-(** In globalize tactics, we need to keep the initial [constr_expr] to recompute
- in the environment by the effective calls to Intro, Inversion, etc
- The [constr_expr] field is [None] in TacDef though *)
-type glob_constr_and_expr = Glob_term.glob_constr * constr_expr option
-type glob_constr_pattern_and_expr = Id.Set.t * glob_constr_and_expr * constr_pattern
-
-type 'a delayed_open = Environ.env -> Evd.evar_map -> Evd.evar_map * 'a
-
-type delayed_open_constr = EConstr.constr delayed_open
-type delayed_open_constr_with_bindings = EConstr.constr with_bindings 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 00:38:38 +0000