aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrextern.ml12
-rw-r--r--interp/constrintern.ml24
-rw-r--r--interp/constrintern.mli3
-rw-r--r--interp/notation.ml1
-rw-r--r--interp/notation_ops.ml4
-rw-r--r--interp/stdarg.ml2
-rw-r--r--interp/stdarg.mli1
-rw-r--r--interp/syntax_def.ml2
8 files changed, 17 insertions, 32 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index bdbfd8c277..59b8b4e5b9 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -654,11 +654,9 @@ let rec extern inctx scopes vars r =
| GEvar (loc,n,l) ->
extern_evar loc n (List.map (on_snd (extern false scopes vars)) l)
- | GPatVar (loc,kind) ->
- if !print_meta_as_hole then CHole (loc, None, Misctypes.IntroAnonymous, None) else
- (match kind with
- | Evar_kinds.SecondOrderPatVar n -> CPatVar (loc,n)
- | Evar_kinds.FirstOrderPatVar n -> CEvar (loc,n,[]))
+ | GPatVar (loc,(b,n)) ->
+ if !print_meta_as_hole then CHole (loc, None, Misctypes.IntroAnonymous, None) else
+ if b then CPatVar (loc,n) else CEvar (loc,n,[])
| GApp (loc,f,args) ->
(match f with
@@ -1031,13 +1029,13 @@ let rec glob_of_pat env sigma = function
with Not_found -> Id.of_string ("_UNBOUND_REL_"^(string_of_int n)) in
GVar (loc,id)
| PMeta None -> GHole (loc,Evar_kinds.InternalHole, Misctypes.IntroAnonymous,None)
- | PMeta (Some n) -> GPatVar (loc,Evar_kinds.FirstOrderPatVar n)
+ | PMeta (Some n) -> GPatVar (loc,(false,n))
| PProj (p,c) -> GApp (loc,GRef (loc, ConstRef (Projection.constant p),None),
[glob_of_pat env sigma c])
| PApp (f,args) ->
GApp (loc,glob_of_pat env sigma f,Array.map_to_list (glob_of_pat env sigma) args)
| PSoApp (n,args) ->
- GApp (loc,GPatVar (loc,Evar_kinds.SecondOrderPatVar n),
+ GApp (loc,GPatVar (loc,(true,n)),
List.map (glob_of_pat env sigma) args)
| PProd (na,t,c) ->
GProd (loc,na,Explicit,glob_of_pat env sigma t,glob_of_pat (na::env) sigma c)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index ea1802ccfa..3f99a3c7c0 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -855,9 +855,9 @@ let intern_qualid loc qid intern env lvar us args =
| Some _, GApp (loc, GRef (loc', ref, None), arg) ->
GApp (loc, GRef (loc', ref, us), arg)
| Some _, _ ->
- user_err ~loc (str "Notation " ++ pr_qualid qid ++
- str " cannot have a universe instance, its expanded head
- does not start with a reference")
+ 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
c, projapp, args2
@@ -1516,7 +1516,7 @@ let extract_explicit_arg imps args =
(**********************************************************************)
(* Main loop *)
-let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
+let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
let rec intern env = function
| CRef (ref,us) as x ->
let (c,imp,subscopes,l),_ =
@@ -1747,10 +1747,10 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
in
GHole (loc, k, naming, solve)
(* Parsing pattern variables *)
- | CPatVar (loc, n) when pattern_mode ->
- GPatVar (loc, Evar_kinds.SecondOrderPatVar n)
- | CEvar (loc, n, []) when pattern_mode ->
- GPatVar (loc, Evar_kinds.FirstOrderPatVar n)
+ | CPatVar (loc, n) when allow_patvar ->
+ GPatVar (loc, (true,n))
+ | CEvar (loc, n, []) when allow_patvar ->
+ GPatVar (loc, (false,n))
(* end *)
(* Parsing existential variables *)
| CEvar (loc, n, l) ->
@@ -1934,13 +1934,13 @@ let empty_ltac_sign = {
}
let intern_gen kind env
- ?(impls=empty_internalization_env) ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign)
+ ?(impls=empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=empty_ltac_sign)
c =
let tmp_scope = scope_of_type_kind kind in
internalize env {ids = extract_ids env; unb = false;
tmp_scope = tmp_scope; scopes = [];
impls = impls}
- pattern_mode (ltacvars, Id.Map.empty) c
+ allow_patvar (ltacvars, Id.Map.empty) c
let intern_constr env c = intern_gen WithoutTypeConstraint env c
@@ -2013,7 +2013,7 @@ let interp_type_evars env evdref ?(impls=empty_internalization_env) c =
let intern_constr_pattern env ?(as_type=false) ?(ltacvars=empty_ltac_sign) c =
let c = intern_gen (if as_type then IsType else WithoutTypeConstraint)
- ~pattern_mode:true ~ltacvars env c in
+ ~allow_patvar:true ~ltacvars env c in
pattern_of_glob_constr c
let interp_notation_constr ?(impls=empty_internalization_env) nenv a =
@@ -2045,8 +2045,6 @@ let interp_binder_evars env evdref na t =
let t' = locate_if_hole (loc_of_glob_constr t) na t in
understand_tcc_evars env evdref ~expected_type:IsType t'
-open Environ
-
let my_intern_constr env lvar acc c =
internalize env acc false lvar c
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 2142d42bce..fdd50c6a1e 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -18,7 +18,6 @@ open Constrexpr
open Notation_term
open Pretyping
open Misctypes
-open Decl_kinds
(** Translation from front abstract syntax of term to untyped terms (glob_constr) *)
@@ -82,7 +81,7 @@ val intern_constr : env -> constr_expr -> glob_constr
val intern_type : env -> constr_expr -> glob_constr
val intern_gen : typing_constraint -> env ->
- ?impls:internalization_env -> ?pattern_mode:bool -> ?ltacvars:ltac_sign ->
+ ?impls:internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
constr_expr -> glob_constr
val intern_pattern : env -> cases_pattern_expr ->
diff --git a/interp/notation.ml b/interp/notation.ml
index 90ac7f7296..6aa6f54c05 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -22,7 +22,6 @@ open Glob_ops
open Ppextend
open Context.Named.Declaration
-module NamedDecl = Context.Named.Declaration
(*i*)
(*s A scope is a set of notations; it includes
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 8b4fadb5a0..d08fb107be 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -1141,10 +1141,6 @@ let term_of_binder = function
| Name id -> GVar (Loc.ghost,id)
| Anonymous -> GHole (Loc.ghost,Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None)
-type glob_decl2 =
- (name, cases_pattern) Util.union * Decl_kinds.binding_kind *
- glob_constr option * glob_constr
-
let match_notation_constr u c (metas,pat) =
let terms,binders,termlists,binderlists =
match_ false u ([],[]) metas ([],[],[],[]) c pat in
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index 341ff5662c..5920b0d508 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -6,9 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Loc
open Misctypes
-open Tactypes
open Genarg
open Geninterp
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index 113fe40ba7..ac40a23281 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -10,7 +10,6 @@
open Loc
open Names
-open Term
open EConstr
open Libnames
open Globnames
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index c3f4c4f302..ed7b0b70d4 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -106,5 +106,3 @@ let search_syntactic_definition kn =
let def = out_pat pat in
verbose_compat kn def v;
def
-
-open Goptions
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 11:49:15 +0000