1 files changed, 14 insertions, 13 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 6fab111e6f..0cc8becd8f 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -46,7 +46,7 @@ let rec head_bound sigma t = match EConstr.kind sigma t with
 | Prod (_, _, b)  -> head_bound sigma b
 | LetIn (_, _, _, b) -> head_bound sigma b
 | App (c, _) -> head_bound sigma c
-| Case (_, _, _, c, _) -> head_bound sigma c
+| Case (_, _, _, _, _, c, _) -> head_bound sigma c
 | Ind (ind, _) -> GlobRef.IndRef ind
 | Const (c, _) -> GlobRef.ConstRef c
 | Construct (c, _) -> GlobRef.ConstructRef c
@@ -340,10 +340,8 @@ let instantiate_hint env sigma p =
   let mk_clenv (c, cty, ctx) =
     let sigma = merge_context_set_opt sigma ctx in
     let cl = mk_clenv_from_env env sigma None (c,cty) in
-    let cl = {cl with templval =
-          { cl.templval with rebus = strip_params env sigma cl.templval.rebus };
-        env = empty_env}
-    in
+    let templval = { cl.templval with rebus = strip_params env sigma cl.templval.rebus } in
+    let cl = mk_clausenv empty_env cl.evd templval cl.templtyp in
     { hint_term = c; hint_type = cty; hint_uctx = ctx; hint_clnv = cl; }
   in
   let code = match p.code.obj with
@@ -593,7 +591,7 @@ struct
   let head_evar sigma c =
     let rec hrec c = match EConstr.kind sigma c with
       | Evar (evk,_)   -> evk
-      | Case (_,_,_,c,_) -> hrec c
+      | Case (_,_,_,_,_,c,_) -> hrec c
       | App (c,_)      -> hrec c
       | Cast (c,_,_)   -> hrec c
       | Proj (p, c)    -> hrec c
@@ -1649,14 +1647,17 @@ let connect_hint_clenv h gl =
     let emap c = Vars.subst_univs_level_constr subst c in
     let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
     (* Only metas are mentioning the old universes. *)
-    {
-      templval = Evd.map_fl emap clenv.templval;
-      templtyp = Evd.map_fl emap clenv.templtyp;
-      evd = Evd.map_metas emap evd;
-      env = Proofview.Goal.env gl;
-    }
+    Clenv.mk_clausenv
+      (Proofview.Goal.env gl)
+      (Evd.map_metas emap evd)
+      (Evd.map_fl emap clenv.templval)
+      (Evd.map_fl emap clenv.templtyp)
   | None ->
-    { clenv with evd = evd ; env = Proofview.Goal.env gl }
+    Clenv.mk_clausenv
+      (Proofview.Goal.env gl)
+      evd
+      clenv.templval
+      clenv.templtyp
 
 let fresh_hint env sigma h =
   let { hint_term = c; hint_uctx = ctx } = h in