diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/base_include | 2 | ||||
| -rw-r--r-- | dev/ci/ci-basic-overlay.sh | 6 | ||||
| -rwxr-xr-x | dev/ci/ci-equations.sh | 10 | ||||
| -rw-r--r-- | dev/top_printers.ml | 4 |
4 files changed, 19 insertions, 3 deletions
diff --git a/dev/base_include b/dev/base_include index 0c2bdb9a25..1da5e3ed18 100644 --- a/dev/base_include +++ b/dev/base_include @@ -230,7 +230,7 @@ let pf_e gl s = let _ = Flags.in_debugger := false let _ = Flags.in_toplevel := true let _ = Constrextern.set_extern_reference - (fun ?loc _ r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Idset.empty r));; + (fun ?loc _ r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Id.Set.empty r));; let go () = Coqloop.loop Option.(get !Coqtop.drop_last_doc) diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index cb1493d6aa..168a34e6e4 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -135,3 +135,9 @@ ######################################################################## : ${bignums_CI_BRANCH:=master} : ${bignums_CI_GITURL:=https://github.com/coq/bignums.git} + +######################################################################## +# Equations +######################################################################## +: ${Equations_CI_BRANCH:=8.8+alpha} +: ${Equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations.git} diff --git a/dev/ci/ci-equations.sh b/dev/ci/ci-equations.sh new file mode 100755 index 0000000000..f7470463d9 --- /dev/null +++ b/dev/ci/ci-equations.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +Equations_CI_DIR=${CI_BUILD_DIR}/Equations + +git_checkout ${Equations_CI_BRANCH} ${Equations_CI_GITURL} ${Equations_CI_DIR} + +( cd ${Equations_CI_DIR} && coq_makefile -f _CoqProject -o Makefile && make -j ${NJOBS} && make -j ${NJOBS} test-suite && make -j ${NJOBS} examples && make install) diff --git a/dev/top_printers.ml b/dev/top_printers.ml index b4c8ae33ca..5b09436c26 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -508,7 +508,7 @@ let _ = (function [c] when genarg_tag c = unquote (topwit wit_constr) && true -> let c = out_gen (rawwit wit_constr) c in - (fun _ -> in_current_context constr_display c) + (fun _ st -> in_current_context constr_display c; st) | _ -> failwith "Vernac extension: cannot occur") with e -> pp (CErrors.print e) @@ -524,7 +524,7 @@ let _ = (function [c] when genarg_tag c = unquote (topwit wit_constr) && true -> let c = out_gen (rawwit wit_constr) c in - (fun _ -> in_current_context print_pure_constr c) + (fun _ st -> in_current_context print_pure_constr c; st) | _ -> failwith "Vernac extension: cannot occur") with e -> pp (CErrors.print e) |