Eradicating uses of open_constr in TACTIC EXTEND in favour of uconstr.

7 files changed, 102 insertions, 71 deletions

diff --git a/tactics/auto.mli b/tactics/auto.mli
index 1132478aa..eca592ad6 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -44,24 +44,24 @@ val conclPattern : constr -> constr_pattern option -> Tacexpr.glob_tactic_expr -
     "nocore" amongst the databases. *)
 
 val auto : ?debug:Tacexpr.debug ->
-  int -> open_constr list -> hint_db_name list -> unit Proofview.tactic
+  int -> Tacexpr.delayed_open_constr list -> hint_db_name list -> unit Proofview.tactic
 
 (** Auto with more delta. *)
 
 val new_auto : ?debug:Tacexpr.debug ->
-  int -> open_constr list -> hint_db_name list -> unit Proofview.tactic
+  int -> Tacexpr.delayed_open_constr list -> hint_db_name list -> unit Proofview.tactic
 
 (** auto with default search depth and with the hint database "core" *)
 val default_auto : unit Proofview.tactic
 
 (** auto with all hint databases except the "v62" compatibility database *)
 val full_auto : ?debug:Tacexpr.debug ->
-  int -> open_constr list -> unit Proofview.tactic
+  int -> Tacexpr.delayed_open_constr list -> unit Proofview.tactic
 
 (** auto with all hint databases except the "v62" compatibility database
    and doing delta *)
 val new_full_auto : ?debug:Tacexpr.debug ->
-  int -> open_constr list -> unit Proofview.tactic
+  int -> Tacexpr.delayed_open_constr list -> unit Proofview.tactic
 
 (** auto with default search depth and with all hint databases
    except the "v62" compatibility database *)
@@ -69,19 +69,19 @@ val default_full_auto : unit Proofview.tactic
 
 (** The generic form of auto (second arg [None] means all bases) *)
 val gen_auto : ?debug:Tacexpr.debug ->
-  int option -> open_constr list -> hint_db_name list option -> unit Proofview.tactic
+  int option -> Tacexpr.delayed_open_constr list -> hint_db_name list option -> unit Proofview.tactic
 
 (** The hidden version of auto *)
 val h_auto   : ?debug:Tacexpr.debug ->
-  int option -> open_constr list -> hint_db_name list option -> unit Proofview.tactic
+  int option -> Tacexpr.delayed_open_constr list -> hint_db_name list option -> unit Proofview.tactic
 
 (** Trivial *)
 
 val trivial : ?debug:Tacexpr.debug ->
-  open_constr list -> hint_db_name list -> unit Proofview.tactic
+  Tacexpr.delayed_open_constr list -> hint_db_name list -> unit Proofview.tactic
 val gen_trivial : ?debug:Tacexpr.debug ->
-  open_constr list -> hint_db_name list option -> unit Proofview.tactic
+  Tacexpr.delayed_open_constr list -> hint_db_name list option -> unit Proofview.tactic
 val full_trivial : ?debug:Tacexpr.debug ->
-  open_constr list -> unit Proofview.tactic
+  Tacexpr.delayed_open_constr list -> unit Proofview.tactic
 val h_trivial : ?debug:Tacexpr.debug ->
-  open_constr list -> hint_db_name list option -> unit Proofview.tactic
+  Tacexpr.delayed_open_constr list -> hint_db_name list option -> unit Proofview.tactic
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 1943a4f1f..fe10b92c3 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -64,6 +64,16 @@ let registered_e_assumption =
               (Tacmach.New.pf_ids_of_hyps gl))
   end }
 
+let eval_uconstrs ist cs =
+  let flags = {
+    Pretyping.use_typeclasses = false;
+    use_unif_heuristics = true;
+    use_hook = Some Pfedit.solve_by_implicit_tactic;
+    fail_evar = false;
+    expand_evars = true
+  } in
+  List.map (fun c -> Tacinterp.type_uconstr ~flags ist c) cs
+
 (************************************************************************)
 (*   PROLOG tactic                                                      *)
 (************************************************************************)
@@ -103,13 +113,19 @@ let out_term = function
   | IsGlobRef gr -> fst (Universes.fresh_global_instance (Global.env ()) gr)
 
 let prolog_tac l n gl =
-  let l = List.map (fun x -> out_term (pf_apply (prepare_hint false (false,true)) gl x)) l in
+  let map c =
+    let (c, sigma) = Tactics.run_delayed (pf_env gl) (project gl) c in
+    let c = pf_apply (prepare_hint false (false,true)) gl (sigma, c) in
+    out_term c
+  in
+  let l = List.map map l in
   try (prolog l n gl)
   with UserError ("Refiner.tclFIRST",_) ->
     errorlabstrm "Prolog.prolog" (str "Prolog failed.")
 
 TACTIC EXTEND prolog
