1 files changed, 107 insertions, 100 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 2d92387c..bc644857 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -10,7 +10,7 @@
 *)
 open Pp
 open Util
-open Errors
+open CErrors
 open Names
 open Vars
 open Termops
@@ -35,6 +35,10 @@ open Hints
 
 let priority l = List.filter (fun (_, hint) -> Int.equal hint.pri 0) l
 
+let compute_secvars gl =
+  let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
+  secvars_of_hyps hyps
+
 (* tell auto not to reuse already instantiated metas in unification (for
    compatibility, since otherwise, apply succeeds oftener) *)
 
@@ -67,16 +71,13 @@ let auto_unif_flags_of st1 st2 useeager =
 let auto_unif_flags =
   auto_unif_flags_of full_transparent_state empty_transparent_state false
 
-let auto_flags_of_state st =
-  auto_unif_flags_of full_transparent_state st false
-
 (* Try unification with the precompiled clause, then use registered Apply *)
 
 let connect_hint_clenv poly (c, _, ctx) clenv gl =
   (** [clenv] has been generated by a hint-making function, so the only relevant
       data in its evarmap is the set of metas. The [evar_reset_evd] function
       below just replaces the metas of sigma by those coming from the clenv. *)
-  let sigma = Proofview.Goal.sigma gl in
+  let sigma = Tacmach.New.project gl in
   let evd = Evd.evars_reset_evd ~with_conv_pbs:true ~with_univs:false sigma clenv.evd in
   (** Still, we need to update the universes *)
   let clenv, c =
@@ -85,22 +86,25 @@ let connect_hint_clenv poly (c, _, ctx) clenv gl =
       let (subst, ctx) = Universes.fresh_universe_context_set_instance ctx in
       let map c = Vars.subst_univs_level_constr subst c in
       let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
-      let clenv = { clenv with evd = evd ; env = Proofview.Goal.env gl } in
-      (** FIXME: We're being inefficient here because we substitute the whole
-          evar map instead of just its metas, which are the only ones
-          mentioning the old universes. *)
-      Clenv.map_clenv map clenv, map c
+      (** Only metas are mentioning the old universes. *)
+      let clenv = {
+        templval = Evd.map_fl map clenv.templval;
+        templtyp = Evd.map_fl map clenv.templtyp;
+        evd = Evd.map_metas map evd;
+        env = Proofview.Goal.env gl;
+      } in
+      clenv, map c
     else
       let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
       { clenv with evd = evd ; env = Proofview.Goal.env gl }, c
   in clenv, c
-		     
+
 let unify_resolve poly flags ((c : raw_hint), clenv) =
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
   let clenv, c = connect_hint_clenv poly c clenv gl in
   let clenv = Tacmach.New.of_old (fun gl -> clenv_unique_resolver ~flags clenv gl) gl in
   Clenvtac.clenv_refine false clenv
-  end
+  end }
 
 let unify_resolve_nodelta poly h = unify_resolve poly auto_unif_flags h
 
@@ -109,20 +113,12 @@ let unify_resolve_gen poly = function
   | Some flags -> unify_resolve poly flags
 
 let exact poly (c,clenv) =
