5 files changed, 25 insertions, 6 deletions
diff --git a/dev/base_include b/dev/base_include
index 350ccaa109..3320a2a942 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -196,7 +196,10 @@ let parse_tac    = Pcoq.parse_string Ltac_plugin.Pltac.tactic;;
 (* build a term of type glob_constr without type-checking or resolution of 
    implicit syntax *)
 
-let e s = Constrintern.intern_constr (Global.env()) (parse_constr s);;
+let e s =
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  Constrintern.intern_constr env sigma (parse_constr s);;
 
 (* build a term of type constr with type-checking and resolution of 
    implicit syntax *)
@@ -229,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/06511-ejgallego-econstr+more_fix.sh b/dev/ci/user-overlays/06511-ejgallego-econstr+more_fix.sh
new file mode 100644
index 0000000000..4b681909d6
--- /dev/null
+++ b/dev/ci/user-overlays/06511-ejgallego-econstr+more_fix.sh
@@ -0,0 +1,7 @@
+ if [ "$CI_PULL_REQUEST" = "6511" ] || [ "$CI_BRANCH" = "econstr+more_fix" ]; then
+    ltac2_CI_BRANCH=econstr+more_fix
+    ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
+
+    Equations_CI_BRANCH=econstr+more_fix
+    Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+fi
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/top_printers.ml b/dev/top_printers.ml
index f99e2593d7..2c983fd8d2 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -313,6 +313,8 @@ let constr_display csr =
   in
   pp (str (term_display csr) ++fnl ())
 
+let econstr_display c = constr_display EConstr.Unsafe.(to_constr c) ;;
+
 open Format;;
 
 let print_pure_constr csr =
@@ -452,6 +454,8 @@ let print_pure_constr csr =
 	print_string (Printexc.to_string e);print_flush ();
 	raise e
 
+let print_pure_econstr c = print_pure_constr EConstr.Unsafe.(to_constr c) ;;
+
 let pploc x = let (l,r) = Loc.unloc x in
   print_string"(";print_int l;print_string",";print_int r;print_string")"
 
@@ -505,7 +509,7 @@ let _ =
       (function
          [c] when genarg_tag c = unquote (topwit wit_constr) && true ->
            let c = out_gen (rawwit wit_constr) c in
-           (fun ~atts ~st -> in_current_context constr_display c; st)
+           (fun ~atts ~st -> in_current_context econstr_display c; st)
        | _ -> failwith "Vernac extension: cannot occur")
   with
     e -> pp (CErrors.print e)
@@ -521,7 +525,7 @@ let _ =
       (function
          [c] when genarg_tag c = unquote (topwit wit_constr) && true ->
            let c = out_gen (rawwit wit_constr) c in
-           (fun ~atts ~st -> in_current_context print_pure_constr c; st)
+           (fun ~atts ~st -> in_current_context print_pure_econstr c; st)
        | _ -> failwith "Vernac extension: cannot occur")
   with
     e -> pp (CErrors.print e)
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()