-| [ "prolog" "[" open_constr_list(l) "]" int_or_var(n) ] -> [ Proofview.V82.tactic (prolog_tac l n) ]
+| [ "prolog" "[" uconstr_list(l) "]" int_or_var(n) ] ->
+    [ Proofview.V82.tactic (prolog_tac (eval_uconstrs ist l) n) ]
 END
 
 open Auto
@@ -214,7 +230,7 @@ type search_state = {
   dblist : hint_db list;
   localdb :  hint_db list;
   prev : prev_search_state;
-  local_lemmas : Evd.open_constr list;
+  local_lemmas : Tacexpr.delayed_open_constr list;
 }
 
 and prev_search_state = (* for info eauto *)
@@ -446,33 +462,33 @@ let wit_hintbases = G_auto.wit_hintbases
 TACTIC EXTEND eauto
 | [ "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
     hintbases(db) ] ->
-    [ Proofview.V82.tactic (gen_eauto (make_dimension n p) lems db) ]
+    [ Proofview.V82.tactic (gen_eauto (make_dimension n p) (eval_uconstrs ist lems) db) ]
 END
 
 TACTIC EXTEND new_eauto
 | [ "new" "auto" int_or_var_opt(n) auto_using(lems)
     hintbases(db) ] ->
     [ match db with
-      | None -> new_full_auto (make_depth n) lems
-      | Some l -> new_auto (make_depth n) lems l ]
+      | None -> new_full_auto (make_depth n) (eval_uconstrs ist lems)
+      | Some l -> new_auto (make_depth n) (eval_uconstrs ist lems) l ]
 END
 
 TACTIC EXTEND debug_eauto
 | [ "debug" "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
     hintbases(db) ] ->
-    [ Proofview.V82.tactic (gen_eauto ~debug:Debug (make_dimension n p) lems db) ]
+    [ Proofview.V82.tactic (gen_eauto ~debug:Debug (make_dimension n p) (eval_uconstrs ist lems) db) ]
 END
 
 TACTIC EXTEND info_eauto
 | [ "info_eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
     hintbases(db) ] ->
-    [ Proofview.V82.tactic (gen_eauto ~debug:Info (make_dimension n p) lems db) ]
+    [ Proofview.V82.tactic (gen_eauto ~debug:Info (make_dimension n p) (eval_uconstrs ist lems) db) ]
 END
 
 TACTIC EXTEND dfs_eauto
 | [ "dfs" "eauto" int_or_var_opt(p) auto_using(lems)
       hintbases(db) ] ->
-    [ Proofview.V82.tactic (gen_eauto (true, make_depth p) lems db) ]
+    [ Proofview.V82.tactic (gen_eauto (true, make_depth p) (eval_uconstrs ist lems) db) ]
 END
 
 let cons a l = a :: l
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index 3d02081bf..8e20793c4 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -21,12 +21,12 @@ val registered_e_assumption : unit Proofview.tactic
 
 val e_give_exact : ?flags:Unification.unify_flags -> constr -> unit Proofview.tactic
 
-val gen_eauto : ?debug:Tacexpr.debug -> bool * int -> open_constr list ->
+val gen_eauto : ?debug:Tacexpr.debug -> bool * int -> Tacexpr.delayed_open_constr list ->
   hint_db_name list option -> tactic
 
 val eauto_with_bases :
   ?debug:Tacexpr.debug ->
   bool * int ->
-  open_constr list -> hint_db list -> Proof_type.tactic
+  Tacexpr.delayed_open_constr list -> hint_db list -> Proof_type.tactic
 
 val autounfold : hint_db_name list -> Locus.clause -> tactic
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 8a5267541..a957a5624 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -31,34 +31,42 @@ DECLARE PLUGIN "extratactics"
 (* replace, discriminate, injection, simplify_eq                      *)
 (* cutrewrite, dependent rewrite                                      *)
 
-let replace_in_clause_maybe_by (sigma1,c1) c2 cl  tac =
-  Tacticals.New.tclWITHHOLES false
-    (replace_in_clause_maybe_by c1 c2 cl (Option.map Tacinterp.eval_tactic tac))
-    sigma1
-
-let replace_term dir_opt (sigma,c) cl =
-  Tacticals.New.tclWITHHOLES false
-    (replace_term dir_opt c cl)
-    sigma
+let with_delayed_uconstr ist c tac =
+  let flags = {
+    Pretyping.use_typeclasses = false;
+    use_unif_heuristics = true;
+    use_hook = Some Pfedit.solve_by_implicit_tactic;
+    fail_evar = false;
+    expand_evars = true
+  } in
+  let c = Tacinterp.type_uconstr ~flags ist c in
+  Tacticals.New.tclDELAYEDWITHHOLES false c tac
+
+let replace_in_clause_maybe_by ist c1 c2 cl tac =
+  with_delayed_uconstr ist c1
+  (fun c1 -> replace_in_clause_maybe_by c1 c2 cl (Option.map Tacinterp.eval_tactic tac))
+
+let replace_term ist dir_opt c cl =
+  with_delayed_uconstr ist c (fun c -> replace_term dir_opt c cl)
 
 TACTIC EXTEND replace
