aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/command.ml4
-rw-r--r--vernac/himsg.ml4
-rw-r--r--vernac/indschemes.ml12
-rw-r--r--vernac/indschemes.mli3
-rw-r--r--vernac/metasyntax.ml49
-rw-r--r--vernac/topfmt.ml5
-rw-r--r--vernac/vernacentries.ml13
7 files changed, 44 insertions, 46 deletions
diff --git a/vernac/command.ml b/vernac/command.ml
index a315ac14e..32ab5401a 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -241,7 +241,7 @@ let do_assumptions_unbound_univs (_, poly, _ as kind) nl l =
else l
in
(* We intepret all declarations in the same evar_map, i.e. as a telescope. *)
- let _,l = List.fold_map (fun (env,ienv) (is_coe,(idl,c)) ->
+ let _,l = List.fold_left_map (fun (env,ienv) (is_coe,(idl,c)) ->
let t,imps = interp_assumption evdref env ienv [] c in
let env =
push_named_context (List.map (fun (_,id) -> LocalAssum (id,t)) idl) env in
@@ -367,7 +367,7 @@ let prepare_param = function
let rec check_anonymous_type ind =
let open Glob_term in
- match ind.CAst.v with
+ match DAst.get ind with
| GSort (GType []) -> true
| GProd ( _, _, _, e)
| GLetIn (_, _, _, e)
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 2be10a039..12b68fe38 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -418,7 +418,7 @@ let explain_not_product env sigma c =
let pr = pr_lconstr_env env sigma c in
str "The type of this term is a product" ++ spc () ++
str "while it is expected to be" ++
- (if is_Type c then str " a sort" else (brk(1,1) ++ pr)) ++ str "."
+ (if Term.is_Type c then str " a sort" else (brk(1,1) ++ pr)) ++ str "."
(* TODO: use the names *)
(* (co)fixpoints *)
@@ -1176,7 +1176,7 @@ let error_not_allowed_case_analysis isrec kind i =
pr_inductive (Global.env()) (fst i) ++ str "."
let error_not_allowed_dependent_analysis isrec i =
- str "Dependent " ++ str (if isrec then "Induction" else "Case analysis") ++
+ str "Dependent " ++ str (if isrec then "induction" else "case analysis") ++
strbrk " is not allowed for inductive definition " ++
pr_inductive (Global.env()) i ++ str "."
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 6ea8bc7f2..facebd096 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -30,7 +30,6 @@ open Globnames
open Goptions
open Nameops
open Termops
-open Pretyping
open Nametab
open Smartlocate
open Vernacexpr
@@ -345,24 +344,23 @@ requested
let names inds recs isdep y z =
let ind = smart_global_inductive y in
let sort_of_ind = inductive_sort_family (snd (lookup_mind_specif env ind)) in
- let z' = interp_elimination_sort z in
let suffix = (
match sort_of_ind with
| InProp ->
- if isdep then (match z' with
+ if isdep then (match z with
| InProp -> inds ^ "_dep"
| InSet -> recs ^ "_dep"
| InType -> recs ^ "t_dep")
- else ( match z' with
+ else ( match z with
| InProp -> inds
| InSet -> recs
| InType -> recs ^ "t" )
| _ ->
- if isdep then (match z' with
+ if isdep then (match z with
| InProp -> inds
| InSet -> recs
| InType -> recs ^ "t" )
- else (match z' with
+ else (match z with
| InProp -> inds ^ "_nodep"
| InSet -> recs ^ "_nodep"
| InType -> recs ^ "t_nodep")
@@ -392,7 +390,7 @@ let do_mutual_induction_scheme lnamedepindsort =
evd, (ind,u), Some u
| Some ui -> evd, (ind, ui), inst
in
- (evd, (indu,dep,interp_elimination_sort sort) :: l, inst))
+ (evd, (indu,dep,sort) :: l, inst))
lnamedepindsort (Evd.from_env env0,[],None)
in
let sigma, listdecl = Indrec.build_mutual_induction_scheme env0 sigma lrecspec in
diff --git a/vernac/indschemes.mli b/vernac/indschemes.mli
index 076e4938f..91c4c5825 100644
--- a/vernac/indschemes.mli
+++ b/vernac/indschemes.mli
@@ -11,7 +11,6 @@ open Names
open Term
open Environ
open Vernacexpr
-open Misctypes
(** See also Auto_ind_decl, Indrec, Eqscheme, Ind_tables, ... *)
@@ -32,7 +31,7 @@ val declare_rewriting_schemes : inductive -> unit
(** Mutual Minimality/Induction scheme *)
val do_mutual_induction_scheme :
- (Id.t located * bool * inductive * glob_sort) list -> unit
+ (Id.t located * bool * inductive * Sorts.family) list -> unit
(** Main calls to interpret the Scheme command *)
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 8b042a3ca..c424b1d50 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -98,8 +98,7 @@ let pr_grammar = function
quote (except a single quote alone) must be quoted) *)
let parse_format ((loc, str) : lstring) =
- let str = " "^str in
- let l = String.length str in
+ let len = String.length str in
let push_token a = function
| cur::l -> (a::cur)::l
| [] -> [[a]] in
@@ -109,16 +108,16 @@ let parse_format ((loc, str) : lstring) =
| a::(_::_ as l) -> push_token (UnpBox (b,a)) l
| _ -> user_err Pp.(str "Non terminated box in format.") in
let close_quotation i =
- if i < String.length str && str.[i] == '\'' && (Int.equal (i+1) l || str.[i+1] == ' ')
+ if i < len && str.[i] == '\'' && (Int.equal (i+1) len || str.[i+1] == ' ')
then i+1
else user_err Pp.(str "Incorrectly terminated quoted expression.") in
let rec spaces n i =
- if i < String.length str && str.[i] == ' ' then spaces (n+1) (i+1)
+ if i < len && str.[i] == ' ' then spaces (n+1) (i+1)
else n in
let rec nonspaces quoted n i =
- if i < String.length str && str.[i] != ' ' then
+ if i < len && str.[i] != ' ' then
if str.[i] == '\'' && quoted &&
- (i+1 >= String.length str || str.[i+1] == ' ')
+ (i+1 >= len || str.[i+1] == ' ')
then if Int.equal n 0 then user_err Pp.(str "Empty quoted token.") else n
else nonspaces quoted (n+1) (i+1)
else
@@ -126,26 +125,26 @@ let parse_format ((loc, str) : lstring) =
else n in
let rec parse_non_format i =
let n = nonspaces false 0 i in
- push_token (UnpTerminal (String.sub str i n)) (parse_token (i+n))
+ push_token (UnpTerminal (String.sub str i n)) (parse_token 1 (i+n))
and parse_quoted n i =
- if i < String.length str then match str.[i] with
+ if i < len then match str.[i] with
(* Parse " // " *)
- | '/' when i <= String.length str && str.[i+1] == '/' ->
+ | '/' when i <= len && str.[i+1] == '/' ->
(* We forget the useless n spaces... *)
push_token (UnpCut PpFnl)
- (parse_token (close_quotation (i+2)))
+ (parse_token 1 (close_quotation (i+2)))
(* Parse " .. / .. " *)
- | '/' when i <= String.length str ->
+ | '/' when i <= len ->
let p = spaces 0 (i+1) in
push_token (UnpCut (PpBrk (n,p)))
- (parse_token (close_quotation (i+p+1)))
+ (parse_token 1 (close_quotation (i+p+1)))
| c ->
(* The spaces are real spaces *)
push_white n (match c with
| '[' ->
- if i <= String.length str then match str.[i+1] with
+ if i <= len then match str.[i+1] with
(* Parse " [h .. ", *)
- | 'h' when i+1 <= String.length str && str.[i+2] == 'v' ->
+ | 'h' when i+1 <= len && str.[i+2] == 'v' ->
(parse_box (fun n -> PpHVB n) (i+3))
(* Parse " [v .. ", *)
| 'v' ->
@@ -157,39 +156,39 @@ let parse_format ((loc, str) : lstring) =
else user_err Pp.(str "\"v\", \"hv\" or \" \" expected after \"[\" in format.")
(* Parse "]" *)
| ']' ->
- ([] :: parse_token (close_quotation (i+1)))
+ ([] :: parse_token 1 (close_quotation (i+1)))
(* Parse a non formatting token *)
| c ->
let n = nonspaces true 0 i in
push_token (UnpTerminal (String.sub str (i-1) (n+2)))
- (parse_token (close_quotation (i+n))))
+ (parse_token 1 (close_quotation (i+n))))
else
if Int.equal n 0 then []
else user_err Pp.(str "Ending spaces non part of a format annotation.")
and parse_box box i =
let n = spaces 0 i in
- close_box i (box n) (parse_token (close_quotation (i+n)))
- and parse_token i =
+ close_box i (box n) (parse_token 1 (close_quotation (i+n)))
+ and parse_token k i =
let n = spaces 0 i in
let i = i+n in
- if i < l then match str.[i] with
+ if i < len then match str.[i] with
(* Parse a ' *)
- | '\'' when i+1 >= String.length str || str.[i+1] == ' ' ->
- push_white (n-1) (push_token (UnpTerminal "'") (parse_token (i+1)))
+ | '\'' when i+1 >= len || str.[i+1] == ' ' ->
+ push_white (n-k) (push_token (UnpTerminal "'") (parse_token 1 (i+1)))
(* Parse the beginning of a quoted expression *)
| '\'' ->
- parse_quoted (n-1) (i+1)
+ parse_quoted (n-k) (i+1)
(* Otherwise *)
| _ ->
- push_white (n-1) (parse_non_format i)
+ push_white (n-k) (parse_non_format i)
else push_white n [[]]
in
try
- if not (String.is_empty str) then match parse_token 0 with
+ if not (String.is_empty str) then match parse_token 0 0 with
| [l] -> l
| _ -> user_err Pp.(str "Box closed without being opened in format.")
else
- user_err Pp.(str "Empty format.")
+ []
with reraise ->
let (e, info) = CErrors.push reraise in
let info = Option.cata (Loc.add_loc info) info loc in
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index e7b14309d..6a10eb43a 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -292,10 +292,11 @@ let emacs_logger = gen_logger Emacs.quote_info Emacs.quote_warning
(* This is specific to the toplevel *)
let pr_loc loc =
let fname = loc.Loc.fname in
- if CString.equal fname "" then
+ match fname with
+ | Loc.ToplevelInput ->
Loc.(str"Toplevel input, characters " ++ int loc.bp ++
str"-" ++ int loc.ep ++ str":")
- else
+ | Loc.InFile fname ->
Loc.(str"File " ++ str "\"" ++ str fname ++ str "\"" ++
str", line " ++ int loc.line_nb ++ str", characters " ++
int (loc.bp-loc.bol_pos) ++ str"-" ++ int (loc.ep-loc.bol_pos) ++
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 8738e58e8..4fd08b42d 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -409,9 +409,10 @@ let dump_global r =
(**********)
(* Syntax *)
-let vernac_syntax_extension locality local =
+let vernac_syntax_extension locality local infix l =
let local = enforce_module_locality locality local in
- Metasyntax.add_syntax_extension local
+ if infix then Metasyntax.check_infix_modifiers (snd l);
+ Metasyntax.add_syntax_extension local l
let vernac_delimiters sc = function
| Some lr -> Metasyntax.add_delimiters sc lr
@@ -1230,7 +1231,7 @@ let vernac_reserve bl =
let env = Global.env() in
let sigma = Evd.from_env env in
let t,ctx = Constrintern.interp_type env sigma c in
- let t = Detyping.detype false [] env (Evd.from_ctx ctx) (EConstr.of_constr t) in
+ let t = Detyping.detype Detyping.Now false [] env (Evd.from_ctx ctx) (EConstr.of_constr t) in
let t,_ = Notation_ops.notation_constr_of_glob_constr (default_env ()) t in
Reserve.declare_reserved_type idl t)
in List.iter sb_decl bl
@@ -1902,7 +1903,7 @@ let vernac_load interp fname =
let input =
let longfname = Loadpath.locate_file fname in
let in_chan = open_utf8_file_in longfname in
- Pcoq.Gram.parsable ~file:longfname (Stream.of_channel in_chan) in
+ Pcoq.Gram.parsable ~file:(Loc.InFile longfname) (Stream.of_channel in_chan) in
try while true do interp (snd (parse_sentence input)) done
with End_of_input -> ()
@@ -1950,8 +1951,8 @@ let interp ?proof ?loc locality poly c =
| VernacLocal _ -> assert false
(* Syntax *)
- | VernacSyntaxExtension (local,sl) ->
- vernac_syntax_extension locality local sl
+ | VernacSyntaxExtension (infix, local,sl) ->
+ vernac_syntax_extension locality local infix sl
| VernacDelimiters (sc,lr) -> vernac_delimiters sc lr
| VernacBindScope (sc,rl) -> vernac_bind_scope sc rl
| VernacOpenCloseScope (local, s) -> vernac_open_close_scope locality local s
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-24 12:01:18 +0000