aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrintern.ml8
-rw-r--r--interp/constrintern.mli1
-rw-r--r--interp/implicit_quantifiers.ml62
-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
-rw-r--r--interp/topconstr.ml7
9 files changed, 10 insertions, 78 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index d75487ecf3..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
@@ -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 758d4e650b..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) *)
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 7f11c0a3b6..19c872b310 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -19,7 +19,6 @@ open Typeclasses_errors
open Pp
open Libobject
open Nameops
-open Misctypes
open Context.Rel.Declaration
module RelDecl = Context.Rel.Declaration
@@ -119,11 +118,6 @@ let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder_expr li
| [] -> bdvars, l
in aux bound l binders
-let add_name_to_ids set na =
- match na with
- | Anonymous -> set
- | Name id -> Id.Set.add id set
-
let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.empty) =
let rec vars bound vs = function
| GVar (loc,id) ->
@@ -131,61 +125,7 @@ let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.emp
if Id.List.mem_assoc id vs then vs
else (id, loc) :: vs
else vs
- | GApp (loc,f,args) -> List.fold_left (vars bound) vs (f::args)
- | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) ->
- let vs' = vars bound vs ty in
- let bound' = add_name_to_ids bound na in
- vars bound' vs' c
- | GLetIn (loc,na,b,ty,c) ->
- let vs' = vars bound vs b in
- let vs'' = Option.fold_left (vars bound) vs' ty in
- let bound' = add_name_to_ids bound na in
- vars bound' vs'' c
- | GCases (loc,sty,rtntypopt,tml,pl) ->
- let vs1 = vars_option bound vs rtntypopt in
- let vs2 = List.fold_left (fun vs (tm,_) -> vars bound vs tm) vs1 tml in
- List.fold_left (vars_pattern bound) vs2 pl
- | GLetTuple (loc,nal,rtntyp,b,c) ->
- let vs1 = vars_return_type bound vs rtntyp in
- let vs2 = vars bound vs1 b in
- let bound' = List.fold_left add_name_to_ids bound nal in
- vars bound' vs2 c
- | GIf (loc,c,rtntyp,b1,b2) ->
- let vs1 = vars_return_type bound vs rtntyp in
- let vs2 = vars bound vs1 c in
- let vs3 = vars bound vs2 b1 in
- vars bound vs3 b2
- | GRec (loc,fk,idl,bl,tyl,bv) ->
- let bound' = Array.fold_right Id.Set.add idl bound in
- let vars_fix i vs fid =
- let vs1,bound1 =
- List.fold_left
- (fun (vs,bound) (na,k,bbd,bty) ->
- let vs' = vars_option bound vs bbd in
- let vs'' = vars bound vs' bty in
- let bound' = add_name_to_ids bound na in
- (vs'',bound')
- )
- (vs,bound')
- bl.(i)
- in
- let vs2 = vars bound1 vs1 tyl.(i) in
- vars bound1 vs2 bv.(i)
- in
- Array.fold_left_i vars_fix vs idl
- | GCast (loc,c,k) -> let v = vars bound vs c in
- (match k with CastConv t | CastVM t -> vars bound v t | _ -> v)
- | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> vs
-
- and vars_pattern bound vs (loc,idl,p,c) =
- let bound' = List.fold_right Id.Set.add idl bound in
- vars bound' vs c
-
- and vars_option bound vs = function None -> vs | Some p -> vars bound vs p
-
- and vars_return_type bound vs (na,tyopt) =
- let bound' = add_name_to_ids bound na in
- vars_option bound' vs tyopt
+ | c -> Glob_ops.fold_glob_constr_with_binders Id.Set.add vars bound vs c
in fun rt ->
let vars = List.rev (vars bound [] rt) in
List.iter (fun (id, loc) ->
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
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index d3142e7f0c..e05be65fb0 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -178,7 +178,12 @@ let split_at_annot bl na =
in
(List.rev ans, CLocalAssum (r, k, t) :: rest)
end
- | CLocalDef _ as x :: rest -> aux (x :: acc) rest
+ | CLocalDef ((_,na),_,_) as x :: rest ->
+ if Name.equal (Name id) na then
+ user_err ~loc
+ (Nameops.pr_id id ++ str" must be a proper parameter and not a local definition.")
+ else
+ aux (x :: acc) rest
| CLocalPattern (loc,_,_) :: rest ->
Loc.raise ~loc (Stream.Error "pattern with quote not allowed after fix")
| [] ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 00:00:45 +0000