diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/build/windows/appveyor.sh | 8 | ||||
| -rw-r--r-- | dev/doc/naming-conventions.tex | 2 | ||||
| -rw-r--r-- | dev/top_printers.ml | 3 |
3 files changed, 10 insertions, 3 deletions
diff --git a/dev/build/windows/appveyor.sh b/dev/build/windows/appveyor.sh new file mode 100644 index 0000000000..53f7a23466 --- /dev/null +++ b/dev/build/windows/appveyor.sh @@ -0,0 +1,8 @@ +#!/bin/bash +set -e -x +wget $opam_url +tar -xf opam64.tar.xz +bash opam64/install.sh +opam init -a mingw https://github.com/fdopen/opam-repository-mingw.git --comp 4.02.3+mingw64c --switch 4.02.3+mingw64c +eval $(opam config env) +opam install -y ocamlfind camlp5 diff --git a/dev/doc/naming-conventions.tex b/dev/doc/naming-conventions.tex index 349164948d..337b9226df 100644 --- a/dev/doc/naming-conventions.tex +++ b/dev/doc/naming-conventions.tex @@ -267,7 +267,7 @@ If the conclusion is in the other way than listed below, add suffix {forall x y:D, op (op' x y) = op' x (op y)} \itemrule{Idempotency of binary operator {\op} on domain {\D}}{Dop\_idempotent} -{forall x:D, op x n = x} +{forall x:D, op x x = x} \itemrule{Idempotency of unary operator {\op} on domain {\D}}{Dop\_idempotent} {forall x:D, op (op x) = op x} diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 9884a0109a..ffa8fffdf5 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -229,7 +229,7 @@ let ppenvwithcst e = pp str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]" ++ spc() ++ str "{" ++ Cmap_env.fold (fun a _ s -> pr_con a ++ spc () ++ s) (Obj.magic e).Pre_env.env_globals.Pre_env.env_constants (mt ()) ++ str "}") -let pptac = (fun x -> pp(Ltac_plugin.Pptactic.pr_glob_tactic (Global.env()) x)) +let pptac = (fun x -> pp(Ltac_plugin.Pptactic.pr_glob_tactic (API.Global.env()) x)) let ppobj obj = Format.print_string (Libobject.object_tag obj) @@ -494,7 +494,6 @@ VERNAC COMMAND EXTEND PrintConstr END *) -open Grammar_API open Genarg open Stdarg open Egramml |