7 files changed, 45 insertions, 13 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/doc/build-system.txt b/dev/doc/build-system.txt
index 1c4fd2eba4..fd3101613a 100644
--- a/dev/doc/build-system.txt
+++ b/dev/doc/build-system.txt
@@ -143,7 +143,9 @@ file list(s):
    These files are also used by the experimental ocamlbuild plugin,
    which is quite touchy about them : be careful with order,
    duplicated entries, whitespace errors, and do not mention .mli there.
- - For .v, in the corresponding vo.itarget (e.g theories/Init/vo.itarget)
+   If module B depends on module A, then B should be after A in the .mllib
+   file.
+- For .v, in the corresponding vo.itarget (e.g theories/Init/vo.itarget)
  - The definitions in Makefile.common might have to be adapted too.
  - If your file needs a specific rule, add it to Makefile.build
 
diff --git a/dev/lint-commits.sh b/dev/lint-commits.sh
index eb12bc2273..d8043558eb 100755
--- a/dev/lint-commits.sh
+++ b/dev/lint-commits.sh
@@ -19,14 +19,21 @@ fi
 BASE_COMMIT="$1"
 HEAD_COMMIT="$2"
 
-# git diff --check
-# uses .gitattributes to know what to check
-if git diff --check "$BASE_COMMIT" "$HEAD_COMMIT";
+bad=()
+while IFS= read -r commit; do
+    echo Checking "$commit"
+    # git diff --check
+    # uses .gitattributes to know what to check
+    if ! git diff --check "${commit}^" "$commit";
+    then
+        bad+=("$commit")
+    fi
+done < <(git rev-list "$HEAD_COMMIT" --not "$BASE_COMMIT" --)
+
+if [ "${#bad[@]}" != 0 ]
 then
-    :
-else
     >&2 echo "Whitespace errors!"
-    >&2 echo "Running 'git diff --check $BASE_COMMIT $HEAD_COMMIT'."
+    >&2 echo "In commits ${bad[*]}"
     >&2 echo "If you use emacs, you can prevent this kind of error from reocurring by installing ws-butler and enabling ws-butler-convert-leading-tabs-or-spaces."
     exit 1
 fi
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 0c3f03d0a5..74cdd788b4 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -315,6 +315,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 =
@@ -454,6 +456,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")"
 
@@ -507,7 +511,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)
@@ -523,7 +527,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..2ddf927d9b 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -36,6 +36,10 @@ let print_idkey idk =
       print_string ")"
   | VarKey id -> print_string (Id.to_string id)
   | RelKey i -> print_string "~";print_int i
+  | EvarKey evk ->
+    print_string "Evar(";
+    print_int (Evar.repr evk);
+    print_string ")"
 
 let rec ppzipper z =
   match z with
@@ -61,7 +65,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 +73,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()