From c4d79461518f5dd4351a558cac4c3d3ad410609a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 23 Oct 2010 14:08:30 +0000
Subject: 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
---
 tactics/auto.ml | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

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
-- 
cgit v1.2.3