-   ["replace" open_constr(c1) "with" constr(c2) clause(cl) by_arg_tac(tac) ]
--> [ replace_in_clause_maybe_by c1 c2 cl tac ]
+   ["replace" uconstr(c1) "with" constr(c2) clause(cl) by_arg_tac(tac) ]
+-> [ replace_in_clause_maybe_by ist c1 c2 cl tac ]
 END
 
 TACTIC EXTEND replace_term_left
-  [ "replace"  "->" open_constr(c) clause(cl) ]
-  -> [ replace_term (Some true) c cl ]
+  [ "replace"  "->" uconstr(c) clause(cl) ]
+  -> [ replace_term ist (Some true) c cl ]
 END
 
 TACTIC EXTEND replace_term_right
-  [ "replace"  "<-" open_constr(c) clause(cl) ]
-  -> [ replace_term (Some false) c cl ]
+  [ "replace"  "<-" uconstr(c) clause(cl) ]
+  -> [ replace_term ist (Some false) c cl ]
 END
 
 TACTIC EXTEND replace_term
-  [ "replace" open_constr(c) clause(cl) ]
-  -> [ replace_term None c cl ]
+  [ "replace" uconstr(c) clause(cl) ]
+  -> [ replace_term ist None c cl ]
 END
 
 let induction_arg_of_quantified_hyp = function
@@ -243,22 +251,22 @@ END
 (**********************************************************************)
 (* Rewrite star                                                       *)
 
-let rewrite_star clause orient occs (sigma,c) (tac : glob_tactic_expr option) =
+let rewrite_star ist clause orient occs c (tac : glob_tactic_expr option) =
   let tac' = Option.map (fun t -> Tacinterp.eval_tactic t, FirstSolved) tac in