-  let (c, _, _) = c in
-  let ctx, c' = 
-    if poly then
-      let evd', subst = Evd.refresh_undefined_universes clenv.evd in
-      let ctx = Evd.evar_universe_context evd' in
-	ctx, subst_univs_level_constr subst c 
-    else 
-      let ctx = Evd.evar_universe_context clenv.evd in
-	ctx, c
-  in
-  Proofview.Goal.enter begin fun gl ->
-    let sigma = Evd.merge_universe_context (Proofview.Goal.sigma gl) ctx in
-    Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (exact_check c')
-  end
+  Proofview.Goal.enter { enter = begin fun gl ->
+    let clenv', c = connect_hint_clenv poly c clenv gl in
+    Tacticals.New.tclTHEN
+    (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
+    (exact_check c)
+  end }
 
 (* Util *)
 
@@ -138,8 +134,6 @@ si après Intros la conclusion matche le pattern.
 
 (* conclPattern doit échouer avec error car il est rattraper par tclFIRST *)
 
-let (forward_interp_tactic, extern_interp) = Hook.make ()
-
 let conclPattern concl pat tac =
   let constr_bindings env sigma =
     match pat with
@@ -150,11 +144,23 @@ let conclPattern concl pat tac =
 	with Constr_matching.PatternMatchingFailure ->
           Tacticals.New.tclZEROMSG (str "conclPattern")
   in
-   Proofview.Goal.enter (fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
      let env = Proofview.Goal.env gl in
-     let sigma = Proofview.Goal.sigma gl in
+     let sigma = Tacmach.New.project gl in
        constr_bindings env sigma >>= fun constr_bindings ->
-     Hook.get forward_interp_tactic constr_bindings tac)
+     let open Genarg in
+     let open Geninterp in
+     let inj c = match val_tag (topwit Constrarg.wit_constr) with
+     | Val.Base tag -> Val.Dyn (tag, c)
+     | _ -> assert false
+     in
+     let fold id c accu = Id.Map.add id (inj c) accu in
+     let lfun = Id.Map.fold fold constr_bindings Id.Map.empty in
+     let ist = { lfun; extra = TacStore.empty } in
+     match tac with
+     | GenArg (Glbwit wit, tac) ->
+      Ftactic.run (Geninterp.interp wit ist tac) (fun _ -> Proofview.tclUNIT ())
+  end }
 
 (***********************************************************)
 (** A debugging / verbosity framework for trivial and auto *)
@@ -217,11 +223,11 @@ let tclLOG (dbg,depth,trace) pp tac =
       Proofview.V82.tactic begin fun gl ->
 	try
 	  let out = Proofview.V82.of_tactic tac gl in
-	  msg_debug (str s ++ spc () ++ pp () ++ str ". (*success*)");
+	  Feedback.msg_debug (str s ++ spc () ++ pp () ++ str ". (*success*)");
 	  out
 	with reraise ->
-          let reraise = Errors.push reraise in
-	  msg_debug (str s ++ spc () ++ pp () ++ str ". (*fail*)");
+          let reraise = CErrors.push reraise in
+	  Feedback.msg_debug (str s ++ spc () ++ pp () ++ str ". (*fail*)");
 	  iraise reraise
       end
     | Info ->
@@ -232,7 +238,7 @@ let tclLOG (dbg,depth,trace) pp tac =
 	  trace := (depth, Some pp) :: !trace;
 	  out
 	with reraise ->
-          let reraise = Errors.push reraise in
+          let reraise = CErrors.push reraise in
 	  trace := (depth, None) :: !trace;
 	  iraise reraise
       end
@@ -258,31 +264,25 @@ let pr_info_atom (d,pp) =
 
 let pr_info_trace = function
   | (Info,_,{contents=(d,Some pp)::l}) ->
-      prlist_with_sep fnl pr_info_atom (cleanup_info_trace d [(d,pp)] l)
-  | _ -> mt ()
+      Feedback.msg_info (prlist_with_sep fnl pr_info_atom (cleanup_info_trace d [(d,pp)] l))
+  | _ -> ()
 
 let pr_info_nop = function
-  | (Info,_,_) -> str "idtac."
-  | _ -> mt ()
+  | (Info,_,_) -> Feedback.msg_info (str "idtac.")
+  | _ -> ()
 
 let pr_dbg_header = function
-  | (Off,_,_) -> mt ()
-  | (Debug,0,_) -> str "(* debug trivial : *)"
-  | (Debug,_,_) -> str "(* debug auto : *)"
-  | (Info,0,_) -> str "(* info trivial : *)"
-  | (Info,_,_) -> str "(* info auto : *)"
+  | (Off,_,_) -> ()
+  | (Debug,0,_) -> Feedback.msg_debug (str "(* debug trivial: *)")
+  | (Debug,_,_) -> Feedback.msg_debug (str "(* debug auto: *)")
+  | (Info,0,_) -> Feedback.msg_info (str "(* info trivial: *)")
+  | (Info,_,_) -> Feedback.msg_info (str "(* info auto: *)")
 
 let tclTRY_dbg d tac =
-  let (level, _, _) = d in
   let delay f = Proofview.tclUNIT () >>= fun () -> f () in
-  let tac = match level with
-  | Off -> tac
-  | Debug | Info -> delay (fun () -> msg_debug (pr_dbg_header d ++ fnl () ++ pr_info_trace d); tac)
-  in
-  let after = match level with
-  | Info -> delay (fun () -> msg_debug (pr_info_nop d); Proofview.tclUNIT ())
-  | Off | Debug -> Proofview.tclUNIT ()
-  in
+  let tac = delay (fun () -> pr_dbg_header d; tac) >>=
+              fun () -> pr_info_trace d; Proofview.tclUNIT () in
+  let after = delay (fun () -> pr_info_nop d; Proofview.tclUNIT ()) in
   Tacticals.New.tclORELSE0 tac after
 
 (**************************************************************************)
@@ -293,21 +293,19 @@ let tclTRY_dbg d tac =
 (* Papageno : cette fonction a été pas mal simplifiée depuis que la base
   de Hint impérative a été remplacée par plusieurs bases fonctionnelles *)
 
-let auto_unif_flags =
-  auto_unif_flags_of full_transparent_state empty_transparent_state false
-
 let flags_of_state st =
   auto_unif_flags_of st st false
 
 let auto_flags_of_state st =
   auto_unif_flags_of full_transparent_state st false
 
-let hintmap_of hdc concl =
+let hintmap_of secvars hdc concl =
   match hdc with
-  | None -> Hint_db.map_none
+  | None -> Hint_db.map_none ~secvars
   | Some hdc ->
-      if occur_existential concl then Hint_db.map_existential hdc concl
-      else Hint_db.map_auto hdc concl
+     if occur_existential concl then
+       Hint_db.map_existential ~secvars hdc concl
+     else Hint_db.map_auto ~secvars hdc concl
 
 let exists_evaluable_reference env = function
   | EvalConstRef _ -> true
@@ -319,35 +317,36 @@ let dbg_assumption dbg = tclLOG dbg (fun () -> str "assumption") assumption
 let rec trivial_fail_db dbg mod_delta db_list local_db =
   let intro_tac =
     Tacticals.New.tclTHEN (dbg_intro dbg)
-      ( Proofview.Goal.enter begin fun gl ->
-          let sigma = Proofview.Goal.sigma gl in
+      ( Proofview.Goal.enter { enter = begin fun gl ->
+          let sigma = Tacmach.New.project gl in
           let env = Proofview.Goal.env gl in
           let nf c = Evarutil.nf_evar sigma c in
           let decl = Tacmach.New.pf_last_hyp (Proofview.Goal.assume gl) in
-          let hyp = Context.map_named_declaration nf decl in
+          let hyp = Context.Named.Declaration.map_constr nf decl in
 	  let hintl = make_resolve_hyp env sigma hyp
 	  in trivial_fail_db dbg mod_delta db_list
 	       (Hint_db.add_list env sigma hintl local_db)
-      end)
+      end })
   in
-  Proofview.Goal.enter begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     let concl = Tacmach.New.pf_nf_concl gl in
+    let secvars = compute_secvars gl in
     Tacticals.New.tclFIRST
       ((dbg_assumption dbg)::intro_tac::
           (List.map Tacticals.New.tclCOMPLETE
-             (trivial_resolve dbg mod_delta db_list local_db concl)))
-  end
+             (trivial_resolve dbg mod_delta db_list local_db secvars concl)))
+  end }
 
