package coq-core

You can search for identifiers within the package.

in-package search v0.2.0

The Coq Proof Assistant -- Core Binaries and Tools

Install

Dune Dependency

coq.inria.fr Readme Edit opam file Versions (9)

Authors

T

The Coq development team, INRIA, CNRS, and contributors

Maintainers

T

The Coq development team <coqdev@inria.fr>

Sources

coq-8.20.1.tar.gz

md5=0cfaa70f569be9494d24c829e6555d46

sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2

doc/src/ltac2_ltac1_plugin/g_ltac2_ltac1.ml.html

Source file `g_ltac2_ltac1.ml`

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
let _ = Mltop.add_known_module "coq-core.plugins.ltac2_ltac1"

# 13 "plugins/ltac2_ltac1/g_ltac2_ltac1.mlg"
 

open Pcoq.Prim
open Ltac2_plugin
open Tac2expr
open Ltac_plugin
open Ltac2_plugin.G_ltac2

let ltac_expr = Pltac.ltac_expr

let inj_wit wit loc x = CAst.make ~loc @@ CTacExt (wit, x)

let inj_ltac1 loc e = inj_wit Tac2quote_ltac1.wit_ltac1 loc e
let inj_ltac1val loc e = inj_wit Tac2quote_ltac1.wit_ltac1val loc e



let _ = let ltac1_expr_in_env = Pcoq.Entry.make "ltac1_expr_in_env"
        in
        let () =
        Egramml.grammar_extend ~plugin_uid:("coq-core.plugins.ltac2_ltac1", "g_ltac2_ltac1.mlg:0")
        ltac2_atom
        (Pcoq.Reuse (None, [Pcoq.Production.make
                            (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.next 
                                                            (Pcoq.Rule.next 
                                                            (Pcoq.Rule.next 
                                                            (Pcoq.Rule.stop)
                                                            ((Pcoq.Symbol.token (Tok.PIDENT (Some
                                                            ("ltac1val"))))))
                                                            ((Pcoq.Symbol.token (Tok.PKEYWORD (":")))))
                                                            ((Pcoq.Symbol.token (Tok.PKEYWORD ("(")))))
                                                            ((Pcoq.Symbol.nterm ltac1_expr_in_env)))
                                            ((Pcoq.Symbol.token (Tok.PKEYWORD (")")))))
                            (fun _ qid _ _ _ loc -> 
# 34 "plugins/ltac2_ltac1/g_ltac2_ltac1.mlg"
                                                                    inj_ltac1val loc qid 
                                                    );
                           Pcoq.Production.make
                           (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.next 
                                                           (Pcoq.Rule.next 
                                                           (Pcoq.Rule.next 
                                                           (Pcoq.Rule.stop)
                                                           ((Pcoq.Symbol.token (Tok.PIDENT (Some
                                                           ("ltac1"))))))
                                                           ((Pcoq.Symbol.token (Tok.PKEYWORD (":")))))
                                                           ((Pcoq.Symbol.token (Tok.PKEYWORD ("(")))))
                                                           ((Pcoq.Symbol.nterm ltac1_expr_in_env)))
                                           ((Pcoq.Symbol.token (Tok.PKEYWORD (")")))))
                           (fun _ qid _ _ _ loc -> 
# 33 "plugins/ltac2_ltac1/g_ltac2_ltac1.mlg"
                                                                 inj_ltac1 loc qid 
                                                   )]))
        in let () = assert (Pcoq.Entry.is_empty ltac1_expr_in_env) in
        let () =
        Egramml.grammar_extend ~plugin_uid:("coq-core.plugins.ltac2_ltac1", "g_ltac2_ltac1.mlg:1")
        ltac1_expr_in_env
        (Pcoq.Fresh
        (Gramlib.Gramext.First, [(None, None,
                                 [Pcoq.Production.make
                                  (Pcoq.Rule.next (Pcoq.Rule.stop)
                                                  ((Pcoq.Symbol.nterm ltac_expr)))
                                  (fun e loc -> 
# 38 "plugins/ltac2_ltac1/g_ltac2_ltac1.mlg"
                           [], e 
                                                );
                                 Pcoq.Production.make
                                 (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.next 
                                                                 (Pcoq.Rule.next 
                                                                 (Pcoq.Rule.stop)
                                                                 ((Pcoq.Symbol.nterm test_ltac1_env)))
                                                                 ((Pcoq.Symbol.list0 (Pcoq.Symbol.nterm identref))))
                                                                 ((Pcoq.Symbol.token (Tok.PKEYWORD ("|-")))))
                                                 ((Pcoq.Symbol.nterm ltac_expr)))
                                 (fun e _ ids _ loc -> 
# 37 "plugins/ltac2_ltac1/g_ltac2_ltac1.mlg"
                                                                       ids, e 
                                                       )])]))
        in ()

package coq-core

Install

Dune Dependency

Authors

Maintainers

Sources

doc/src/ltac2_ltac1_plugin/g_ltac2_ltac1.ml.html

Source file g_ltac2_ltac1.ml

Source file `g_ltac2_ltac1.ml`