An experimental support for open constrs in hints and in "using"

option of "auto". Works for not too complicated hints (e.g. "@pair _ _ 0").
Would be simpler if make_apply_entry supported lemmas containing evars.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13598 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 21 insertions, 0 deletions

diff --git a/pretyping/namegen.mli b/pretyping/namegen.mli
index 8849c9ed3b..0c9fc4f6b5 100644
--- a/pretyping/namegen.mli
+++ b/pretyping/namegen.mli
@@ -39,6 +39,9 @@ val it_mkLambda_or_LetIn_name : env -> constr -> rel_context -> constr
 (*********************************************************************
    Fresh names *)
 
+(** Avoid clashing with a name satisfying some predicate *)
+val next_ident_away_from : identifier -> (identifier -> bool) -> identifier
+
 (** Avoid clashing with a name of the given list *)
 val next_ident_away : identifier -> identifier list -> identifier
 
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index d31242aa2b..9888821d14 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -262,6 +262,14 @@ let rec strip_head_cast c = match kind_of_term c with
   | Cast (c,_,_) -> strip_head_cast c
   | _ -> c
 
+let rec drop_extra_implicit_args c = match kind_of_term c with
+  (* Removed trailing extra implicit arguments, what improves compatibility
+     for constants with recently added maximal implicit arguments *)
+  | App (f,args) when isEvar (array_last args) ->
+      drop_extra_implicit_args
+	(mkApp (f,fst (array_chop (Array.length args - 1) args)))
+  | _ -> c
+
 (* Get the last arg of an application *)
 let last_arg c = match kind_of_term c with
   | App (f,cl) -> array_last cl
@@ -526,6 +534,14 @@ let collect_metas c =
   in
   List.rev (collrec [] c)
 
+(* collects all vars; warning: this is only visible vars, not dependencies in
+   all section variables; for the latter, use global_vars_set *)
+let collect_vars c =
+  let rec aux vars c = match kind_of_term c with
+  | Var id -> Idset.add id vars
+  | _ -> fold_constr aux vars c in
+  aux Idset.empty c
+
 (* Tests whether [m] is a subterm of [t]:
    [m] is appropriately lifted through abstractions of [t] *)
 
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 385bd3022a..1350743d5d 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -91,6 +91,7 @@ val iter_constr_with_full_binders :
 (**********************************************************************)
 
 val strip_head_cast : constr -> constr
+val drop_extra_implicit_args : constr -> constr
 
 (** occur checks *)
 exception Occur
@@ -107,6 +108,7 @@ val free_rels : constr -> Intset.t
 val dependent : constr -> constr -> bool
 val dependent_no_evar : constr -> constr -> bool
 val collect_metas : constr -> int list
+val collect_vars : constr -> Idset.t (** for visible vars only *)
 val occur_term : constr -> constr -> bool (** Synonymous
  of dependent 
    Substitution of metavariables *)