Merge branch 'v8.6'

5 files changed, 444 insertions, 12 deletions

diff --git a/ltac/ltac.mllib b/ltac/ltac.mllib
index 65ed114cf..fc51e48ae 100644
--- a/ltac/ltac.mllib
+++ b/ltac/ltac.mllib
@@ -1,3 +1,4 @@
+Taccoerce
 Tacsubst
 Tacenv
 Tactic_debug
diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml
index f332e1a0d..bea02e3dc 100644
--- a/ltac/profile_ltac.ml
+++ b/ltac/profile_ltac.ml
@@ -139,7 +139,7 @@ let string_of_call ck =
   let s =
   string_of_ppcmds
     (match ck with
-       | Tacexpr.LtacNotationCall s -> Names.KerName.print s
+       | Tacexpr.LtacNotationCall s -> Pptactic.pr_alias_key s
        | Tacexpr.LtacNameCall cst -> Pptactic.pr_ltac_constant cst
        | Tacexpr.LtacVarCall (id, t) -> Nameops.pr_id id
        | Tacexpr.LtacAtomCall te ->
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index 47c78ae5c..7acad20d2 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -1440,17 +1440,8 @@ let rewrite_with l2r flags c occs : strategy = { strategy =
   fun ({ state = () } as input) ->
     let unify env evars t =
       let (sigma, cstrs) = evars in
-      let ans =
-        try Some (refresh_hypinfo env sigma c)
-        with e when Class_tactics.catchable e -> None
-      in
-      match ans with
-      | None -> None
-      | Some (sigma, rew) ->
-        let rew = unify_eqn rew l2r flags env (sigma, cstrs) None t in
-        match rew with
-        | None -> None
-        | Some rew -> Some rew
+      let (sigma, rew) = refresh_hypinfo env sigma c in
+      unify_eqn rew l2r flags env (sigma, cstrs) None t
     in
     let app = apply_rule unify occs in
     let strat = 
diff --git a/ltac/taccoerce.ml b/ltac/taccoerce.ml
new file mode 100644
index 000000000..0110510d3
--- /dev/null
+++ b/ltac/taccoerce.ml
@@ -0,0 +1,344 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Util
+open Names
+open Term
+open Pattern
+open Misctypes
+open Genarg
+open Stdarg
+open Constrarg
+open Geninterp
+
+exception CannotCoerceTo of string
+
+let (wit_constr_context : (Empty.t, Empty.t, constr) Genarg.genarg_type) =
+  let wit = Genarg.create_arg "constr_context" in
+  let () = register_val0 wit None in
+  wit
+
+(* includes idents known to be bound and references *)
+let (wit_constr_under_binders : (Empty.t, Empty.t, constr_under_binders) Genarg.genarg_type) =
+  let wit = Genarg.create_arg "constr_under_binders" in
+  let () = register_val0 wit None in
+  wit
+
+(** All the types considered here are base types *)
+let val_tag wit = match val_tag wit with
+| Val.Base t -> t
+| _ -> assert false
+
+let has_type : type a. Val.t -> a typed_abstract_argument_type -> bool = fun v wit ->
+  let Val.Dyn (t, _) = v in
+  match Val.eq t (val_tag wit) with
+  | None -> false
+  | Some Refl -> true
+
+let prj : type a. a Val.typ -> Val.t -> a option = fun t v ->
+  let Val.Dyn (t', x) = v in
+  match Val.eq t t' with
+  | None -> None
+  | Some Refl -> Some x
+
+let in_gen wit v = Val.Dyn (val_tag wit, v)
+let out_gen wit v = match prj (val_tag wit) v with None -> assert false | Some x -> x
+
+module Value =
+struct
+
+type t = Val.t
+
+let normalize v = v
+
+let of_constr c = in_gen (topwit wit_constr) c
+
+let to_constr v =
+  let v = normalize v in
+  if has_type v (topwit wit_constr) then
+    let c = out_gen (topwit wit_constr) v in
+    Some c
+  else if has_type v (topwit wit_constr_under_binders) then
+    let vars, c = out_gen (topwit wit_constr_under_binders) v in
+    match vars with [] -> Some c | _ -> None
+  else None
+
+let of_uconstr c = in_gen (topwit wit_uconstr) c
+
+let to_uconstr v =
+  let v = normalize v in
+  if has_type v (topwit wit_uconstr) then
+    Some (out_gen (topwit wit_uconstr) v)
+  else None
+
+let of_int i = in_gen (topwit wit_int) i
+
+let to_int v =
+  let v = normalize v in
+  if has_type v (topwit wit_int) then
+    Some (out_gen (topwit wit_int) v)
+  else None
+
+let to_list v = prj Val.typ_list v
+
+let to_option v = prj Val.typ_opt v
+
+let to_pair v = prj Val.typ_pair v
+
+end
+
+let is_variable env id =
+  Id.List.mem id (Termops.ids_of_named_context (Environ.named_context env))
+
+(* Transforms an id into a constr if possible, or fails with Not_found *)
+let constr_of_id env id =
+  Term.mkVar (let _ = Environ.lookup_named id env in id)
+
+(* Gives the constr corresponding to a Constr_context tactic_arg *)
+let coerce_to_constr_context v =
+  let v = Value.normalize v in
+  if has_type v (topwit wit_constr_context) then
+    out_gen (topwit wit_constr_context) v
+  else raise (CannotCoerceTo "a term context")
+
+(* Interprets an identifier which must be fresh *)
+let coerce_var_to_ident fresh env v =
+  let v = Value.normalize v in
+  let fail () = raise (CannotCoerceTo "a fresh identifier") in
+  if has_type v (topwit wit_intro_pattern) then
+    match out_gen (topwit wit_intro_pattern) v with
+    | _, IntroNaming (IntroIdentifier id) -> id
+    | _ -> fail ()
+  else if has_type v (topwit wit_var) then
+    out_gen (topwit wit_var) v
+  else match Value.to_constr v with
+  | None -> fail ()
+  | Some c ->
+    (* We need it fresh for intro e.g. in "Tac H = clear H; intro H" *)
+    if isVar c && not (fresh && is_variable env (destVar c)) then
+      destVar c
+    else fail ()
+
+
+(* Interprets, if possible, a constr to an identifier which may not
+   be fresh but suitable to be given to the fresh tactic. Works for
+   vars, constants, inductive, constructors and sorts. *)
+let coerce_to_ident_not_fresh g env v =
+let id_of_name = function
+  | Names.Anonymous -> Id.of_string "x"
+  | Names.Name x -> x in
+  let v = Value.normalize v in
+  let fail () = raise (CannotCoerceTo "an identifier") in
+  if has_type v (topwit wit_intro_pattern) then
+    match out_gen (topwit wit_intro_pattern) v with
+    | _, IntroNaming (IntroIdentifier id) -> id
+    | _ -> fail ()
+  else if has_type v (topwit wit_var) then
+    out_gen (topwit wit_var) v
+  else
+    match Value.to_constr v with
+    | None -> fail ()
+    | Some c ->
+       match Constr.kind c with
+       | Var id -> id 
+       | Meta m -> id_of_name (Evd.meta_name g m)
+       | Evar (kn,_) ->
+        begin match Evd.evar_ident kn g with
+        | None -> fail ()
+        | Some id -> id
+        end
+       | Const (cst,_) -> Label.to_id (Constant.label cst)
+       | Construct (cstr,_) ->
+	  let ref = Globnames.ConstructRef cstr in
+	  let basename = Nametab.basename_of_global ref in
+	  basename
+       | Ind (ind,_) ->
+	  let ref = Globnames.IndRef ind in
+	  let basename = Nametab.basename_of_global ref in
+	  basename
+       | Sort s ->
+	  begin
+	    match s with
+	    | Prop _ -> Label.to_id (Label.make "Prop")
+	    | Type _ -> Label.to_id (Label.make "Type")
+	  end
+       | _ -> fail()
+
+
+let coerce_to_intro_pattern env v =
+  let v = Value.normalize v in
+  if has_type v (topwit wit_intro_pattern) then
+    snd (out_gen (topwit wit_intro_pattern) v)
+  else if has_type v (topwit wit_var) then
+    let id = out_gen (topwit wit_var) v in
+    IntroNaming (IntroIdentifier id)
+  else match Value.to_constr v with
+  | Some c when isVar c ->
+      (* This happens e.g. in definitions like "Tac H = clear H; intro H" *)
+      (* but also in "destruct H as (H,H')" *)
+      IntroNaming (IntroIdentifier (destVar c))
+  | _ -> raise (CannotCoerceTo "an introduction pattern")
+
+let coerce_to_intro_pattern_naming env v =
+  match coerce_to_intro_pattern env v with
+  | IntroNaming pat -> pat
+  | _ -> raise (CannotCoerceTo "a naming introduction pattern")
+
+let coerce_to_hint_base v =
+  let v = Value.normalize v in
+  if has_type v (topwit wit_intro_pattern) then
+    match out_gen (topwit wit_intro_pattern) v with
+    | _, IntroNaming (IntroIdentifier id) -> Id.to_string id
+    | _ -> raise (CannotCoerceTo "a hint base name")
+  else raise (CannotCoerceTo "a hint base name")
+
+let coerce_to_int v =
+  let v = Value.normalize v in
+  if has_type v (topwit wit_int) then
+    out_gen (topwit wit_int) v
+  else raise (CannotCoerceTo "an integer")
+
+let coerce_to_constr env v =
+  let v = Value.normalize v in
+  let fail () = raise (CannotCoerceTo "a term") in
+  if has_type v (topwit wit_intro_pattern) then
+    match out_gen (topwit wit_intro_pattern) v with
+    | _, IntroNaming (IntroIdentifier id) ->
+      (try ([], constr_of_id env id) with Not_found -> fail ())
+    | _ -> fail ()
+  else if has_type v (topwit wit_constr) then
+    let c = out_gen (topwit wit_constr) v in
+    ([], c)
+  else if has_type v (topwit wit_constr_under_binders) then
+    out_gen (topwit wit_constr_under_binders) v
+  else if has_type v (topwit wit_var) then
+    let id = out_gen (topwit wit_var) v in
+    (try [], constr_of_id env id with Not_found -> fail ())
+  else fail ()
+
+let coerce_to_uconstr env v =
+  let v = Value.normalize v in
+  if has_type v (topwit wit_uconstr) then
+    out_gen (topwit wit_uconstr) v
+  else
+    raise (CannotCoerceTo "an untyped term")
+
+let coerce_to_closed_constr env v =
+  let ids,c = coerce_to_constr env v in
+  let () = if not (List.is_empty ids) then raise (CannotCoerceTo "a term") in
+  c
+
+let coerce_to_evaluable_ref env v =
+  let fail () = raise (CannotCoerceTo "an evaluable reference") in
+  let v = Value.normalize v in
+  if has_type v (topwit wit_intro_pattern) then
+    match out_gen (topwit wit_intro_pattern) v with
+    | _, IntroNaming (IntroIdentifier id) when is_variable env id -> EvalVarRef id
+    | _ -> fail ()
+  else if has_type v (topwit wit_var) then
+    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))
+    | Some c when isVar c -> EvalVarRef (destVar c)
+    | _ -> fail ()
+    in
+    if Tacred.is_evaluable env ev then ev else fail ()
+
+let coerce_to_constr_list env v =
+  let v = Value.to_list v in
+  match v with
+  | Some l ->
+    let map v = coerce_to_closed_constr env v in
+    List.map map l
+  | None -> raise (CannotCoerceTo "a term list")
+
+let coerce_to_intro_pattern_list loc env v =
+  match Value.to_list v with
+  | None -> raise (CannotCoerceTo "an intro pattern list")
+  | Some l ->
+    let map v = (loc, coerce_to_intro_pattern env v) in
+    List.map map l
+
+let coerce_to_hyp env v =
+  let fail () = raise (CannotCoerceTo "a variable") in
+  let v = Value.normalize v in
+  if has_type v (topwit wit_intro_pattern) then
+    match out_gen (topwit wit_intro_pattern) v with
+    | _, IntroNaming (IntroIdentifier id) when is_variable env id -> id
+    | _ -> fail ()
+  else if has_type v (topwit wit_var) then
+    let id = out_gen (topwit wit_var) v in
+    if is_variable env id then id else fail ()
+  else match Value.to_constr v with
+  | Some c when isVar c -> destVar c
+  | _ -> fail ()
+
+let coerce_to_hyp_list env v =
+  let v = Value.to_list v in
+  match v with
+  | Some l ->
+    let map n = coerce_to_hyp env n in
+    List.map map l
+  | None -> raise (CannotCoerceTo "a variable list")
+
+(* Interprets a qualified name *)
+let coerce_to_reference env v =
+  let v = Value.normalize v in
+  match Value.to_constr v with
+  | Some c ->
+    begin
+      try Globnames.global_of_constr c
+      with Not_found -> raise (CannotCoerceTo "a reference")
+    end
+  | None -> raise (CannotCoerceTo "a reference")
+
+(* Quantified named or numbered hypothesis or hypothesis in context *)
+(* (as in Inversion) *)
+let coerce_to_quantified_hypothesis v =
+  let v = Value.normalize v in
+  if has_type v (topwit wit_intro_pattern) then
+    let v = out_gen (topwit wit_intro_pattern) v in
+    match v with
+    | _, IntroNaming (IntroIdentifier id) -> NamedHyp id
+    | _ -> raise (CannotCoerceTo "a quantified hypothesis")
+  else if has_type v (topwit wit_var) then
+    let id = out_gen (topwit wit_var) v in
+    NamedHyp id
+  else if has_type v (topwit wit_int) then
+    AnonHyp (out_gen (topwit wit_int) v)
+  else match Value.to_constr v with
+  | Some c when isVar c -> NamedHyp (destVar c)
+  | _ -> raise (CannotCoerceTo "a quantified hypothesis")
+
+(* Quantified named or numbered hypothesis or hypothesis in context *)
+(* (as in Inversion) *)
+let coerce_to_decl_or_quant_hyp env v =
+  let v = Value.normalize v in
+  if has_type v (topwit wit_int) then
+    AnonHyp (out_gen (topwit wit_int) v)
+  else
+    try coerce_to_quantified_hypothesis v
+    with CannotCoerceTo _ ->
+      raise (CannotCoerceTo "a declared or quantified hypothesis")
+
+let coerce_to_int_or_var_list v =
+  match Value.to_list v with
+  | None -> raise (CannotCoerceTo "an int list")
+  | Some l ->
+    let map n = ArgArg (coerce_to_int n) in
+    List.map map l
diff --git a/ltac/taccoerce.mli b/ltac/taccoerce.mli
new file mode 100644
index 000000000..0b67f8726
--- /dev/null
+++ b/ltac/taccoerce.mli
@@ -0,0 +1,96 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Util
+open Names
+open Term
+open Misctypes
+open Pattern
+open Genarg
+open Geninterp
+
+(** Coercions from highest level generic arguments to actual data used by Ltac
+    interpretation. Those functions examinate dynamic types and try to return
+    something sensible according to the object content. *)
+
+exception CannotCoerceTo of string
+(** Exception raised whenever a coercion failed. *)
+
+(** {5 High-level access to values}
+
+  The [of_*] functions cast a given argument into a value. The [to_*] do the
+  converse, and return [None] if there is a type mismatch.
+
+*)
+
+module Value :
+sig
+  type t = Val.t
+
+  val normalize : t -> t
+  (** Eliminated the leading dynamic type casts. *)
+
+  val of_constr : constr -> t
+  val to_constr : t -> constr option
+  val of_uconstr : Glob_term.closed_glob_constr -> t
+  val to_uconstr : t -> Glob_term.closed_glob_constr option
+  val of_int : int -> t
+  val to_int : t -> int option
+  val to_list : t -> t list option
+  val to_option : t -> t option option
+  val to_pair : t -> (t * t) option
+end
+
+(** {5 Coercion functions} *)
+
+val coerce_to_constr_context : Value.t -> constr
+
+val coerce_var_to_ident : bool -> Environ.env -> Value.t -> Id.t
+
+val coerce_to_ident_not_fresh : Evd.evar_map -> Environ.env -> Value.t -> Id.t
+
+val coerce_to_intro_pattern : Environ.env -> Value.t -> Tacexpr.delayed_open_constr intro_pattern_expr
+
+val coerce_to_intro_pattern_naming :
+  Environ.env -> Value.t -> intro_pattern_naming_expr
+
+val coerce_to_hint_base : Value.t -> string
+
+val coerce_to_int : Value.t -> int
+
+val coerce_to_constr : Environ.env -> Value.t -> constr_under_binders
+
+val coerce_to_uconstr : Environ.env -> Value.t -> Glob_term.closed_glob_constr
+
+val coerce_to_closed_constr : Environ.env -> Value.t -> constr
+
+val coerce_to_evaluable_ref :
+  Environ.env -> Value.t -> evaluable_global_reference
+
+val coerce_to_constr_list : Environ.env -> Value.t -> constr list
+
+val coerce_to_intro_pattern_list :
+  Loc.t -> Environ.env -> Value.t -> Tacexpr.intro_patterns
+
+val coerce_to_hyp : Environ.env -> Value.t -> Id.t
+
+val coerce_to_hyp_list : Environ.env -> Value.t -> Id.t list
+
+val coerce_to_reference : Environ.env -> Value.t -> Globnames.global_reference
+
+val coerce_to_quantified_hypothesis : Value.t -> quantified_hypothesis
+
+val coerce_to_decl_or_quant_hyp : Environ.env -> Value.t -> quantified_hypothesis
+
+val coerce_to_int_or_var_list : Value.t -> int or_var list
+
+(** {5 Missing generic arguments} *)
+
+val wit_constr_context : (Empty.t, Empty.t, constr) genarg_type
+
+val wit_constr_under_binders : (Empty.t, Empty.t, constr_under_binders) genarg_type