aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/cemitcodes.ml31
-rw-r--r--parsing/g_prim.ml45
-rw-r--r--parsing/g_vernac.ml42
-rw-r--r--parsing/pcoq.ml1
-rw-r--r--parsing/pcoq.mli1
-rw-r--r--tactics/class_tactics.ml12
-rw-r--r--test-suite/bugs/closed/4969.v11
-rw-r--r--test-suite/success/Notations.v7
-rw-r--r--tools/coq_makefile.ml1
-rw-r--r--vernac/metasyntax.ml16
10 files changed, 62 insertions, 25 deletions
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index f2c3b402b..40c1e027d 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -274,41 +274,44 @@ let emit_instr = function
| Kstop ->
out opSTOP
-(* Emission of a list of instructions. Include some peephole optimization. *)
+(* Emission of a current list and remaining lists of instructions. Include some peephole optimization. *)
-let rec emit = function
- | [] -> ()
+let rec emit insns remaining = match insns with
+ | [] ->
+ (match remaining with
+ [] -> ()
+ | (first::rest) -> emit first rest)
(* Peephole optimizations *)
| Kpush :: Kacc n :: c ->
if n < 8 then out(opPUSHACC0 + n) else (out opPUSHACC; out_int n);
- emit c
+ emit c remaining
| Kpush :: Kenvacc n :: c ->
if n >= 1 && n <= 4
then out(opPUSHENVACC1 + n - 1)
else (out opPUSHENVACC; out_int n);
- emit c
+ emit c remaining
| Kpush :: Koffsetclosure ofs :: c ->
if Int.equal ofs (-2) || Int.equal ofs 0 || Int.equal ofs 2
then out(opPUSHOFFSETCLOSURE0 + ofs / 2)
else (out opPUSHOFFSETCLOSURE; out_int ofs);
- emit c
+ emit c remaining
| Kpush :: Kgetglobal id :: c ->
- out opPUSHGETGLOBAL; slot_for_getglobal id; emit c
+ out opPUSHGETGLOBAL; slot_for_getglobal id; emit c remaining
| Kpush :: Kconst (Const_b0 i) :: c ->
if i >= 0 && i <= 3
then out (opPUSHCONST0 + i)
else (out opPUSHCONSTINT; out_int i);
- emit c
+ emit c remaining
| Kpush :: Kconst const :: c ->
out opPUSHGETGLOBAL; slot_for_const const;
- emit c
+ emit c remaining
| Kpop n :: Kjump :: c ->
- out opRETURN; out_int n; emit c
+ out opRETURN; out_int n; emit c remaining
| Ksequence(c1,c2)::c ->
- emit c1; emit c2;emit c
+ emit c1 (c2::c::remaining)
(* Default case *)
| instr :: c ->
- emit_instr instr; emit c
+ emit_instr instr; emit c remaining
(* Initialization *)
@@ -379,8 +382,8 @@ let repr_body_code = function
let to_memory (init_code, fun_code, fv) =
init();
- emit init_code;
- emit fun_code;
+ emit init_code [];
+ emit fun_code [];
(** Later uses of this string are all purely functional *)
let code = Bytes.sub_string !out_buffer 0 !out_position in
let code = CString.hcons code in
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 820514b08..2db91b8f8 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -34,7 +34,7 @@ GEXTEND Gram
GLOBAL:
bigint natural integer identref name ident var preident
fullyqualid qualid reference dirpath ne_lstring
- ne_string string pattern_ident pattern_identref by_notation smart_global;
+ ne_string string lstring pattern_ident pattern_identref by_notation smart_global;
preident:
[ [ s = IDENT -> s ] ]
;
@@ -106,6 +106,9 @@ GEXTEND Gram
string:
[ [ s = STRING -> s ] ]
;
+ lstring:
+ [ [ s = string -> (!@loc, s) ] ]
+ ;
integer:
[ [ i = INT -> my_int_of_string (!@loc) i
| "-"; i = INT -> - my_int_of_string (!@loc) i ] ]
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index d46880831..18807113c 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -1112,7 +1112,7 @@ GEXTEND Gram
idl = LIST0 ident; ":="; c = constr; b = only_parsing ->
VernacSyntacticDefinition
(id,(idl,c),local,b)
- | IDENT "Notation"; local = obsolete_locality; s = ne_lstring; ":=";
+ | IDENT "Notation"; local = obsolete_locality; s = lstring; ":=";
c = constr;
modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
sc = OPT [ ":"; sc = IDENT -> sc ] ->
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index c5823440a..b8405ca8c 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -267,6 +267,7 @@ module Prim =
let integer = gec_gen "integer"
let bigint = Gram.entry_create "Prim.bigint"
let string = gec_gen "string"
+ let lstring = Gram.entry_create "Prim.lstring"
let reference = make_gen_entry uprim "reference"
let by_notation = Gram.entry_create "by_notation"
let smart_global = Gram.entry_create "smart_global"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index d987bb455..cf5174af9 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -136,6 +136,7 @@ module Prim :
val bigint : Bigint.bigint Gram.entry
val integer : int Gram.entry
val string : string Gram.entry
+ val lstring : string located Gram.entry
val qualid : qualid located Gram.entry
val fullyqualid : Id.t list located Gram.entry
val reference : reference Gram.entry
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index a85afcbf0..edfe21d34 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1613,10 +1613,16 @@ let is_ground c gl =
else tclFAIL 0 (str"Not ground") gl
let autoapply c i gl =
+ let open Proofview.Notations in
let flags = auto_unif_flags Evar.Set.empty
(Hints.Hint_db.transparent_state (Hints.searchtable_map i)) in
let cty = pf_unsafe_type_of gl c in
let ce = mk_clenv_from gl (c,cty) in
- let tac = { enter = fun gl -> (unify_e_resolve false flags).enter gl
- ((c,cty,Univ.ContextSet.empty),0,ce) } in
- Proofview.V82.of_tactic (Proofview.Goal.nf_enter tac) gl
+ let enter gl =
+ (unify_e_resolve false flags).enter gl
+ ((c,cty,Univ.ContextSet.empty),0,ce) <*>
+ Proofview.tclEVARMAP >>= (fun sigma ->
+ let sigma = Typeclasses.mark_unresolvables ~filter:Typeclasses.all_goals sigma in
+ Proofview.Unsafe.tclEVARS sigma)
+ in
+ Proofview.V82.of_tactic (Proofview.Goal.nf_enter { enter }) gl
diff --git a/test-suite/bugs/closed/4969.v b/test-suite/bugs/closed/4969.v
new file mode 100644
index 000000000..4dee41e22
--- /dev/null
+++ b/test-suite/bugs/closed/4969.v
@@ -0,0 +1,11 @@
+Require Import Classes.Init.
+
+Class C A := c : A.
+Instance nat_C : C nat := 0.
+Instance bool_C : C bool := true.
+Lemma silly {A} `{C A} : 0 = 0 -> c = c -> True.
+Proof. auto. Qed.
+
+Goal True.
+ class_apply @silly; [reflexivity|].
+ reflexivity. Fail Qed.
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 07bbb60c4..52acad746 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -128,3 +128,10 @@ Notation " |- {{ a }} b" := (a=b) (no associativity, at level 10).
Goal True.
{{ exact I. }}
Qed.
+
+(* Check that we can have notations without any symbol iff they are "only printing". *)
+Fail Notation "" := (@nil).
+Notation "" := (@nil) (only printing).
+
+(* Check that a notation cannot be neither parsing nor printing. *)
+Fail Notation "'foobarkeyword'" := (@nil) (only parsing, only printing).
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 4dfb7af6a..22b1408c0 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -673,6 +673,7 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other
print "VO=vo\n";
print "VOFILES:=$(VFILES:.v=.$(VO))\n";
classify_files_by_root "VOFILES" l inc;
+ classify_files_by_root "VFILES" l inc;
print "GLOBFILES:=$(VFILES:.v=.glob)\n";
print "GFILES:=$(VFILES:.v=.g)\n";
print "HTMLFILES:=$(VFILES:.v=.html)\n";
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 0aaf6afd7..7e98d114a 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -932,8 +932,8 @@ let find_precedence lev etyps symbols =
let first_symbol =
let rec aux = function
| Break _ :: t -> aux t
- | h :: t -> h
- | [] -> assert false (* rule is known to be productive *) in
+ | h :: t -> Some h
+ | [] -> None in
aux symbols in
let last_is_terminal () =
let rec aux b = function
@@ -943,7 +943,8 @@ let find_precedence lev etyps symbols =
| [] -> b in
aux false symbols in
match first_symbol with
- | NonTerminal x ->
+ | None -> [],0
+ | Some (NonTerminal x) ->
(try match List.assoc x etyps with
| ETConstr _ ->
error "The level of the leftmost non-terminal cannot be changed."
@@ -966,11 +967,11 @@ let find_precedence lev etyps symbols =
if Option.is_empty lev then
error "A left-recursive notation must have an explicit level."
else [],Option.get lev)
- | Terminal _ when last_is_terminal () ->
+ | Some (Terminal _) when last_is_terminal () ->
if Option.is_empty lev then
([Feedback.msg_info ?loc:None ,strbrk "Setting notation at level 0."], 0)
else [],Option.get lev
- | _ ->
+ | Some _ ->
if Option.is_empty lev then error "Cannot determine the level.";
[],Option.get lev
@@ -1049,6 +1050,9 @@ let compute_syntax_data df modifiers =
let open SynData in
let open NotationMods in
let mods = interp_modifiers modifiers in
+ let onlyprint = mods.only_printing in
+ let onlyparse = mods.only_parsing in
+ if onlyprint && onlyparse then error "A notation cannot be both 'only printing' and 'only parsing'.";
let assoc = Option.append mods.assoc (Some NonA) in
let toks = split_notation_string df in
let recvars,mainvars,symbols = analyze_notation_tokens toks in
@@ -1058,7 +1062,7 @@ let compute_syntax_data df modifiers =
let ntn_for_interp = make_notation_key symbols in
let symbols' = remove_curly_brackets symbols in
let ntn_for_grammar = make_notation_key symbols' in
- check_rule_productivity symbols';
+ if not onlyprint then check_rule_productivity symbols';
(* Misc *)
let need_squash = not (List.equal Notation.symbol_eq symbols symbols') in
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-07 13:15:53 +0000