-and my_find_search_nodelta db_list local_db hdc concl =
+and my_find_search_nodelta db_list local_db secvars hdc concl =
   List.map (fun hint -> (None,hint))
-    (List.map_append (hintmap_of hdc concl) (local_db::db_list))
+    (List.map_append (hintmap_of secvars hdc concl) (local_db::db_list))
 
 and my_find_search mod_delta =
   if mod_delta then my_find_search_delta
   else my_find_search_nodelta
 
-and my_find_search_delta db_list local_db hdc concl =
-  let f = hintmap_of hdc concl in
+and my_find_search_delta db_list local_db secvars hdc concl =
+  let f = hintmap_of secvars hdc concl in
     if occur_existential concl then
       List.map_append
 	(fun db ->
@@ -367,16 +366,16 @@ and my_find_search_delta db_list local_db hdc concl =
 	  let (ids, csts as st) = Hint_db.transparent_state db in
 	  let flags, l =
 	    let l =
-	      match hdc with None -> Hint_db.map_none db
+	      match hdc with None -> Hint_db.map_none ~secvars db
 	      | Some hdc ->
 		  if (Id.Pred.is_empty ids && Cpred.is_empty csts)
-		  then Hint_db.map_auto hdc concl db
-		  else Hint_db.map_existential hdc concl db
+		  then Hint_db.map_auto ~secvars hdc concl db
+		  else Hint_db.map_existential ~secvars hdc concl db
 	    in auto_flags_of_state st, l
 	  in List.map (fun x -> (Some flags,x)) l)
       	(local_db::db_list)
 
