Merge branch 'v8.5'

4 files changed, 39 insertions, 35 deletions

diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 0d24b71387..0c8440fe5a 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -641,12 +641,7 @@ TACTIC EXTEND convert_concl_no_check
 | ["convert_concl_no_check" constr(x) ] -> [ convert_concl_no_check x DEFAULTcast ]
 END
 
-
-let pr_hints_path_atom prc _ _ a =
-  match a with
-  | PathAny -> str"."
-  | PathHints grs ->
-    pr_sequence Printer.pr_global grs
+let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom
 
 ARGUMENT EXTEND hints_path_atom
   TYPED AS hints_path_atom
@@ -655,15 +650,7 @@ ARGUMENT EXTEND hints_path_atom
 | [ "*" ] -> [ PathAny ]
 END
 
-let pr_hints_path prc prx pry c =
-  let rec aux = function
-  | PathAtom a -> pr_hints_path_atom prc prx pry a
-  | PathStar p -> str"(" ++ aux p ++ str")*"
-  | PathSeq (p, p') -> aux p ++ spc () ++ aux p'
-  | PathOr (p, p') -> str "(" ++ aux p ++ str"|" ++ aux p' ++ str")"
-  | PathEmpty -> str"ø"
-  | PathEpsilon -> str"ε"
-  in aux c
+let pr_hints_path prc prx pry c = Hints.pp_hints_path c
 
 ARGUMENT EXTEND hints_path
   TYPED AS hints_path
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 4ba9adafec..5630d20b5d 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -382,15 +382,19 @@ let rec normalize_path h =
 
 let path_derivate hp hint = normalize_path (path_derivate hp hint)
 
+let pp_hints_path_atom a =
+  match a with
+  | PathAny -> str"*"
+  | PathHints grs -> pr_sequence pr_global grs
+					   
 let rec pp_hints_path = function
-  | PathAtom (PathAny) -> str"."
-  | PathAtom (PathHints grs) -> pr_sequence pr_global grs
-  | PathStar p -> str "(" ++ pp_hints_path p ++ str")*"
+  | PathAtom pa -> pp_hints_path_atom pa
+  | PathStar p -> str "!(" ++ pp_hints_path p ++ str")"
   | PathSeq (p, p') -> pp_hints_path p ++ str" ; " ++ pp_hints_path p'
   | PathOr (p, p') -> 
     str "(" ++ pp_hints_path p ++ spc () ++ str"|" ++ spc () ++ pp_hints_path p' ++ str ")"
-  | PathEmpty -> str"Ø"
-  | PathEpsilon -> str"ε"
+  | PathEmpty -> str"emp"
+  | PathEpsilon -> str"eps"
 
 let subst_path_atom subst p =
   match p with
diff --git a/tactics/hints.mli b/tactics/hints.mli
index af4d3d1f66..3a0521f665 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -70,6 +70,7 @@ type hints_path =
 val normalize_path : hints_path -> hints_path
 val path_matches : hints_path -> hints_path_atom list -> bool
 val path_derivate : hints_path -> hints_path_atom -> hints_path
+val pp_hints_path_atom : hints_path_atom -> Pp.std_ppcmds
 val pp_hints_path : hints_path -> Pp.std_ppcmds
 
 module Hint_db :
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index fc453cfaf9..bb97c80be2 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -242,8 +242,9 @@ let convert_hyp_no_check = convert_hyp ~check:false
 let convert_gen pb x y =
   Proofview.Goal.enter { enter = begin fun gl ->
     try
-      let sigma = Tacmach.New.pf_apply Evd.conversion gl pb x y in
-      Proofview.Unsafe.tclEVARS sigma
+      let sigma, b = Tacmach.New.pf_apply (Reductionops.infer_conv ~pb) gl x y in
+      if b then Proofview.Unsafe.tclEVARS sigma
+      else Tacticals.New.tclFAIL 0 (str "Not convertible")
     with (* Reduction.NotConvertible *) _ ->
       (** FIXME: Sometimes an anomaly is raised from conversion *)
       Tacticals.New.tclFAIL 0 (str "Not convertible")
@@ -3300,7 +3301,7 @@ let is_defined_variable env id = match lookup_named id env with
 | (_, Some _, _) -> true
 
 let abstract_args gl generalize_vars dep id defined f args =
-  let sigma = Tacmach.project gl in
+  let sigma = ref (Tacmach.project gl) in
   let env = Tacmach.pf_env gl in
   let concl = Tacmach.pf_concl gl in
   let dep = dep || dependent (mkVar id) concl in
@@ -3317,11 +3318,12 @@ let abstract_args gl generalize_vars dep id defined f args =
     *)
   let aux (prod, ctx, ctxenv, c, args, eqs, refls, nongenvars, vars, env) arg =
     let (name, _, ty), arity =
-      let rel, c = Reductionops.splay_prod_n env sigma 1 prod in
+      let rel, c = Reductionops.splay_prod_n env !sigma 1 prod in
 	List.hd rel, c
     in
     let argty = Tacmach.pf_unsafe_type_of gl arg in
-    let ty = (* refresh_universes_strict *) ty in
+    let sigma', ty = Evarsolve.refresh_universes (Some true) env !sigma ty in
+    let () = sigma := sigma' in
     let lenctx = List.length ctx in
     let liftargty = lift lenctx argty in
     let leq = constr_cmp Reduction.CUMUL liftargty ty in
@@ -3360,8 +3362,9 @@ let abstract_args gl generalize_vars dep id defined f args =
 	      true, mkApp (f', before), after
   in
     if dogen then
+      let tyf' = Tacmach.pf_unsafe_type_of gl f' in
       let arity, ctx, ctxenv, c', args, eqs, refls, nogen, vars, env =
-	Array.fold_left aux (Tacmach.pf_unsafe_type_of gl f',[],env,f',[],[],[],Id.Set.empty,Id.Set.empty,env) args'
+	Array.fold_left aux (tyf',[],env,f',[],[],[],Id.Set.empty,Id.Set.empty,env) args'
       in
       let args, refls = List.rev args, List.rev refls in
       let vars =
@@ -3370,9 +3373,12 @@ let abstract_args gl generalize_vars dep id defined f args =
 	    hyps_of_vars (pf_env gl) (pf_hyps gl) nogen vars
 	else []
       in
-      let body, c' = if defined then Some c', Retyping.get_type_of ctxenv Evd.empty c' else None, c' in
-	Some (make_abstract_generalize gl id concl dep ctx body c' eqs args refls,
-	     dep, succ (List.length ctx), vars)
+      let body, c' =
+	if defined then Some c', Retyping.get_type_of ctxenv !sigma c'
+	else None, c'
+      in
+      let term = make_abstract_generalize {gl with sigma = !sigma} id concl dep ctx body c' eqs args refls in
+	Some (term, !sigma, dep, succ (List.length ctx), vars)
     else None
 
 let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id =
@@ -3394,20 +3400,26 @@ let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id =
     let newc = Tacmach.New.of_old (fun gl -> abstract_args gl generalize_vars force_dep id def f args) gl in
       match newc with
       | None -> Proofview.tclUNIT ()
-      | Some (newc, dep, n, vars) ->
+      | Some (newc, sigma, dep, n, vars) ->
 	  let tac =
 	    if dep then
-	      Tacticals.New.tclTHENLIST [Proofview.V82.tactic (refine newc); rename_hyp [(id, oldid)]; Tacticals.New.tclDO n intro;
-			   Proofview.V82.tactic (generalize_dep ~with_let:true (mkVar oldid))]
-	    else
-	      Tacticals.New.tclTHENLIST [Proofview.V82.tactic (refine newc); Proofview.V82.tactic (clear [id]); Tacticals.New.tclDO n intro]
+	      Tacticals.New.tclTHENLIST
+		[Proofview.Unsafe.tclEVARS sigma;
+		 Proofview.V82.tactic (refine newc);
+		 rename_hyp [(id, oldid)]; Tacticals.New.tclDO n intro;
+		 Proofview.V82.tactic (generalize_dep ~with_let:true (mkVar oldid))]
+	    else Tacticals.New.tclTHENLIST
+		   [Proofview.Unsafe.tclEVARS sigma;
+		    Proofview.V82.tactic (refine newc);
+		    Proofview.V82.tactic (clear [id]);
+		    Tacticals.New.tclDO n intro]
 	  in
 	    if List.is_empty vars then tac
 	    else Tacticals.New.tclTHEN tac
               (Tacticals.New.tclFIRST
                 [revert vars ;
 		 Proofview.V82.tactic (fun gl -> tclMAP (fun id ->
-				     tclTRY (generalize_dep ~with_let:true (mkVar id))) vars gl)])
+		      tclTRY (generalize_dep ~with_let:true (mkVar id))) vars gl)])
   end }
 
 let rec compare_upto_variables x y =