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

5 files changed, 33 insertions, 36 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 41f89a541d..277d8b3c8c 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -43,12 +43,11 @@ let loc_of_binder_let = function
 
 let rec index_and_rec_order_of_annot loc bl ann =
   match names_of_local_assums bl,ann with
-    | [_], (None, r) -> Some 0, r
-    | lids, (Some x, ro) ->
-        let ids = List.map snd lids in
-        (try Some (list_index0 (snd x) ids), ro
-        with Not_found ->
-          user_err_loc(fst x,"index_of_annot", Pp.str"no such fix variable"))
+    | [loc,Name id], (None, r) -> Some (loc, id), r
+    | lids, (Some (loc, n), ro) ->
+        if List.exists (fun (_, x) -> x = Name n) lids then
+	  Some (loc, n), ro
+        else user_err_loc(loc,"index_of_annot", Pp.str"no such fix variable")
     | _, (None, r) -> None, r
 
 let mk_fixb (id,bl,ann,body,(loc,tyc)) =
@@ -370,9 +369,9 @@ GEXTEND Gram
     ] ]
   ;
   fixannot:
-    [ [ "{"; IDENT "struct"; id=name; "}" -> (Some id, CStructRec)
-    | "{"; IDENT "wf"; rel=constr; id=OPT name; "}" -> (id, CWfRec rel)
-    | "{"; IDENT "measure"; rel=constr; id=OPT name; "}" -> (id, CMeasureRec rel)
+    [ [ "{"; IDENT "struct"; id=identref; "}" -> (Some id, CStructRec)
+    | "{"; IDENT "wf"; rel=constr; id=OPT identref; "}" -> (id, CWfRec rel)
+    | "{"; IDENT "measure"; rel=constr; id=OPT identref; "}" -> (id, CMeasureRec rel)
     ] ]
   ;
   binders_let_fixannot:
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 8285bbad37..76646a4f97 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -263,18 +263,22 @@ GEXTEND Gram
         ty = type_cstr; 
 	":="; def = lconstr; ntn = decl_notation ->
 	  let bl, annot = (b :: fst bl, snd bl) in
-          let names = List.map snd (names_of_local_assums bl) in
+          let names = names_of_local_assums bl in
           let ni =
             match fst annot with
-                Some (_, id) ->
-                  (try Some (list_index0 id names)
-                   with Not_found ->  Util.user_err_loc
-                     (loc,"Fixpoint",
-                      Pp.str "No argument named " ++ Nameops.pr_name id))
+                Some (loc, id) ->
+                  (if List.exists (fun (_, id') -> Name id = id') names then
+		    Some (loc, id)
+		    else Util.user_err_loc
+                      (loc,"Fixpoint",
+                      Pp.str "No argument named " ++ Nameops.pr_id id))
               | None -> 
 		  (* If there is only one argument, it is the recursive one, 
 		     otherwise, we search the recursive index later *)
-		  if List.length names = 1 then Some 0 else None	  
+		  if List.length names = 1 then
+		    let (loc, na) = List.hd names in
+		      Some (loc, Nameops.out_name na)
+		  else None	  
 	  in 
 	  ((id,(ni,snd annot),bl,ty,def),ntn) ] ]
   ;
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index d9d4139e95..6f6cff2752 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -166,7 +166,7 @@ module Constr :
     val binder_let : local_binder Gram.Entry.e
     val delimited_binder_let : local_binder Gram.Entry.e
     val binders_let : local_binder list Gram.Entry.e
-    val binders_let_fixannot : (local_binder list * (name located option * recursion_order_expr)) Gram.Entry.e
+    val binders_let_fixannot : (local_binder list * (identifier located option * recursion_order_expr)) Gram.Entry.e
     val delimited_binders_let : local_binder list Gram.Entry.e
     val typeclass_constraint : (name located * binding_kind * constr_expr) Gram.Entry.e
     val appl_arg : (constr_expr * explicitation located option) Gram.Entry.e
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 21c5a343b4..41d98f2bc8 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -395,16 +395,15 @@ let pr_recursive_decl pr pr_dangling dangling_with_for id bl annot t c =
 
 let pr_fixdecl pr prd dangling_with_for (id,(n,ro),bl,t,c) =
   let annot =
-    let ids = names_of_local_assums bl in
-      match ro with
-	  CStructRec ->
-	    if List.length ids > 1 && n <> None then 
-	      spc() ++ str "{struct " ++ pr_name (snd (List.nth ids (Option.get n))) ++ str"}"
-	    else mt() 
-	| CWfRec c ->
-	    spc () ++ str "{wf " ++ pr lsimple c ++ pr_name (snd (List.nth ids (Option.get n))) ++ str"}"
-	| CMeasureRec c ->
-	    spc () ++ str "{measure " ++ pr lsimple c ++ pr_name (snd (List.nth ids (Option.get n))) ++ str"}"
+    match ro with
+	CStructRec ->
+	  if List.length bl > 1 && n <> None then 
+	    spc() ++ str "{struct " ++ pr_id (snd (Option.get n)) ++ str"}"
+	  else mt() 
+      | CWfRec c ->
+	  spc () ++ str "{wf " ++ pr lsimple c ++ pr_id (snd (Option.get n)) ++ str"}"
+      | CMeasureRec c ->
+	  spc () ++ str "{measure " ++ pr lsimple c ++ pr_id (snd (Option.get n)) ++ str"}"
   in
     pr_recursive_decl pr prd dangling_with_for id bl annot t c
 
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 57e21c2ce6..352f58f6ba 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -594,23 +594,18 @@ let rec pr_vernac = function
             let annot =
 	      match n with 
 		| None -> mt () 
-		| Some n -> 
-		    let name =
-		      try snd (List.nth ids n)
-		      with Failure _ ->
-			warn (str "non-printable fixpoint \""++pr_id id++str"\"");
-			Anonymous in
+		| Some (loc, id) -> 
 		    match (ro : Topconstr.recursion_order_expr) with
 			CStructRec -> 
 			  if List.length ids > 1 then 
-			    spc() ++ str "{struct " ++ pr_name name ++ str"}"
+			    spc() ++ str "{struct " ++ pr_id id ++ str"}"
 			  else mt()
 		      | CWfRec c -> 
 			  spc() ++ str "{wf " ++ pr_lconstr_expr c ++ spc() ++ 
-			    pr_name name ++ str"}"
+			    pr_id id ++ str"}"
 		      | CMeasureRec c -> 
 			  spc() ++ str "{measure " ++ pr_lconstr_expr c ++ spc() ++ 
-			    pr_name name ++ str"}"
+			    pr_id id ++ str"}"
 	    in
             pr_id id ++ pr_binders_arg bl ++ annot ++ spc()
             ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_