Merge branch 'v8.5'

2 files changed, 21 insertions, 16 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 7d101b4c72..a38a36bdcc 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -356,9 +356,11 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
       | App (f,l) ->
 	let (acc',hdty,sigma,applicand) =
 	  if is_template_polymorphic env f then
-	    let sigma, ty = 
+	    let ty = 
 	      (* Template sort-polymorphism of definition and inductive types *)
-	      type_of_global_reference_knowing_conclusion env sigma f conclty
+	      let firstmeta = Array.findi (fun i x -> occur_meta x) l in
+	      let args, _ = Option.cata (fun i -> CArray.chop i l) (l, [||]) firstmeta in
+	        type_of_global_reference_knowing_parameters env sigma f args
 	    in
 	      goalacc, ty, sigma, f
 	  else
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 96ba88233e..d69b5b4215 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -387,20 +387,23 @@ let tclTRYFOCUS i j t = tclFOCUS_gen (tclUNIT ()) i j t
 let tclFOCUSID id t =
   let open Proof in
   Pv.get >>= fun initial ->
-  let rec aux n = function
-    | [] -> tclZERO (NoSuchGoals 1)
-    | g::l ->
-        if Names.Id.equal (Evd.evar_ident g initial.solution) id then
-          let (focused,context) = focus n n initial in
-          Pv.set focused >>
-          t >>= fun result ->
-          Pv.modify (fun next -> unfocus context next) >>
-          return result
-        else
-          aux (n+1) l in
-  aux 1 initial.comb
-
-
+  try
+    let ev = Evd.evar_key id initial.solution in
+    try
+      let n = CList.index Evar.equal ev initial.comb in
+      (* goal is already under focus *)
+      let (focused,context) = focus n n initial in
+      Pv.set focused >>
+        t >>= fun result ->
+      Pv.modify (fun next -> unfocus context next) >>
+        return result
+    with Not_found ->
+      (* otherwise, save current focus and work purely on the shelve *)
+      Comb.set [ev] >>
+        t >>= fun result ->
+      Comb.set initial.comb  >>
+        return result
+  with Not_found -> tclZERO (NoSuchGoals 1)
 
 (** {7 Dispatching on goals} *)