diff options
Diffstat (limited to 'theories/Init/SpecifSyntax.v')
| -rw-r--r-- | theories/Init/SpecifSyntax.v | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/theories/Init/SpecifSyntax.v b/theories/Init/SpecifSyntax.v index 431f44fb78..3aadaaec73 100644 --- a/theories/Init/SpecifSyntax.v +++ b/theories/Init/SpecifSyntax.v @@ -11,7 +11,7 @@ Require LogicSyntax. Require Specif. -(* Parsing of things in Specif.v *) +(** Parsing of things in Specif.v *) Grammar constr constr1 := sig [ "{" lconstr($lc) ":" lconstr($c1) "|" lconstr($c2) "}" ] @@ -43,10 +43,10 @@ Grammar constr lassoc_constr4 := | $_ -> [ (sum $c1 $c2) ] (* c1+c2 *) esac. -(* Pretty-printing of things in Specif.v *) +(** Pretty-printing of things in Specif.v *) Syntax constr - (* Default pretty-printing rules *) +(** Default pretty-printing rules *) level 10: sig_var [<<(ABSTR_B_NB $c1 $c2)>>] -> [ [<hov 0> "sig " $c1:L [1 1] $c2:L ] ] @@ -60,14 +60,14 @@ Syntax constr ; level 1: -(* Pretty-printing of [sig] *) +(** Pretty-printing of [sig] *) sig [ (sig $c1 $c2) ] -> [ (ABSTR_B_NB $c1 $c2):E ] | sig_nb [ << (ABSTR_B_NB $c1 (LAMBDALIST $c1 [<>]$c2)) >> ] -> [ [<hov 0> "{_:" $c1:E " |" [1 3] $c2:E "}" ] ] | sigma_b [ << (ABSTR_B_NB $c1 (LAMBDALIST $c1 [$id]$c2)) >> ] -> [ [<hov 0> "{" $id ":" $c1:E " |" [1 3] $c2:E "}" ] ] -(* Pretty-printing of [sig2] *) +(** Pretty-printing of [sig2] *) | sig2 [ (sig2 $c1 $c2 $c3) ] -> [ (Sig2_ABSTR_B_NB $c1 $c2 $c3):E ] | sig2_b_b [ << (Sig2_ABSTR_B_NB $c1 (LAMBDALIST $c1 [$id]$c2) @@ -86,14 +86,14 @@ Syntax constr (LAMBDALIST $c1 [<>]$c3)) >> ] -> [ [<hov 0> "{_:"$c1:E "|" [1 3] $c2:E [1 3]"& " $c3:E "}" ] ] -(* Pretty-printing of [sigS] *) +(** Pretty-printing of [sigS] *) | sigS [ (sigS $c1 $c2) ] -> [(SigS_ABSTR_B_NB $c1 $c2):E] | sigS_nb [ << (SigS_ABSTR_B_NB $c1 (LAMBDALIST $c1 [<>]$c2)) >> ] -> [ [<hov 0> "{_:" $c1:E [1 3]"& " $c2:E "}" ] ] | sigS_b [ << (SigS_ABSTR_B_NB $c1 (LAMBDALIST $c1 [$id]$c2)) >> ] -> [ [<hov 0> "{" $id ":" $c1:E [1 3] "& " $c2:E "}" ] ] -(* Pretty-printing of [sigS2] *) +(** Pretty-printing of [sigS2] *) | sigS2 [ (sigS2 $c1 $c2 $c3) ] -> [(SigS2_ABSTR_B_NB $c1 $c2 $c3):E] | sigS2_b_b [ << (SigS2_ABSTR_B_NB $c1 (LAMBDALIST $c1 [$id]$c2) @@ -112,12 +112,12 @@ Syntax constr (LAMBDALIST $c1 [<>]$c3)) >> ] -> [ [<hov 0> "{_:"$c1:E [1 3]"& "$c2:E [1 3]"& "$c3:E "}" ] ] -(* Pretty-printing of [projS1] and [projS2] *) +(** Pretty-printing of [projS1] and [projS2] *) | projS1_imp [ (projS1 ? ? $a) ] -> ["(ProjS1 " $a:E ")"] | projS2_imp [ (projS2 ? ? $a) ] -> ["(ProjS2 " $a:E ")"] ; -(* Pretty-printing of [sumbool] and [sumor] *) +(** Pretty-printing of [sumbool] and [sumor] *) level 4: sumbool [ (sumbool $t1 $t2) ] -> [ [<hov 0> "{" $t1:E "}" [0 1] "+" "{" $t2:L "}"] ] @@ -125,11 +125,11 @@ Syntax constr -> [ [<hov 0> $t1:E [0 1] "+" "{" $t2:L "}"] ] ; -(* Pretty-printing of [except] *) +(** Pretty-printing of [except] *) level 1: Except_imp [ (except $1 $t2) ] -> [ [<hov 0> "Except " $t2 ] ] -(* Pretty-printing of [error] and [value] *) +(** Pretty-printing of [error] and [value] *) | Error_imp [ (error $t1) ] -> [ [<hov 0> "Error" ] ] | Value_imp [ (value $t1 $t2) ] -> [ [<hov 0> "(Value " $t2 ")" ] ]. |