Postpone the search for the recursive argument index from the user given

name after internalisation, to get the correct behavior with typeclass
binders. This simplifies the pretty printing and translation
of the recursive argument name in various places too. Use this
opportunity to factorize the different internalization and
interpretation functions of binders as well.
This definitely fixes part 2 of bug
#1846 and makes it possible to use fixpoint definitions with typeclass arguments in
program too, with an example given in EquivDec. 
At the same time, one fix and one enhancement in Program:
- fix a de Bruijn bug in subtac_cases
- introduce locations of obligations and use them in case the obligation tactic
raises a failure when tried on a particular obligation, as suggested by
Sean Wilson.


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

1 files changed, 1 insertions, 1 deletions

diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index 9641794bea..06c67e60b1 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -54,7 +54,7 @@ let solve_tccs_in_type env id isevars evm c typ =
     let stmt_id = Nameops.add_suffix id "_stmt" in
     let obls, c', t' = eterm_obligations env stmt_id !isevars evm 0 c typ in
     (** Make all obligations transparent so that real dependencies can be sorted out by the user *)
-    let obls = Array.map (fun (id, t, op, d) -> (id, t, false, d)) obls in
+    let obls = Array.map (fun (id, t, l, op, d) -> (id, t, l, false, d)) obls in
       match Subtac_obligations.add_definition stmt_id c' typ obls with
 	  Subtac_obligations.Defined cst -> constant_value (Global.env()) cst
 	| _ ->