- Add more precise error localisation when one of the application fails

  in a chain of apply or apply-in.
- Improved comments on the notions of permutation used in the library (still
  the equality relation in file Permutation.v misses the property of being
  effectively an equivalence relation, hence missing expected properties of
  this notion of permutation).



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

1 files changed, 4 insertions, 4 deletions

diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 65a56100b..e6130cfcd 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -40,10 +40,10 @@ let h_exact_no_check c =
 let h_vm_cast_no_check c = 
   abstract_tactic (TacVmCastNoCheck (inj_open c)) (vm_cast_no_check c)
 let h_apply simple ev cb =
-  abstract_tactic (TacApply (simple,ev,cb,None))
+  abstract_tactic (TacApply (simple,ev,List.map snd cb,None))
     (apply_with_ebindings_gen simple ev cb)
 let h_apply_in simple ev cb (id,ipat as inhyp) =
-  abstract_tactic (TacApply (simple,ev,cb,Some inhyp))
+  abstract_tactic (TacApply (simple,ev,List.map snd cb,Some inhyp))
     (apply_in simple ev id cb ipat)
 let h_elim ev cb cbo    =
   abstract_tactic (TacElim (ev,inj_open_wb cb,Option.map inj_open_wb cbo))
@@ -131,8 +131,8 @@ let h_transitivity c =
   abstract_tactic (TacTransitivity (Option.map inj_open c))
     (intros_transitivity c)
 
-let h_simplest_apply c  = h_apply false false [inj_open c,NoBindings]
-let h_simplest_eapply c = h_apply false true [inj_open c,NoBindings]
+let h_simplest_apply c = h_apply false false [dummy_loc,(inj_open c,NoBindings)]
+let h_simplest_eapply c = h_apply false true [dummy_loc,(inj_open c,NoBindings)]
 let h_simplest_elim c   = h_elim false (c,NoBindings) None
 let h_simplest_case   c = h_case false (c,NoBindings)