-and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly})) =
+and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=dbname})) =
   let tactic = function
     | Res_pf (c,cl) -> unify_resolve_gen poly flags (c,cl)
     | ERes_pf _ -> Proofview.V82.tactic (fun gl -> error "eres_pf")
@@ -390,14 +389,21 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly}))
     | Unfold_nth c ->
       Proofview.V82.tactic (fun gl ->
        if exists_evaluable_reference (pf_env gl) c then
-	 tclPROGRESS (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl) gl
+	 tclPROGRESS (Proofview.V82.of_tactic (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl)) gl
        else tclFAIL 0 (str"Unbound reference") gl)
     | Extern tacast -> 
       conclPattern concl p tacast
   in
-  tclLOG dbg (fun () -> pr_hint t) (run_hint t tactic)
+  let pr_hint () =
+    let origin = match dbname with
+    | None -> mt ()
+    | Some n -> str " (in " ++ str n ++ str ")"
+    in
+    pr_hint t ++ origin
+  in
+  tclLOG dbg pr_hint (run_hint t tactic)
 
-and trivial_resolve dbg mod_delta db_list local_db cl =
+and trivial_resolve dbg mod_delta db_list local_db secvars cl =
   try
     let head =
       try let hdconstr = decompose_app_bound cl in
@@ -406,33 +412,33 @@ and trivial_resolve dbg mod_delta db_list local_db cl =
     in
       List.map (tac_of_hint dbg db_list local_db cl)
 	(priority
-	    (my_find_search mod_delta db_list local_db head cl))
+	    (my_find_search mod_delta db_list local_db secvars head cl))
   with Not_found -> []
 
 (** The use of the "core" database can be de-activated by passing
     "nocore" amongst the databases. *)
 
 let trivial ?(debug=Off) lems dbnames =
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
-  let sigma = Proofview.Goal.sigma gl in
+  let sigma = Tacmach.New.project gl in
   let db_list = make_db_list dbnames in
   let d = mk_trivial_dbg debug in
   let hints = make_local_hint_db env sigma false lems in
   tclTRY_dbg d
     (trivial_fail_db d false db_list hints)
-  end
+  end }
 
 let full_trivial ?(debug=Off) lems =
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
-  let sigma = Proofview.Goal.sigma gl in
+  let sigma = Tacmach.New.project gl in
   let db_list = current_pure_db () in
   let d = mk_trivial_dbg debug in
   let hints = make_local_hint_db env sigma false lems in
   tclTRY_dbg d
     (trivial_fail_db d false db_list hints)
-  end
+  end }
 
 let gen_trivial ?(debug=Off) lems = function
   | None -> full_trivial ~debug lems
