aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--ide/coq.lang4
-rw-r--r--intf/vernacexpr.mli6
-rw-r--r--parsing/g_vernac.ml440
-rw-r--r--plugins/funind/g_indfun.ml42
-rw-r--r--plugins/funind/glob_term_to_relation.ml4
-rw-r--r--printing/ppvernac.ml19
-rw-r--r--stm/texmacspp.ml6
-rw-r--r--stm/vernac_classifier.ml6
-rw-r--r--toplevel/vernacentries.ml7
9 files changed, 30 insertions, 64 deletions
diff --git a/ide/coq.lang b/ide/coq.lang
index a31eadc707..c65432bdb7 100644
--- a/ide/coq.lang
+++ b/ide/coq.lang
@@ -29,13 +29,12 @@
<define-regex id="qualit">(\%{ident}\.)*\%{ident}</define-regex>
<define-regex id="dot_sep">\.(\s|\z)</define-regex>
<define-regex id="bullet">([-+*]+|{)(\s|\z)|}(\s*})*</define-regex>
- <define-regex id="assume">(?'gal0'Assume)\%{space}\[\%{ident}*\]\%{space}</define-regex>
<define-regex id="single_decl">Definition|Let|Example|SubClass|(Co)?Fixpoint|Function|Conjecture|(Co)?Inductive|Record|Structure|Ltac|Instance|Class|Existing\%{space}Instance|Canonical\%{space}Structure|Coercion</define-regex>
<define-regex id="mult_decl">Hypothes[ie]s|Axiom(s)?|Variable(s)?|Parameter(s)?|Context|Implicit\%{space}Type(s)?</define-regex>
<define-regex id="locality">((Local|Global)\%{space})?</define-regex>
<define-regex id="begin_proof">Theorem|Lemma|Fact|Remark|Corollary|Proposition|Property</define-regex>
<define-regex id="end_proof">Qed|Defined|Admitted|Abort|Save</define-regex>
- <define-regex id="decl_head">((\%{assume})?(?'gal'\%{locality}(Program\%{space})?(\%{single_decl}|\%{begin_proof}))\%{space}(?'id'\%{ident}))|((?'gal4list'\%{mult_decl})(?'id_list'(\%{space}\%{ident})*))|(?'gal2'Goal)</define-regex>
+ <define-regex id="decl_head">((?'gal'\%{locality}(Program\%{space})?(\%{single_decl}|\%{begin_proof}))\%{space}(?'id'\%{ident}))|((?'gal4list'\%{mult_decl})(?'id_list'(\%{space}\%{ident})*))|(?'gal2'Goal)</define-regex>
<!-- Strings, with '""' an escape sequence -->
<context id="string" style-ref="string" class="string">
@@ -107,7 +106,6 @@
<end>\%{dot_sep}</end>
<include>
<context sub-pattern="id" where="start" style-ref="identifier"/>
- <context sub-pattern="gal0" where="start" style-ref="gallina-keyword"/>
<context sub-pattern="gal" where="start" style-ref="gallina-keyword"/>
<context sub-pattern="gal2" where="start" style-ref="gallina-keyword"/>
<context sub-pattern="id_list" where="start" style-ref="identifier"/>
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 2f2f973761..d7b269a1de 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -303,14 +303,10 @@ type vernac_expr =
| VernacExactProof of constr_expr
| VernacAssumption of (locality option * assumption_object_kind) *
inline * simple_binder with_coercion list
- | VernacInductive of
- bool (*[false] => assume positive*) *
- private_flag * inductive_flag * (inductive_expr * decl_notation list) list
+ | VernacInductive of private_flag * inductive_flag * (inductive_expr * decl_notation list) list
| VernacFixpoint of
- Declarations.typing_flags *
locality option * (fixpoint_expr * decl_notation list) list
| VernacCoFixpoint of
- Declarations.typing_flags *
locality option * (cofixpoint_expr * decl_notation list) list
| VernacScheme of (lident option * scheme) list
| VernacCombinedScheme of lident * lident list
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 3ad5e77fcf..e8a1b512c0 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -71,19 +71,6 @@ let make_bullet s =
| '*' -> Star n
| _ -> assert false
-type nl_assumption =
- | Positive
- | Guarded
-let eq_nl_assumption x y =
- match x,y with
- | Positive,Positive -> true
- | Guarded,Guarded -> true
- | _ , _ -> false
-let check_positivity l =
- not (List.mem_f eq_nl_assumption Positive l)
-let check_guardedness l =
- not (List.mem_f eq_nl_assumption Guarded l)
-
let default_command_entry =
Gram.Entry.of_parser "command_entry"
(fun strm -> Gram.parse_tokens_after_filter (get_command_entry ()) strm)
@@ -213,19 +200,19 @@ GEXTEND Gram
| IDENT "Let"; id = identref; b = def_body ->
VernacDefinition ((Some Discharge, Definition), id, b)
(* Gallina inductive declarations *)
- | priv = private_token; a = assume_token; f = finite_token;
+ | priv = private_token; f = finite_token;
indl = LIST1 inductive_definition SEP "with" ->
let (k,f) = f in
let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in
- VernacInductive (check_positivity a,priv,f,indl)
- | "Fixpoint"; a=assume_token; recs = LIST1 rec_definition SEP "with" ->
- VernacFixpoint ({Declarations.check_guarded=check_guardedness a},None, recs)
- | IDENT "Let"; "Fixpoint"; a=assume_token; recs = LIST1 rec_definition SEP "with" ->
- VernacFixpoint ({Declarations.check_guarded=check_guardedness a},Some Discharge, recs)
- | "CoFixpoint"; a=assume_token; corecs = LIST1 corec_definition SEP "with" ->
- VernacCoFixpoint ({Declarations.check_guarded=check_guardedness a},None, corecs)
- | IDENT "Let"; "CoFixpoint"; a=assume_token; corecs = LIST1 corec_definition SEP "with" ->
- VernacCoFixpoint ({Declarations.check_guarded=check_guardedness a},Some Discharge, corecs)
+ VernacInductive (priv,f,indl)
+ | "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
+ VernacFixpoint (None, recs)
+ | IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
+ VernacFixpoint (Some Discharge, recs)
+ | "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" ->
+ VernacCoFixpoint (None, corecs)
+ | IDENT "Let"; "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" ->
+ VernacCoFixpoint (Some Discharge, corecs)
| IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l
| IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from";
l = LIST1 identref SEP "," -> VernacCombinedScheme (id, l)
@@ -282,13 +269,6 @@ GEXTEND Gram
| IDENT "Structure" -> (Structure,BiFinite)
| IDENT "Class" -> (Class true,BiFinite) ] ]
;
- assume_token:
- [ [ IDENT "Assume"; "[" ; l=LIST1 nl_assumption ; "]" -> l | -> [] ] ]
- ;
- nl_assumption:
- [ [ IDENT "Positive" -> Positive
- | IDENT "Guarded" -> Guarded ] ]
- ;
private_token:
[ [ IDENT "Private" -> true | -> false ] ]
;
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 91fcb3f8b9..61f03d6f22 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -166,7 +166,7 @@ VERNAC COMMAND EXTEND Function
| _,((_,(_,CStructRec),_,_,_),_) -> false) recsl in
match
Vernac_classifier.classify_vernac
- (Vernacexpr.VernacFixpoint({Declarations.check_guarded=true},None, List.map snd recsl))
+ (Vernacexpr.VernacFixpoint(None, List.map snd recsl))
with
| Vernacexpr.VtSideff ids, _ when hard ->
Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater)
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index b4febba668..f1c379ecc6 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1435,7 +1435,7 @@ let do_build_inductive
in
let msg =
str "while trying to define"++ spc () ++
- Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,false,Decl_kinds.Finite,repacked_rel_inds))
+ Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,Decl_kinds.Finite,repacked_rel_inds))
++ fnl () ++
msg
in
@@ -1450,7 +1450,7 @@ let do_build_inductive
in
let msg =
str "while trying to define"++ spc () ++
- Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,false,Decl_kinds.Finite,repacked_rel_inds))
+ Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,Decl_kinds.Finite,repacked_rel_inds))
++ fnl () ++
Errors.print reraise
in
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 8a8521ccc1..832c08fe0e 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -399,15 +399,6 @@ module Make
| None -> mt ()
| Some i -> spc () ++ str "|" ++ spc () ++ int i
- let pr_assume ?(positive=false) ?(guarded=false) () =
- let assumed =
- (if guarded then [str"Guarded"] else []) @
- (if positive then [str"Positive"] else [])
- in
- match assumed with
- | [] -> mt ()
- | l -> keyword"Assume" ++ spc() ++ str"[" ++ prlist (fun x->x) l ++ str"]" ++ spc()
-
(**************************************)
(* Pretty printer for vernac commands *)
(**************************************)
@@ -770,7 +761,7 @@ module Make
(pr_assumption_token (n > 1) stre ++ spc() ++
pr_ne_params_list pr_lconstr_expr l)
)
- | VernacInductive (chk,p,f,l) ->
+ | VernacInductive (p,f,l) ->
let pr_constructor (coe,(id,c)) =
hov 2 (pr_lident id ++ str" " ++
(if coe then str":>" else str":") ++
@@ -806,7 +797,7 @@ module Make
(prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l))
)
- | VernacFixpoint (flags,local, recs) ->
+ | VernacFixpoint (local, recs) ->
let local = match local with
| Some Discharge -> "Let "
| Some Local -> "Local "
@@ -821,11 +812,11 @@ module Make
prlist (pr_decl_notation pr_constr) ntn
in
return (
- hov 0 (pr_assume ~guarded:flags.Declarations.check_guarded ()++str local ++ keyword "Fixpoint" ++ spc () ++
+ hov 0 (str local ++ keyword "Fixpoint" ++ spc () ++
prlist_with_sep (fun _ -> fnl () ++ keyword "with" ++ spc ()) pr_onerec recs)
)
- | VernacCoFixpoint (flags,local, corecs) ->
+ | VernacCoFixpoint (local, corecs) ->
let local = match local with
| Some Discharge -> keyword "Let" ++ spc ()
| Some Local -> keyword "Local" ++ spc ()
@@ -838,7 +829,7 @@ module Make
prlist (pr_decl_notation pr_constr) ntn
in
return (
- hov 0 (pr_assume ~guarded:flags.Declarations.check_guarded ()++local ++ keyword "CoFixpoint" ++ spc() ++
+ hov 0 (local ++ keyword "CoFixpoint" ++ spc() ++
prlist_with_sep (fun _ -> fnl() ++ keyword "with" ++ spc ()) pr_onecorec corecs)
)
| VernacScheme l ->
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml
index 4f014be2de..9edc1f1c70 100644
--- a/stm/texmacspp.ml
+++ b/stm/texmacspp.ml
@@ -580,7 +580,7 @@ let rec tmpp v loc =
let l = match l with Some x -> x | None -> Decl_kinds.Global in
let kind = string_of_assumption_kind l a many in
xmlAssumption kind loc exprs
- | VernacInductive (_,_, _, iednll) ->
+ | VernacInductive (_, _, iednll) ->
let kind =
let (_, _, _, k, _),_ = List.hd iednll in
begin
@@ -598,14 +598,14 @@ let rec tmpp v loc =
(fun (ie, dnl) -> (pp_inductive_expr ie) @
(List.map pp_decl_notation dnl)) iednll) in
xmlInductive kind loc exprs
- | VernacFixpoint (_,_, fednll) ->
+ | VernacFixpoint (_, fednll) ->
let exprs =
List.flatten (* should probably not be flattened *)
(List.map
(fun (fe, dnl) -> (pp_fixpoint_expr fe) @
(List.map pp_decl_notation dnl)) fednll) in
xmlFixpoint exprs
- | VernacCoFixpoint (_,_, cfednll) ->
+ | VernacCoFixpoint (_, cfednll) ->
(* Nota: it is like VernacFixpoint without so could be merged *)
let exprs =
List.flatten (* should probably not be flattened *)
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 574cc0044c..2b5eb86834 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -125,14 +125,14 @@ let rec classify_vernac e =
CList.map_filter (function (Some(_,i), _) -> Some i | _ -> None) l in
VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
| VernacGoal _ -> VtStartProof ("Classic",GuaranteesOpacity,[]), VtLater
- | VernacFixpoint (_,_,l) ->
+ | VernacFixpoint (_,l) ->
let ids, open_proof =
List.fold_left (fun (l,b) (((_,id),_,_,_,p),_) ->
id::l, b || p = None) ([],false) l in
if open_proof
then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
else VtSideff ids, VtLater
- | VernacCoFixpoint (_,_,l) ->
+ | VernacCoFixpoint (_,l) ->
let ids, open_proof =
List.fold_left (fun (l,b) (((_,id),_,_,p),_) ->
id::l, b || p = None) ([],false) l in
@@ -144,7 +144,7 @@ let rec classify_vernac e =
let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map snd l) l) in
VtSideff ids, VtLater
| VernacDefinition (_,(_,id),DefineBody _) -> VtSideff [id], VtLater
- | VernacInductive (_,_,_,l) ->
+ | VernacInductive (_,_,l) ->
let ids = List.map (fun (((_,(_,id)),_,_,_,cl),_) -> id :: match cl with
| Constructors l -> List.map (fun (_,((_,id),_)) -> id) l
| RecordDecl (oid,l) -> (match oid with Some (_,x) -> [x] | _ -> []) @
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 40dfa1b9a5..a5e771d75d 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1856,6 +1856,7 @@ let vernac_load interp fname =
try while true do interp (snd (parse_sentence input)) done
with End_of_input -> ()
+let all_checks = { Declarations.check_guarded = true }
(* "locality" is the prefix "Local" attribute, while the "local" component
* is the outdated/deprecated "Local" attribute of some vernacular commands
@@ -1894,9 +1895,9 @@ let interp ?proof locality poly c =
| VernacEndProof e -> vernac_end_proof ?proof e
| VernacExactProof c -> vernac_exact_proof c
| VernacAssumption (stre,nl,l) -> vernac_assumption locality poly stre l nl
- | VernacInductive (chk,priv,finite,l) -> vernac_inductive chk poly priv finite l
- | VernacFixpoint (flags,local, l) -> vernac_fixpoint ~flags locality poly local l
- | VernacCoFixpoint (flags,local, l) -> vernac_cofixpoint ~flags locality poly local l
+ | VernacInductive (priv,finite,l) -> vernac_inductive true poly priv finite l
+ | VernacFixpoint (local, l) -> vernac_fixpoint locality ~flags:all_checks poly local l
+ | VernacCoFixpoint (local, l) -> vernac_cofixpoint ~flags:all_checks locality poly local l
| VernacScheme l -> vernac_scheme l
| VernacCombinedScheme (id, l) -> vernac_combined_scheme id l
| VernacUniverse l -> vernac_universe l
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:55:35 +0000