aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/himsg.ml2
-rw-r--r--vernac/indschemes.ml12
-rw-r--r--vernac/indschemes.mli3
-rw-r--r--vernac/metasyntax.ml49
4 files changed, 31 insertions, 35 deletions
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 2be10a0397..e15911dd65 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -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 6ea8bc7f2c..facebd096a 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 076e4938fd..91c4c58255 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 8b042a3ca3..c424b1d501 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 04:01:39 +0000