@@ -444,7 +450,7 @@ let h_trivial ?(debug=Off) lems l = gen_trivial ~debug lems l
 (*                       The classical Auto tactic                        *)
 (**************************************************************************)
 
-let possible_resolve dbg mod_delta db_list local_db cl =
+let possible_resolve dbg mod_delta db_list local_db secvars cl =
   try
     let head =
       try let hdconstr = decompose_app_bound cl in
@@ -452,12 +458,12 @@ let possible_resolve dbg mod_delta db_list local_db cl =
       with Bound -> None
     in
       List.map (tac_of_hint dbg db_list local_db cl)
-	(my_find_search mod_delta db_list local_db head cl)
+	(my_find_search mod_delta db_list local_db secvars head cl)
   with Not_found -> []
 
 let extend_local_db decl db gl =
   let env = Tacmach.New.pf_env gl in
-  let sigma = Proofview.Goal.sigma gl in
+  let sigma = Tacmach.New.project gl in
   Hint_db.add_list env sigma (make_resolve_hyp env sigma decl) db
 
 (* Introduce an hypothesis, then call the continuation tactic [kont]
@@ -465,10 +471,10 @@ let extend_local_db decl db gl =
 
 let intro_register dbg kont db =
   Tacticals.New.tclTHEN (dbg_intro dbg)
-    (Proofview.Goal.enter begin fun gl ->
+    (Proofview.Goal.enter { enter = begin fun gl ->
       let extend_local_db decl db = extend_local_db decl db gl in
       Tacticals.New.onLastDecl (fun decl -> kont (extend_local_db decl db))
-    end)
+    end })
 
 (* n is the max depth of search *)
 (* local_db contains the local Hypotheses *)
@@ -481,14 +487,15 @@ let search d n mod_delta db_list local_db =
       if Int.equal n 0 then Tacticals.New.tclZEROMSG (str"BOUND 2") else
         Tacticals.New.tclORELSE0 (dbg_assumption d)
 	  (Tacticals.New.tclORELSE0 (intro_register d (search d n) local_db)
-	     ( Proofview.Goal.enter begin fun gl ->
+	     ( Proofview.Goal.enter { enter = begin fun gl ->
                let concl = Tacmach.New.pf_nf_concl gl in
+               let secvars = compute_secvars gl in
 	       let d' = incr_dbg d in
 	       Tacticals.New.tclFIRST
 	         (List.map
 		    (fun ntac -> Tacticals.New.tclTHEN ntac (search d' (n-1) local_db))
-		    (possible_resolve d mod_delta db_list local_db concl))
-             end))
+		    (possible_resolve d mod_delta db_list local_db secvars concl))
+             end }))
     end []
   in
   search d n local_db
@@ -496,15 +503,15 @@ let search d n mod_delta db_list local_db =
 let default_search_depth = ref 5
 
 let delta_auto debug mod_delta n lems dbnames =
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
-  let sigma = Proofview.Goal.sigma gl in
+  let sigma = Tacmach.New.project gl in
   let db_list = make_db_list dbnames in
   let d = mk_auto_dbg debug in
   let hints = make_local_hint_db env sigma false lems in
   tclTRY_dbg d
     (search d n mod_delta db_list hints)
-  end
+  end }
 
 let delta_auto = 
   if Flags.profile then
@@ -519,15 +526,15 @@ let new_auto ?(debug=Off) n = delta_auto debug true n
 let default_auto = auto !default_search_depth [] []
 
 let delta_full_auto ?(debug=Off) mod_delta n lems =
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
-  let sigma = Proofview.Goal.sigma gl in
+  let sigma = Tacmach.New.project gl in
   let db_list = current_pure_db () in
   let d = mk_auto_dbg debug in
   let hints = make_local_hint_db env sigma false lems in
   tclTRY_dbg d
     (search d n mod_delta db_list hints)
-  end
+  end }
 
 let full_auto ?(debug=Off) n = delta_full_auto ~debug false n
 let new_full_auto ?(debug=Off) n = delta_full_auto ~debug true n