- Addition of "Hint Resolve ->" and "Hint Resolve <-" continued: it

  revealed a too strict test for detection of inferable metas in
  Clenv. Restored tolerance for unbound names in interactive tactic use.
- Moral removals of some captures of Not_found in Environ.evaluable_* since
  kernel is assumed to deal with existing names.


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

5 files changed, 23 insertions, 20 deletions

diff --git a/CHANGES b/CHANGES
index 2ef2ab93b8..2fae9a7e70 100644
--- a/CHANGES
+++ b/CHANGES
@@ -17,6 +17,8 @@ Tactics
 - Tactic "idtac" now displays its list arguments.
 - Tactic "tauto" now proves classical tautologies as soon as classical logic
   (i.e. library Classical_Prop or Classical) is loaded.
+- New "Hint Resolve ->" (or "<-") for declaring iff's as oriented
+  hints (wish #2104).
 
 Tactic Language
 
diff --git a/kernel/environ.ml b/kernel/environ.ml
index e0f364f2ee..de833c540e 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -44,12 +44,9 @@ let lookup_rel n env =
   lookup_rel n env.env_rel_context
 
 let evaluable_rel n env =
-  try
-    match lookup_rel n env with
-        (_,Some _,_) -> true
-      | _ -> false
-  with Not_found -> 
-    false
+  match lookup_rel n env with
+  | (_,Some _,_) -> true
+  | _ -> false
 
 let nb_rel env = env.env_nb_rel
 
@@ -111,11 +108,9 @@ let named_body id env =
   let (_,b,_) = lookup_named id env in b
 
 let evaluable_named id env =
-  try 
-    match named_body id env with
-    |Some _      -> true
-    | _          -> false
-  with Not_found -> false
+  match named_body id env with
+  | Some _      -> true
+  | _          -> false
       
 let reset_with_named_context (ctxt,ctxtv) env =
   { env with
@@ -175,7 +170,7 @@ let constant_opt_value env cst =
 (* A global const is evaluable if it is defined and not opaque *)
 let evaluable_constant cst env =
   try let _  = constant_value env cst in true
-  with Not_found | NotEvaluableConst _ -> false
+  with NotEvaluableConst _ -> false
 
 (* Mutual Inductives *)
 let lookup_mind = lookup_mind
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 576e217aa5..dd2af306c9 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -231,9 +231,9 @@ let clenv_dependent hyps_only clenv =
   let nonlinear = duplicated_metas (clenv_value clenv) in
   (* Make the assumption that duplicated metas have internal dependencies *)
   List.filter
-    (fun mv -> (Metaset.mem mv deps &&
-                not (hyps_only && Metaset.mem mv ctyp_mvs))
-               or List.mem mv nonlinear) 
+    (fun mv -> if Metaset.mem mv deps
+               then not (hyps_only && Metaset.mem mv ctyp_mvs)
+               else List.mem mv nonlinear)
     mvs
 
 let clenv_missing ce = clenv_dependent true ce
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 8236f3e9e5..cbc1c6ce24 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -548,16 +548,16 @@ let short_name = function
   | AN (Ident (loc,id)) when not !strict_check -> Some (loc,id)
   | _ -> None
 
-let interp_global_reference r =
+let intern_evaluable_global_reference ist r =
   let lqid = qualid_of_reference r in
-  try locate_global_with_alias lqid
+  try evaluable_of_global_reference ist.genv (locate_global_with_alias lqid)
   with Not_found ->
   match r with 
-  | Ident (loc,id) when not !strict_check -> VarRef id
+  | Ident (loc,id) when not !strict_check -> EvalVarRef id
   | _ -> error_global_not_found_loc lqid
 
 let intern_evaluable_reference_or_by_notation ist = function
-  | AN r -> evaluable_of_global_reference ist.genv (interp_global_reference r)
+  | AN r -> intern_evaluable_global_reference ist r
   | ByNotation (loc,ntn,sc) ->
       evaluable_of_global_reference ist.genv
       (Notation.interp_notation_as_global_reference loc
diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v
index e1c74048cb..98b5992ade 100644
--- a/test-suite/success/Hints.v
+++ b/test-suite/success/Hints.v
@@ -24,7 +24,7 @@ Hint Destruct h8 := 4 Hypothesis (_ <= _) => fun H => apply H.
 (* Checks that local names are accepted *)
 Section A.
   Remark Refl : forall (A : Set) (x : A), x = x. 
-  Proof refl_equal.
+  Proof. exact refl_equal. Defined.
   Definition Sym := sym_equal.
   Let Trans := trans_equal.
  
@@ -46,3 +46,9 @@ Section A.
 
 End A.
 
+Axiom a : forall n, n=0 <-> n<=0.
+
+Hint Resolve -> a.
+Goal forall n, n=0 -> n<=0.
+auto.
+Qed.