diff options
| -rw-r--r-- | coq-refman.opam | 2 | ||||
| -rw-r--r-- | coq.opam | 2 | ||||
| -rw-r--r-- | coqide-server.opam | 4 | ||||
| -rw-r--r-- | coqide.opam | 4 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 24 | ||||
| -rw-r--r-- | ide/.merlin.in | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrvernac.mlg | 2 | ||||
| -rw-r--r-- | tools/CoqMakefile.in | 2 | ||||
| -rw-r--r-- | topbin/dune | 5 |
9 files changed, 26 insertions, 21 deletions
diff --git a/coq-refman.opam b/coq-refman.opam index b9500243a3..16be422c27 100644 --- a/coq-refman.opam +++ b/coq-refman.opam @@ -17,7 +17,7 @@ license: "Open Publication License" depends: [ "dune" { build } - "coq" { build } + "coq" { build & = version } ] build-env: [ @@ -20,7 +20,7 @@ license: "LGPL-2.1" depends: [ "ocaml" { >= "4.05.0" } - "dune" { build & >= "1.4.0" } + "dune" { build & >= "1.6.0" } "ocamlfind" { build } "num" ] diff --git a/coqide-server.opam b/coqide-server.opam index ed6f3d98d8..0325d2549c 100644 --- a/coqide-server.opam +++ b/coqide-server.opam @@ -19,8 +19,8 @@ dev-repo: "git+https://github.com/coq/coq.git" license: "LGPL-2.1" depends: [ - "dune" { build & >= "1.4.0" } - "coq" + "dune" { build & >= "1.6.0" } + "coq" { = version } ] build: [ [ "dune" "build" "-p" name "-j" jobs ] ] diff --git a/coqide.opam b/coqide.opam index c82fa72564..2507acbb26 100644 --- a/coqide.opam +++ b/coqide.opam @@ -17,8 +17,8 @@ dev-repo: "git+https://github.com/coq/coq.git" license: "LGPL-2.1" depends: [ - "dune" { build & >= "1.4.0" } - "coqide-server" + "dune" { build & >= "1.6.0" } + "coqide-server" { = version } "lablgtk3" { >= "3.0.beta5" } "lablgtk3-sourceview3" { >= "3.0.beta5" } ] diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index afb0239be4..e6922408aa 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3830,25 +3830,25 @@ The general command to add a hint to some databases :n:`{+ @ident}` is check with :cmd:`Print HintDb` to verify the current cut expression: .. productionlist:: regexp - e : `ident` hint or instance identifier - : _ any hint - : `e` | `e` disjunction - : `e` `e` sequence - : `e` * Kleene star - : emp empty - : eps epsilon - : ( `e` ) + regexp : `ident` (hint or instance identifier) + : _ (any hint) + : `regexp` | `regexp` (disjunction) + : `regexp` `regexp` (sequence) + : `regexp` * (Kleene star) + : emp (empty) + : eps (epsilon) + : ( `regexp` ) The `emp` regexp does not match any search path while `eps` matches the empty path. During proof search, the path of successive successful hints on a search branch is recorded, as a - list of identifiers for the hints (note that Hint Extern’s do not have + list of identifiers for the hints (note that :cmd:`Hint Extern`\’s do not have an associated identifier). Before applying any hint :n:`@ident` the current path `p` extended with :n:`@ident` is matched against the current cut expression `c` associated to the hint database. If matching succeeds, the hint is *not* applied. The - semantics of ``Hint Cut e`` is to set the cut expression to ``c | e``, the - initial cut expression being `emp`. + semantics of :n:`Hint Cut @regexp` is to set the cut expression + to :n:`c | regexp`, the initial cut expression being `emp`. .. cmdv:: Hint Mode @qualid {* (+ | ! | -)} : @ident :name: Hint Mode @@ -3875,7 +3875,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is .. note:: One can use an ``Extern`` hint with no pattern to do pattern matching on - hypotheses using ``match goal`` with inside the tactic. + hypotheses using ``match goal with`` inside the tactic. Hint databases defined in the Coq standard library diff --git a/ide/.merlin.in b/ide/.merlin.in index 4dc6f45550..b8d7953833 100644 --- a/ide/.merlin.in +++ b/ide/.merlin.in @@ -1,4 +1,4 @@ -PKG unix laglgtk2 lablgtk2.sourceview2 +PKG unix laglgtk3 lablgtk3-sourceview3 S utils B utils diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index bf7f082192..08f028465b 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -465,7 +465,7 @@ let interp_modloc mr = (* The unified, extended vernacular "Search" command *) let ssrdisplaysearch gr env t = - let pr_res = pr_global gr ++ spc () ++ str " " ++ pr_lconstr_env env Evd.empty t in + let pr_res = pr_global gr ++ str ":" ++ spc () ++ pr_lconstr_env env Evd.empty t in Feedback.msg_info (hov 2 pr_res ++ fnl ()) } diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 48b797a3cd..2ec55d1bd0 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -177,7 +177,7 @@ COQCHKEXTRAFLAGS?= COQDOCEXTRAFLAGS?= # these flags do NOT contain the libraries, to make them easier to overwrite -COQFLAGS?=-q $(OPT) $(OTHERFLAGS) $(COQEXTRAFLAGS) +COQFLAGS?=-q $(OTHERFLAGS) $(COQEXTRAFLAGS) COQCHKFLAGS?=-silent -o $(COQCHKEXTRAFLAGS) COQDOCFLAGS?=-interpolate -utf8 $(COQDOCEXTRAFLAGS) diff --git a/topbin/dune b/topbin/dune index e35a3de54b..3b861afe78 100644 --- a/topbin/dune +++ b/topbin/dune @@ -28,6 +28,11 @@ (libraries coq.toplevel) (link_flags -linkall)) +(install + (section bin) + (package coq) + (files (coqc_bin.bc as coqc.byte))) + ; Workers (executables (names coqqueryworker_bin coqtacticworker_bin coqproofworker_bin) |