diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/Makefile | 4 | ||||
| -rw-r--r-- | test-suite/bugs/closed/5761.v | 126 | ||||
| -rw-r--r-- | test-suite/bugs/closed/5762.v | 6 | ||||
| -rw-r--r-- | test-suite/bugs/closed/6129.v | 9 | ||||
| -rw-r--r-- | test-suite/coqdoc/bug5648.html.out | 18 | ||||
| -rw-r--r-- | test-suite/coqdoc/bug5648.tex.out | 12 | ||||
| -rw-r--r-- | test-suite/coqdoc/bug5700.html.out | 2 | ||||
| -rw-r--r-- | test-suite/coqdoc/bug5700.tex.out | 12 | ||||
| -rw-r--r-- | test-suite/coqdoc/links.html.out | 8 | ||||
| -rw-r--r-- | test-suite/coqdoc/links.tex.out | 14 | ||||
| -rw-r--r-- | test-suite/success/Notations2.v | 6 |
11 files changed, 197 insertions, 20 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 61e75fa5d..7a204bfd8 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -549,8 +549,8 @@ $(addsuffix .log,$(wildcard coqdoc/*.v)): %.v.log: %.v %.html.out %.tex.out $(PR $(coqc) -R coqdoc Coqdoc $* 2>&1; \ cd coqdoc; \ f=`basename $*`; \ - $(coqdoc) -R . Coqdoc -coqlib http://coq.inria.fr/stdlib --html $$f.v; \ - $(coqdoc) -R . Coqdoc -coqlib http://coq.inria.fr/stdlib --latex $$f.v; \ + $(coqdoc) -utf8 -R . Coqdoc -coqlib http://coq.inria.fr/stdlib --html $$f.v; \ + $(coqdoc) -utf8 -R . Coqdoc -coqlib http://coq.inria.fr/stdlib --latex $$f.v; \ diff -u --strip-trailing-cr $$f.html.out Coqdoc.$$f.html 2>&1; R=$$?; times; \ grep -v "^%%" Coqdoc.$$f.tex | diff -u --strip-trailing-cr $$f.tex.out - 2>&1; S=$$?; times; \ if [ $$R = 0 -a $$S = 0 ]; then \ diff --git a/test-suite/bugs/closed/5761.v b/test-suite/bugs/closed/5761.v new file mode 100644 index 000000000..6f28d1981 --- /dev/null +++ b/test-suite/bugs/closed/5761.v @@ -0,0 +1,126 @@ +Set Primitive Projections. +Record mix := { a : nat ; b : a = a ; c : nat ; d : a = c ; e : nat ; f : nat }. +Ltac strip_args T ctor := + lazymatch type of ctor with + | context[T] + => match eval cbv beta in ctor with + | ?ctor _ => strip_args T ctor + | _ => ctor + end + end. +Ltac get_ctor T := + let full_ctor := constr:(ltac:(let x := fresh in intro x; econstructor; apply +x) : T -> T) in + let ctor := constr:(fun x : T => ltac:(let v := strip_args T (full_ctor x) in +exact v)) in + lazymatch ctor with + | fun _ => ?ctor => ctor + end. +Ltac uncurry_domain f := + lazymatch type of f with + | forall (a : ?A) (b : @ ?B a), _ + => uncurry_domain (fun ab : { a : A & B a } => f (projT1 ab) (projT2 ab)) + | _ => eval cbv beta in f + end. +Ltac get_of_sigma T := + let ctor := get_ctor T in + uncurry_domain ctor. +Ltac repeat_existT := + lazymatch goal with + | [ |- sigT _ ] => simple refine (existT _ _ _); [ repeat_existT | shelve ] + | _ => shelve + end. + Ltac prove_to_of_sigma_goal of_sigma := + let v := fresh "v" in + simple refine (exist _ _ (fun v => _ : id _ (of_sigma v) = v)); + try unfold of_sigma; + [ intro v; destruct v; repeat_existT + | cbv beta; + repeat match goal with + | [ |- context[projT2 ?k] ] + => let x := fresh "x" in + is_var k; + destruct k as [k x]; cbn [projT1 projT2] + end; + unfold id; reflexivity ]. +Ltac prove_to_of_sigma of_sigma := + constr:( + ltac:(prove_to_of_sigma_goal of_sigma) + : { to_sigma : _ | forall v, id to_sigma (of_sigma v) = v }). +Ltac get_to_sigma_gen of_sigma := + let v := prove_to_of_sigma of_sigma in + eval hnf in (proj1_sig v). +Ltac get_to_sigma T := + let of_sigma := get_of_sigma T in + get_to_sigma_gen of_sigma. +Definition to_sigma := ltac:(let v := get_to_sigma mix in exact v). +(* Error: +In nested Ltac calls to "get_to_sigma", "get_to_sigma_gen", +"prove_to_of_sigma", +"(_ : {to_sigma : _ | forall v, id to_sigma (of_sigma v) = v})" (with +of_sigma:=fun + ab : {_ + : {_ + : {ab : {_ : {a : nat & a = a} & nat} & + projT1 (projT1 ab) = projT2 ab} & nat} & nat} => + {| + a := projT1 (projT1 (projT1 (projT1 (projT1 ab)))); + b := projT2 (projT1 (projT1 (projT1 (projT1 ab)))); + c := projT2 (projT1 (projT1 (projT1 ab))); + d := projT2 (projT1 (projT1 ab)); + e := projT2 (projT1 ab); + f := projT2 ab |}) and "prove_to_of_sigma_goal", last call failed. +Anomaly "Uncaught exception Not_found." Please report at +http://coq.inria.fr/bugs/. +frame @ file "toplevel/coqtop.ml", line 640, characters 6-22 +frame @ file "list.ml", line 73, characters 12-15 +frame @ file "toplevel/vernac.ml", line 344, characters 2-13 +frame @ file "toplevel/vernac.ml", line 308, characters 14-75 +raise @ file "lib/exninfo.ml", line 63, characters 8-15 +frame @ file "lib/flags.ml", line 141, characters 19-40 +raise @ file "lib/exninfo.ml", line 63, characters 8-15 +frame @ file "lib/flags.ml", line 11, characters 15-18 +raise @ file "lib/exninfo.ml", line 63, characters 8-15 +frame @ file "toplevel/vernac.ml", line 167, characters 6-16 +frame @ file "toplevel/vernac.ml", line 151, characters 26-39 +frame @ file "stm/stm.ml", line 2365, characters 2-35 +raise @ file "lib/exninfo.ml", line 63, characters 8-15 +frame @ file "stm/stm.ml", line 2355, characters 4-48 +frame @ file "stm/stm.ml", line 2321, characters 4-100 +raise @ file "lib/exninfo.ml", line 63, characters 8-15 +frame @ file "stm/stm.ml", line 832, characters 6-10 +frame @ file "stm/stm.ml", line 2206, characters 10-32 +raise @ file "lib/exninfo.ml", line 63, characters 8-15 +frame @ file "stm/stm.ml", line 975, characters 8-81 +raise @ file "lib/exninfo.ml", line 63, characters 8-15 +frame @ file "vernac/vernacentries.ml", line 2216, characters 10-389 +frame @ file "lib/flags.ml", line 141, characters 19-40 +raise @ file "lib/exninfo.ml", line 63, characters 8-15 +frame @ file "lib/flags.ml", line 11, characters 15-18 +frame @ file "vernac/command.ml", line 150, characters 4-56 +frame @ file "interp/constrintern.ml", line 2046, characters 2-73 +frame @ file "pretyping/pretyping.ml", line 1194, characters 19-77 +frame @ file "pretyping/pretyping.ml", line 1155, characters 8-72 +frame @ file "pretyping/pretyping.ml", line 628, characters 23-65 +frame @ file "plugins/ltac/tacinterp.ml", line 2095, characters 21-61 +frame @ file "proofs/pfedit.ml", line 178, characters 6-22 +raise @ file "lib/exninfo.ml", line 63, characters 8-15 +frame @ file "proofs/pfedit.ml", line 174, characters 8-36 +frame @ file "proofs/proof.ml", line 351, characters 4-30 +raise @ file "lib/exninfo.ml", line 63, characters 8-15 +frame @ file "engine/proofview.ml", line 1222, characters 8-12 +frame @ file "plugins/ltac/tacinterp.ml", line 2020, characters 19-36 +frame @ file "plugins/ltac/tacinterp.ml", line 618, characters 4-70 +raise @ file "lib/exninfo.ml", line 63, characters 8-15 +frame @ file "plugins/ltac/tacinterp.ml", line 214, characters 6-9 +frame @ file "pretyping/pretyping.ml", line 1198, characters 19-62 +frame @ file "pretyping/pretyping.ml", line 1155, characters 8-72 +raise @ unknown +frame @ file "pretyping/pretyping.ml", line 628, characters 23-65 +frame @ file "plugins/ltac/tacinterp.ml", line 2095, characters 21-61 +frame @ file "proofs/pfedit.ml", line 178, characters 6-22 +raise @ file "lib/exninfo.ml", line 63, characters 8-15 +frame @ file "proofs/pfedit.ml", line 174, characters 8-36 +frame @ file "proofs/proof.ml", line 351, characters 4-30 +raise @ file "lib/exninfo.ml", line 63, characters 8-15 + *) diff --git a/test-suite/bugs/closed/5762.v b/test-suite/bugs/closed/5762.v index edd5c8d73..55d36bd72 100644 --- a/test-suite/bugs/closed/5762.v +++ b/test-suite/bugs/closed/5762.v @@ -26,3 +26,9 @@ Reserved Notation "%% a" (at level 70). Record R := {g : forall {A} (a:A), a=a where "%% x" := (g x); k : %% 0 = eq_refl}. + +(* An extra example *) + +Module A. +Inductive I {A:Type} := C : # 0 -> I where "# I" := (I = I) : I_scope. +End A. diff --git a/test-suite/bugs/closed/6129.v b/test-suite/bugs/closed/6129.v new file mode 100644 index 000000000..e4a2a2ba9 --- /dev/null +++ b/test-suite/bugs/closed/6129.v @@ -0,0 +1,9 @@ +(* Make definition of coercions compatible with local definitions. *) + +Record foo (x : Type) (y:=1) := { foo_nat :> nat }. +Record foo2 (x : Type) (y:=1) (z t: Type) := { foo_nat2 :> nat }. +Record foo3 (y:=1) (z t: Type) := { foo_nat3 :> nat }. + +Check fun x : foo nat => x + 1. +Check fun x : foo2 nat nat nat => x + 1. +Check fun x : foo3 nat nat => x + 1. diff --git a/test-suite/coqdoc/bug5648.html.out b/test-suite/coqdoc/bug5648.html.out index 06789c1c1..5c5a2dc29 100644 --- a/test-suite/coqdoc/bug5648.html.out +++ b/test-suite/coqdoc/bug5648.html.out @@ -2,7 +2,7 @@ "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> <html xmlns="http://www.w3.org/1999/xhtml"> <head> -<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1" /> +<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> <link href="coqdoc.css" rel="stylesheet" type="text/css" /> <title>Coqdoc.bug5648</title> </head> @@ -31,14 +31,14 @@ <br/> <span class="id" title="keyword">Definition</span> <a name="d"><span class="id" title="definition">d</span></a> <span class="id" title="var">x</span> :=<br/> <span class="id" title="keyword">match</span> <a class="idref" href="Coqdoc.bug5648.html#x"><span class="id" title="variable">x</span></a> <span class="id" title="keyword">with</span><br/> - | <a class="idref" href="Coqdoc.bug5648.html#A"><span class="id" title="constructor">A</span></a> => 0<br/> - | <a class="idref" href="Coqdoc.bug5648.html#Add"><span class="id" title="constructor">Add</span></a> => 1<br/> - | <a class="idref" href="Coqdoc.bug5648.html#G"><span class="id" title="constructor">G</span></a> => 2<br/> - | <a class="idref" href="Coqdoc.bug5648.html#Goal"><span class="id" title="constructor">Goal</span></a> => 3<br/> - | <a class="idref" href="Coqdoc.bug5648.html#L"><span class="id" title="constructor">L</span></a> => 4<br/> - | <a class="idref" href="Coqdoc.bug5648.html#Lemma"><span class="id" title="constructor">Lemma</span></a> => 5<br/> - | <a class="idref" href="Coqdoc.bug5648.html#P"><span class="id" title="constructor">P</span></a> => 6<br/> - | <a class="idref" href="Coqdoc.bug5648.html#Proof"><span class="id" title="constructor">Proof</span></a> => 7<br/> + | <a class="idref" href="Coqdoc.bug5648.html#A"><span class="id" title="constructor">A</span></a> ⇒ 0<br/> + | <a class="idref" href="Coqdoc.bug5648.html#Add"><span class="id" title="constructor">Add</span></a> ⇒ 1<br/> + | <a class="idref" href="Coqdoc.bug5648.html#G"><span class="id" title="constructor">G</span></a> ⇒ 2<br/> + | <a class="idref" href="Coqdoc.bug5648.html#Goal"><span class="id" title="constructor">Goal</span></a> ⇒ 3<br/> + | <a class="idref" href="Coqdoc.bug5648.html#L"><span class="id" title="constructor">L</span></a> ⇒ 4<br/> + | <a class="idref" href="Coqdoc.bug5648.html#Lemma"><span class="id" title="constructor">Lemma</span></a> ⇒ 5<br/> + | <a class="idref" href="Coqdoc.bug5648.html#P"><span class="id" title="constructor">P</span></a> ⇒ 6<br/> + | <a class="idref" href="Coqdoc.bug5648.html#Proof"><span class="id" title="constructor">Proof</span></a> ⇒ 7<br/> <span class="id" title="keyword">end</span>.<br/> </div> </div> diff --git a/test-suite/coqdoc/bug5648.tex.out b/test-suite/coqdoc/bug5648.tex.out index b0b732eff..82f7da230 100644 --- a/test-suite/coqdoc/bug5648.tex.out +++ b/test-suite/coqdoc/bug5648.tex.out @@ -1,5 +1,15 @@ \documentclass[12pt]{report} -\usepackage[]{inputenc} +\usepackage[utf8x]{inputenc} + +%Warning: tipa declares many non-standard macros used by utf8x to +%interpret utf8 characters but extra packages might have to be added +%such as "textgreek" for Greek letters not already in tipa +%or "stmaryrd" for mathematical symbols. +%Utf8 codes missing a LaTeX interpretation can be defined by using +%\DeclareUnicodeCharacter{code}{interpretation}. +%Use coqdoc's option -p to add new packages or declarations. +\usepackage{tipa} + \usepackage[T1]{fontenc} \usepackage{fullpage} \usepackage{coqdoc} diff --git a/test-suite/coqdoc/bug5700.html.out b/test-suite/coqdoc/bug5700.html.out index 0e05660d6..b96fc6281 100644 --- a/test-suite/coqdoc/bug5700.html.out +++ b/test-suite/coqdoc/bug5700.html.out @@ -2,7 +2,7 @@ "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> <html xmlns="http://www.w3.org/1999/xhtml"> <head> -<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1" /> +<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> <link href="coqdoc.css" rel="stylesheet" type="text/css" /> <title>Coqdoc.bug5700</title> </head> diff --git a/test-suite/coqdoc/bug5700.tex.out b/test-suite/coqdoc/bug5700.tex.out index 33990cb89..1a1af5dfd 100644 --- a/test-suite/coqdoc/bug5700.tex.out +++ b/test-suite/coqdoc/bug5700.tex.out @@ -1,5 +1,15 @@ \documentclass[12pt]{report} -\usepackage[]{inputenc} +\usepackage[utf8x]{inputenc} + +%Warning: tipa declares many non-standard macros used by utf8x to +%interpret utf8 characters but extra packages might have to be added +%such as "textgreek" for Greek letters not already in tipa +%or "stmaryrd" for mathematical symbols. +%Utf8 codes missing a LaTeX interpretation can be defined by using +%\DeclareUnicodeCharacter{code}{interpretation}. +%Use coqdoc's option -p to add new packages or declarations. +\usepackage{tipa} + \usepackage[T1]{fontenc} \usepackage{fullpage} \usepackage{coqdoc} diff --git a/test-suite/coqdoc/links.html.out b/test-suite/coqdoc/links.html.out index e2928f78d..5e4b676c2 100644 --- a/test-suite/coqdoc/links.html.out +++ b/test-suite/coqdoc/links.html.out @@ -2,7 +2,7 @@ "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> <html xmlns="http://www.w3.org/1999/xhtml"> <head> -<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1" /> +<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> <link href="coqdoc.css" rel="stylesheet" type="text/css" /> <title>Coqdoc.links</title> </head> @@ -57,7 +57,7 @@ Various checks for coqdoc <span class="id" title="keyword">Definition</span> <a name="a"><span class="id" title="definition">a</span></a> (<span class="id" title="var">b</span>: <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) := <a class="idref" href="Coqdoc.links.html#b"><span class="id" title="variable">b</span></a>.<br/> <br/> -<span class="id" title="keyword">Definition</span> <a name="f"><span class="id" title="definition">f</span></a> := <span class="id" title="keyword">forall</span> <span class="id" title="var">C</span>:<span class="id" title="keyword">Prop</span>, <a class="idref" href="Coqdoc.links.html#C"><span class="id" title="variable">C</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="f"><span class="id" title="definition">f</span></a> := <span class="id" title="keyword">∀</span> <span class="id" title="var">C</span>:<span class="id" title="keyword">Prop</span>, <a class="idref" href="Coqdoc.links.html#C"><span class="id" title="variable">C</span></a>.<br/> <br/> <span class="id" title="keyword">Notation</span> <a name="1a1c7f13320341c3638e9edcc3e6389d"><span class="id" title="notation">"</span></a>n ++ m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>).<br/> @@ -74,9 +74,9 @@ Various checks for coqdoc <span class="id" title="keyword">Notation</span> <a name="347f39a83bf7d45676cff54fd7e8966f"><span class="id" title="notation">"</span></a>n '_' ++ 'x' m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 3).<br/> <br/> -<span class="id" title="keyword">Inductive</span> <a name="eq"><span class="id" title="inductive">eq</span></a> (<span class="id" title="var">A</span>:<span class="id" title="keyword">Type</span>) (<span class="id" title="var">x</span>:<a class="idref" href="Coqdoc.links.html#A"><span class="id" title="variable">A</span></a>) : <span class="id" title="var">A</span> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">-></span></a> <span class="id" title="keyword">Prop</span> := <a name="eq_refl"><span class="id" title="constructor">eq_refl</span></a> : <a class="idref" href="Coqdoc.links.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">=</span></a> <a class="idref" href="Coqdoc.links.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">:></span></a><a class="idref" href="Coqdoc.links.html#A"><span class="id" title="variable">A</span></a><br/> +<span class="id" title="keyword">Inductive</span> <a name="eq"><span class="id" title="inductive">eq</span></a> (<span class="id" title="var">A</span>:<span class="id" title="keyword">Type</span>) (<span class="id" title="var">x</span>:<a class="idref" href="Coqdoc.links.html#A"><span class="id" title="variable">A</span></a>) : <span class="id" title="var">A</span> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span> := <a name="eq_refl"><span class="id" title="constructor">eq_refl</span></a> : <a class="idref" href="Coqdoc.links.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">=</span></a> <a class="idref" href="Coqdoc.links.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">:></span></a><a class="idref" href="Coqdoc.links.html#A"><span class="id" title="variable">A</span></a><br/> <br/> -<span class="id" title="keyword">where</span> <a name="8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">"</span></a>x = y :> A" := (@<a class="idref" href="Coqdoc.links.html#eq"><span class="id" title="inductive">eq</span></a> <a class="idref" href="Coqdoc.links.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="Coqdoc.links.html#x"><span class="id" title="variable">x</span></a> <span class="id" title="var">y</span>) : <span class="id" title="var">type_scope</span>.<br/> +<span class="id" title="keyword">where</span> <a name="8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">"</span></a>x = y :> A" := (@<a class="idref" href="Coqdoc.links.html#eq"><span class="id" title="inductive">eq</span></a> <span class="id" title="var">A</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>) : <span class="id" title="var">type_scope</span>.<br/> <br/> <span class="id" title="keyword">Definition</span> <a name="eq0"><span class="id" title="definition">eq0</span></a> := 0 <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">=</span></a> 0 <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">:></span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/> diff --git a/test-suite/coqdoc/links.tex.out b/test-suite/coqdoc/links.tex.out index de3182d1a..f42db99dc 100644 --- a/test-suite/coqdoc/links.tex.out +++ b/test-suite/coqdoc/links.tex.out @@ -1,5 +1,15 @@ \documentclass[12pt]{report} -\usepackage[]{inputenc} +\usepackage[utf8x]{inputenc} + +%Warning: tipa declares many non-standard macros used by utf8x to +%interpret utf8 characters but extra packages might have to be added +%such as "textgreek" for Greek letters not already in tipa +%or "stmaryrd" for mathematical symbols. +%Utf8 codes missing a LaTeX interpretation can be defined by using +%\DeclareUnicodeCharacter{code}{interpretation}. +%Use coqdoc's option -p to add new packages or declarations. +\usepackage{tipa} + \usepackage[T1]{fontenc} \usepackage{fullpage} \usepackage{coqdoc} @@ -59,7 +69,7 @@ Various checks for coqdoc \coqdocnoindent \coqdoceol \coqdocnoindent -\coqdockw{where} \coqdef{Coqdoc.links.:type scope:x '=' x ':>' x}{"}{"}x = y :> A" := (@\coqref{Coqdoc.links.eq}{\coqdocinductive{eq}} \coqdocvariable{A} \coqdocvariable{x} \coqdocvar{y}) : \coqdocvar{type\_scope}.\coqdoceol +\coqdockw{where} \coqdef{Coqdoc.links.:type scope:x '=' x ':>' x}{"}{"}x = y :> A" := (@\coqref{Coqdoc.links.eq}{\coqdocinductive{eq}} \coqdocvar{A} \coqdocvar{x} \coqdocvar{y}) : \coqdocvar{type\_scope}.\coqdoceol \coqdocemptyline \coqdocnoindent \coqdockw{Definition} \coqdef{Coqdoc.links.eq0}{eq0}{\coqdocdefinition{eq0}} := 0 \coqref{Coqdoc.links.:type scope:x '=' x ':>' x}{\coqdocnotation{=}} 0 \coqref{Coqdoc.links.:type scope:x '=' x ':>' x}{\coqdocnotation{:>}} \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v index 9505a56e3..e86b3edb8 100644 --- a/test-suite/success/Notations2.v +++ b/test-suite/success/Notations2.v @@ -90,3 +90,9 @@ Check fun A (x :prod' bool A) => match x with #### 0 y 0 => 2 | _ => 1 end. Notation "##### x" := (pair' x) (at level 0, x at level 1). Check ##### 0 _ 0%bool 0%bool : prod' bool bool. Check fun A (x :prod' bool A) => match x with ##### 0 _ y 0%bool => 2 | _ => 1 end. + +(* 10. Check computation of binding variable through other notations *) +(* i should be detected as binding variable and the scopes not being checked *) + +Notation "'FUNNAT' i => t" := (fun i : nat => i = t) (at level 200). +Notation "'Funnat' i => t" := (FUNNAT i => t + i%nat) (at level 200). |