-  Tacticals.New.tclWITHHOLES false
-    (general_rewrite_ebindings_clause clause orient occs ?tac:tac' true true (c,NoBindings) true) sigma
+  with_delayed_uconstr ist c
+    (fun c -> general_rewrite_ebindings_clause clause orient occs ?tac:tac' true true (c,NoBindings) true)
 
 TACTIC EXTEND rewrite_star
-| [ "rewrite" "*" orient(o) open_constr(c) "in" hyp(id) "at" occurrences(occ) by_arg_tac(tac) ] ->
-    [ rewrite_star (Some id) o (occurrences_of occ) c tac ]
-| [ "rewrite" "*" orient(o) open_constr(c) "at" occurrences(occ) "in" hyp(id) by_arg_tac(tac) ] ->
-    [ rewrite_star (Some id) o (occurrences_of occ) c tac ]
-| [ "rewrite" "*" orient(o) open_constr(c) "in" hyp(id) by_arg_tac(tac) ] ->
-    [ rewrite_star (Some id) o Locus.AllOccurrences c tac ]
-| [ "rewrite" "*" orient(o) open_constr(c) "at" occurrences(occ) by_arg_tac(tac) ] ->
-    [ rewrite_star None o (occurrences_of occ) c tac ]
-| [ "rewrite" "*" orient(o) open_constr(c) by_arg_tac(tac) ] ->
-    [ rewrite_star None o Locus.AllOccurrences c tac ]
+| [ "rewrite" "*" orient(o) uconstr(c) "in" hyp(id) "at" occurrences(occ) by_arg_tac(tac) ] ->
+    [ rewrite_star ist (Some id) o (occurrences_of occ) c tac ]
+| [ "rewrite" "*" orient(o) uconstr(c) "at" occurrences(occ) "in" hyp(id) by_arg_tac(tac) ] ->
+    [ rewrite_star ist (Some id) o (occurrences_of occ) c tac ]
+| [ "rewrite" "*" orient(o) uconstr(c) "in" hyp(id) by_arg_tac(tac) ] ->
+    [ rewrite_star ist (Some id) o Locus.AllOccurrences c tac ]
+| [ "rewrite" "*" orient(o) uconstr(c) "at" occurrences(occ) by_arg_tac(tac) ] ->
+    [ rewrite_star ist None o (occurrences_of occ) c tac ]
+| [ "rewrite" "*" orient(o) uconstr(c) by_arg_tac(tac) ] ->
+    [ rewrite_star ist None o Locus.AllOccurrences c tac ]
     END
 
 (**********************************************************************)
diff --git a/tactics/g_auto.ml4 b/tactics/g_auto.ml4
index 7d35cfaab..3a2cee9f7 100644
--- a/tactics/g_auto.ml4
+++ b/tactics/g_auto.ml4
@@ -26,51 +26,51 @@ ARGUMENT EXTEND hintbases
 | [ ] -> [ Some [] ]
 END
 
-let pr_constr_coma_sequence prc _ _ =
-  prlist_with_sep pr_comma (fun (_,c) -> prc c)
-
-ARGUMENT EXTEND constr_coma_sequence
-  TYPED AS open_constr_list
-  PRINTED BY pr_constr_coma_sequence
-| [ open_constr(c) "," constr_coma_sequence(l) ] -> [ c::l ]
-| [ open_constr(c) ] -> [ [c] ]
-END
-
-let pr_auto_using prc _prlc _prt = Pptactic.pr_auto_using (fun (_,c) -> prc c)
+let eval_uconstrs ist cs =
+  let flags = {
+    Pretyping.use_typeclasses = false;
+    use_unif_heuristics = true;
+    use_hook = Some Pfedit.solve_by_implicit_tactic;
+    fail_evar = false;
+    expand_evars = true
+  } in
+  List.map (fun c -> Tacinterp.type_uconstr ~flags ist c) cs
+
+let pr_auto_using _ _ _ = Pptactic.pr_auto_using (fun _ -> mt ())
 
 ARGUMENT EXTEND auto_using
-  TYPED AS open_constr_list
+  TYPED AS uconstr_list
   PRINTED BY pr_auto_using
-| [ "using" constr_coma_sequence(l) ] -> [ l ]
+| [ "using" ne_uconstr_list_sep(l, ",") ] -> [ l ]
 | [ ] -> [ [] ]
 END
 
 TACTIC EXTEND trivial
 | [ "trivial" auto_using(lems) hintbases(db) ] ->
-    [ Auto.h_trivial lems db ]
+    [ Auto.h_trivial (eval_uconstrs ist lems) db ]
 END
 
 TACTIC EXTEND info_trivial
 | [ "info_trivial" auto_using(lems) hintbases(db) ] ->
-    [ Auto.h_trivial ~debug:Info lems db ]
+    [ Auto.h_trivial ~debug:Info (eval_uconstrs ist lems) db ]
 END
 
 TACTIC EXTEND debug_trivial
 | [ "debug" "trivial" auto_using(lems) hintbases(db) ] ->
-    [ Auto.h_trivial ~debug:Debug lems db ]
+    [ Auto.h_trivial ~debug:Debug (eval_uconstrs ist lems) db ]
 END
 
 TACTIC EXTEND auto
 | [ "auto" int_or_var_opt(n) auto_using(lems) hintbases(db) ] ->
-    [ Auto.h_auto n lems db ]
+    [ Auto.h_auto n (eval_uconstrs ist lems) db ]
 END
 
 TACTIC EXTEND info_auto
 | [ "info_auto" int_or_var_opt(n) auto_using(lems) hintbases(db) ] ->
-    [ Auto.h_auto ~debug:Info n lems db ]
+    [ Auto.h_auto ~debug:Info n (eval_uconstrs ist lems) db ]
 END
 
 TACTIC EXTEND debug_auto
 | [ "debug" "auto" int_or_var_opt(n) auto_using(lems) hintbases(db) ] ->
-    [ Auto.h_auto ~debug:Debug n lems db ]
+    [ Auto.h_auto ~debug:Debug n (eval_uconstrs ist lems) db ]
 END
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 625088682..6d623f1c3 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -33,6 +33,7 @@ open Pfedit
 open Tacred
 open Printer
 open Vernacexpr
+open Sigma.Notations
 
 (****************************************)
 (* General functions                    *)
@@ -1184,6 +1185,12 @@ let add_hint_lemmas env sigma eapply lems hint_db =
   Hint_db.add_list env sigma hintlist' hint_db
 
 let make_local_hint_db env sigma ts eapply lems =
+  let map c =
+    let sigma = Sigma.Unsafe.of_evar_map sigma in
+    let Sigma (c, sigma, _) = c.delayed env sigma in
+    (Sigma.to_evar_map sigma, c)
+  in
+  let lems = List.map map lems in
   let sign = Environ.named_context env in
   let ts = match ts with
     | None -> Hint_db.transparent_state (searchtable_map "core") 
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 3a0521f66..257598d18 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -214,7 +214,7 @@ val extern_intern_tac :
    Useful to take the current goal hypotheses as hints;
    Boolean tells if lemmas with evars are allowed *)
 
-val make_local_hint_db : env -> evar_map -> ?ts:transparent_state -> bool -> open_constr list -> hint_db
+val make_local_hint_db : env -> evar_map -> ?ts:transparent_state -> bool -> Tacexpr.delayed_open_constr list -> hint_db
 
 val make_db_list : hint_db_name list -> hint_db list