diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/base_include | 2 | ||||
| -rw-r--r-- | dev/ci/user-overlays/06676-gares-proofview-goals-come-with-a-state.sh | 6 | ||||
| -rw-r--r-- | dev/vm_printers.ml | 3 |
3 files changed, 8 insertions, 3 deletions
diff --git a/dev/base_include b/dev/base_include index 39e3ef2bde..3320a2a942 100644 --- a/dev/base_include +++ b/dev/base_include @@ -232,7 +232,7 @@ let _ = Flags.in_toplevel := true let _ = Constrextern.set_extern_reference (fun ?loc _ r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Id.Set.empty r));; -let go () = Coqloop.loop ~time:false ~state:Option.(get !Coqtop.drop_last_doc) +let go () = Coqloop.loop ~time:false ~state:Option.(get !Coqloop.drop_last_doc) let _ = print_string diff --git a/dev/ci/user-overlays/06676-gares-proofview-goals-come-with-a-state.sh b/dev/ci/user-overlays/06676-gares-proofview-goals-come-with-a-state.sh new file mode 100644 index 0000000000..2451657d43 --- /dev/null +++ b/dev/ci/user-overlays/06676-gares-proofview-goals-come-with-a-state.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "6676" ] || [ "$CI_BRANCH" = "proofview/goal-w-state" ]; then + ltac2_CI_BRANCH=fix-for/6676 + ltac2_CI_GITURL=https://github.com/gares/ltac2.git + Equations_CI_BRANCH=fix-for/6676 + Equations_CI_GITURL=https://github.com/gares/Coq-Equations.git +fi diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index f819d2e6a9..bb7a963aa1 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -61,7 +61,7 @@ and ppstack s = and ppatom a = match a with | Aid idk -> print_idkey idk - | Atype u -> print_string "Type(...)" + | Asort u -> print_string "Sort(...)" | Aind(sp,i) -> print_string "Ind("; print_string (MutInd.to_string sp); print_string ","; print_int i; @@ -69,7 +69,6 @@ and ppatom a = and ppwhd whd = match whd with - | Vsort s -> ppsort s | Vprod _ -> print_string "product" | Vfun _ -> print_string "function" | Vfix _ -> print_vfix() |