Merge branch 'v8.5'

3 files changed, 24 insertions, 11 deletions

diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index f00ecf8feb..9a64b03fd1 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -210,6 +210,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
   end in
   let avoid = ref [] in
   let { sigma=sigma } = Proof.V82.subgoals pf in
+  let sigma = Evd.nf_constraints sigma in
   let rec fill_holes c =
     match kind_of_term c with
     | Evar (e,args) ->
@@ -222,13 +223,13 @@ let inversion_scheme env sigma t sort dep_option inv_op =
   in
   let c = fill_holes pfterm in
   (* warning: side-effect on ownSign *)
-  let invProof = it_mkNamedLambda_or_LetIn c !ownSign
-  in
-  invProof
+  let invProof = it_mkNamedLambda_or_LetIn c !ownSign in
+  let p = Evarutil.nf_evars_universes sigma invProof in
+    p, Evd.universe_context sigma
 
 let add_inversion_lemma name env sigma t sort dep inv_op =
-  let invProof = inversion_scheme env sigma t sort dep inv_op in
-  let entry = definition_entry ~poly:true (*FIXME*) invProof in
+  let invProof, ctx = inversion_scheme env sigma t sort dep inv_op in
+  let entry = definition_entry ~poly:(Flags.use_polymorphic_flag ()) ~univs:ctx invProof in
   let _ = declare_constant name (DefinitionEntry entry, IsProof Lemma) in
   ()
 
@@ -236,7 +237,8 @@ let add_inversion_lemma name env sigma t sort dep inv_op =
  * inv_op = InvNoThining (derives de semi inversion lemma) *)
 
 let add_inversion_lemma_exn na com comsort bool tac =
-  let env = Global.env () and evd = ref Evd.empty in
+  let env = Global.env () in
+  let evd = ref (Evd.from_env env) in
   let c = Constrintern.interp_type_evars env evd com in
   let sigma, sort = Pretyping.interp_sort !evd comsort in
   try
diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml
index 215713d981..ab71f5f2e7 100644
--- a/tactics/taccoerce.ml
+++ b/tactics/taccoerce.ml
@@ -176,6 +176,13 @@ let coerce_to_evaluable_ref env v =
     let id = out_gen (topwit wit_var) v in
     if Id.List.mem id (Termops.ids_of_context env) then EvalVarRef id
     else fail ()
+  else if has_type v (topwit wit_ref) then
+    let open Globnames in
+    let r = out_gen (topwit wit_ref) v in
+    match r with
+    | VarRef var -> EvalVarRef var
+    | ConstRef c -> EvalConstRef c
+    | IndRef _ | ConstructRef _ -> fail ()
   else
     let ev = match Value.to_constr v with
     | Some c when isConst c -> EvalConstRef (Univ.out_punivs (destConst c))
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 9265328a47..04df3b8cda 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -425,7 +425,7 @@ let pf_reduce_decl redfun where (id,c,ty) gl =
   match c with
   | None ->
       if where == InHypValueOnly then
-	errorlabstrm "" (pr_id id ++ str "has no value.");
+	errorlabstrm "" (pr_id id ++ str " has no value.");
       (id,None,redfun' ty)
   | Some b ->
       let b' = if where != InHypTypeOnly then redfun' b else b in
@@ -522,7 +522,7 @@ let pf_e_reduce_decl redfun where (id,c,ty) gl =
   match c with
   | None ->
       if where == InHypValueOnly then
-	errorlabstrm "" (pr_id id ++ str "has no value.");
+	errorlabstrm "" (pr_id id ++ str " has no value.");
     let sigma, ty' = redfun sigma ty in
       sigma, (id,None,ty')
   | Some b ->
@@ -565,12 +565,16 @@ let e_pf_change_decl (redfun : bool -> e_reduction_function) where (id,c,ty) env
   match c with
   | None ->
       if where == InHypValueOnly then
-	errorlabstrm "" (pr_id id ++ str "has no value.");
+	errorlabstrm "" (pr_id id ++ str " has no value.");
     let sigma',ty' = redfun false env sigma ty in
       sigma', (id,None,ty')
   | Some b ->
-      let sigma',b' = if where != InHypTypeOnly then redfun true env sigma b else sigma, b in
-      let sigma',ty' = if where != InHypValueOnly then redfun false env sigma ty else sigma', ty in
+      let sigma',b' = 
+	if where != InHypTypeOnly then redfun true env sigma b else sigma, b 
+      in
+      let sigma',ty' = 
+	if where != InHypValueOnly then redfun false env sigma' ty else sigma', ty 
+      in
 	sigma', (id,Some b',ty')
 
 let e_change_in_hyp redfun (id,where) =