4 files changed, 21 insertions, 16 deletions
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 344a04a6aa..260e86ad67 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -116,9 +116,9 @@ open Pp
 open Genarg
 open Ppconstr
 open Printer
-let pr_firstorder_using_raw _ _ _ l = str "using " ++ prlist_with_sep pr_comma pr_reference l
-let pr_firstorder_using_glob _ _ _ l = str "using " ++ prlist_with_sep pr_comma (pr_or_var (fun x -> (pr_global (snd x)))) l
-let pr_firstorder_using_typed _ _ _ l = str "using " ++ prlist_with_sep pr_comma pr_global l
+let pr_firstorder_using_raw _ _ _ = Pptactic.pr_auto_using pr_reference
+let pr_firstorder_using_glob _ _ _ = Pptactic.pr_auto_using (pr_or_var (fun x -> pr_global (snd x)))
+let pr_firstorder_using_typed _ _ _ = Pptactic.pr_auto_using pr_global
 
 let warn_deprecated_syntax =
   CWarnings.create ~name:"firstorder-deprecated-syntax" ~category:"deprecated"
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index a063cbbfe3..e4b58a56f9 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1517,27 +1517,27 @@ let rec apply_ids t ids =
   | [] -> t
   | i::ids -> apply_ids (Term.mkApp(t,[| Term.mkVar i |])) ids
 
-let coq_Node = 
+let coq_Node = lazy
  (Coqlib.gen_constant_in_modules "VarMap"
    [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Node")
-let coq_Leaf = 
+let coq_Leaf = lazy
  (Coqlib.gen_constant_in_modules "VarMap"
    [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Leaf")
-let coq_Empty = 
+let coq_Empty = lazy
  (Coqlib.gen_constant_in_modules "VarMap"
    [["Coq" ; "micromega" ;"VarMap"];["VarMap"]] "Empty")
 
-let coq_VarMap = 
+let coq_VarMap = lazy
   (Coqlib.gen_constant_in_modules "VarMap"
      [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t")
  
 
 let rec dump_varmap typ m =
   match m with
-  | Mc.Empty -> Term.mkApp(coq_Empty,[| typ |])
-  | Mc.Leaf v -> Term.mkApp(coq_Leaf,[| typ; v|])
-  | Mc.Node(l,o,r) -> 
-    Term.mkApp (coq_Node, [| typ; dump_varmap typ l; o ; dump_varmap typ r |])
+  | Mc.Empty -> Term.mkApp(Lazy.force coq_Empty,[| typ |])
+  | Mc.Leaf v -> Term.mkApp(Lazy.force coq_Leaf,[| typ; v|])
+  | Mc.Node(l,o,r) ->
+    Term.mkApp (Lazy.force coq_Node, [| typ; dump_varmap typ l; o ; dump_varmap typ r |])
 
 
 let vm_of_list env =
@@ -1709,7 +1709,7 @@ let micromega_order_change spec cert cert_typ env ff  (*: unit Proofview.tactic*
     (set
       [
        ("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |]));
-       ("__varmap", vm, Term.mkApp( coq_VarMap, [|spec.typ|])); 
+       ("__varmap", vm, Term.mkApp(Lazy.force coq_VarMap, [|spec.typ|]));
        ("__wit", cert, cert_typ)
       ]
       (Tacmach.pf_concl gl))
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 77e25b2a5b..0d4be72d9e 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -355,7 +355,7 @@ let nf_open_term sigma0 ise c =
   !s', Evd.evar_universe_context s, c'
 
 let unif_end env sigma0 ise0 pt ok =
-  let ise = Evarconv.consider_remaining_unif_problems env ise0 in
+  let ise = Evarconv.solve_unif_constraints_with_heuristics env ise0 in
   let s, uc, t = nf_open_term sigma0 ise pt in
   let ise1 = create_evar_defs s in
   let ise1 = Evd.set_universe_context ise1 uc in
@@ -435,7 +435,7 @@ let proj_nparams c =
   try 1 + Recordops.find_projection_nparams (ConstRef c) with _ -> 0
 
 let isFixed c = match kind_of_term c with
-  | Var _ | Ind _ | Construct _ | Const _ -> true
+  | Var _ | Ind _ | Construct _ | Const _ | Proj _ -> true
   | _ -> false
 
 let isRigid c = match kind_of_term c with
@@ -487,6 +487,7 @@ let mk_tpattern ?p_origin ?(hack=false) env sigma0 (ise, t) ok dir p =
       let np = proj_nparams p in
       if np = 0 || np > List.length a then KpatConst, f, a else
       let a1, a2 = List.chop np a in KpatProj p, applist(f, a1), a2
+    | Proj (p,arg) -> KpatProj (Projection.constant p), f, a
     | Var _ | Ind _ | Construct _ -> KpatFixed, f, a
     | Evar (k, _) ->
       if Evd.mem sigma0 k then KpatEvar k, f, a else
@@ -567,6 +568,10 @@ let filter_upat i0 f n u fpats =
   if np < na then fpats else
   let () = if !i0 < np then i0 := n in (u, np) :: fpats
 
+let eq_prim_proj c t = match kind_of_term t with
+  | Proj(p,_) -> Constant.equal (Projection.constant p) c
+  | _ -> false
+
 let filter_upat_FO i0 f n u fpats =
   let np = nb_args u.up_FO in
   if n < np then fpats else
@@ -577,7 +582,7 @@ let filter_upat_FO i0 f n u fpats =
   | KpatLet -> isLetIn f
   | KpatLam -> isLambda f
   | KpatRigid -> isRigid f
-  | KpatProj pc -> Term.eq_constr f (mkConst pc)
+  | KpatProj pc -> Term.eq_constr f (mkConst pc) || eq_prim_proj pc f
   | KpatFlex -> i0 := n; true in
   if ok then begin if !i0 < np then i0 := np; (u, np) :: fpats end else fpats
 
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index 74a603e51c..288a04e60a 100644
--- a/plugins/ssrmatching/ssrmatching.mli
+++ b/plugins/ssrmatching/ssrmatching.mli
@@ -213,7 +213,7 @@ val assert_done : 'a option ref -> 'a
 
 (** Very low level APIs.
     these are calls to evarconv's [the_conv_x] followed by
-    [consider_remaining_unif_problems] and [resolve_typeclasses].
+    [solve_unif_constraints_with_heuristics] and [resolve_typeclasses].
     In case of failure they raise [NoMatch] *)
 
 val unify_HO : env -> evar_map -> constr -> constr -> evar_map