diff options
| author | herbelin | 2010-10-23 14:08:30 +0000 |
|---|---|---|
| committer | herbelin | 2010-10-23 14:08:30 +0000 |
| commit | c4d79461518f5dd4351a558cac4c3d3ad410609a (patch) | |
| tree | b6a534c22b40c5b64a0aa235478e991eec3612c4 | |
| parent | d77eaf1431ee13066ee5e55074297bbb4b4d4197 (diff) | |
Automatically translate hints of the form "c _ ... _" into "c". Besides
being convenient, it improves compatibility when moving more implicit
arguments to maximal status.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13574 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/auto.ml | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 17a2ea1740..95cffeb423 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -566,8 +566,19 @@ type hints_entry = | HintsDestructEntry of identifier * int * (bool,unit) location * (patvar list * constr_pattern) * glob_tactic_expr +let rec drop_extra_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_args (mkApp (f,fst (array_chop (Array.length args - 1) args))) + | _ -> c + let interp_hints h = - let f = Constrintern.interp_constr Evd.empty (Global.env()) in + let f c = + let evd,c = Constrintern.interp_open_constr Evd.empty (Global.env()) c in + let c = drop_extra_args c in + Evarutil.check_evars (Global.env()) Evd.empty evd c; + c in let fr r = let gr = global_with_alias r in let r' = evaluable_of_global_reference (Global.env()) gr in |