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, 68 insertions, 50 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 5047d1b98e..dedaf6af4a 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -720,7 +720,12 @@ let rec extern inctx scopes vars r =
                  let (ids,bl) = extern_local_binder scopes vars bl in
                  let vars0 = List.fold_right (name_fold Idset.add) ids vars in
                  let vars1 = List.fold_right (name_fold Idset.add) ids vars' in
-		 let n, ro = fst nv.(i), extern_recursion_order scopes vars (snd nv.(i)) in
+		 let n = 
+		   match fst nv.(i) with
+		     | None -> None
+		     | Some x -> Some (dummy_loc, out_name (List.nth ids x))
+		 in 
+		 let ro = extern_recursion_order scopes vars (snd nv.(i)) in
 		 (fi, (n, ro), bl, extern_typ scopes vars0 ty,
                   extern false scopes vars1 def)) idv
 	     in 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index fe1fca3489..65efc1f67b 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -32,6 +32,8 @@ type var_internalisation_data =
 type implicits_env = (identifier * var_internalisation_data) list
 type full_implicits_env = identifier list * implicits_env
 
+type raw_binder = (name * binding_kind * rawconstr option * rawconstr)
+
 let interning_grammar = ref false
 
 (* Historically for parsing grammar rules, but in fact used only for
@@ -848,23 +850,32 @@ let internalise sigma globalenv env allow_patvar lvar c =
         let idl = Array.map
           (fun (id,(n,order),bl,ty,bd) ->
 	     let intern_ro_arg c f =
-	       let before, after = list_chop (succ (Option.get n)) bl in
-	       let ((ids',_,_),rafter) =
-		 List.fold_left intern_local_binder (env,[]) after in
-	       let ro = (intern (ids', tmp_scope, scopes) c) in
-		 f ro, List.fold_left intern_local_binder (env,rafter) before
+	       let idx = 
+		 match n with
+		     Some (loc, n) -> list_index0 (Name n) (List.map snd (names_of_local_assums bl))
+		   | None -> 0
+	       in
+	       let before, after = list_chop idx bl in
+	       let ((ids',_,_) as env',rbefore) =
+		 List.fold_left intern_local_binder (env,[]) before in
+	       let ro =
+		 match c with 
+		   | None -> RStructRec 
+		   | Some c' -> f (intern (ids', tmp_scope, scopes) c') 
+	       in 
+	       let n' = Option.map (fun _ -> List.length before) n in
+		 n', ro, List.fold_left intern_local_binder (env',rbefore) after
 	     in
-	     let ro, ((ids',_,_),rbl) =
+	     let n, ro, ((ids',_,_),rbl) =
 	       (match order with
-		    CStructRec -> 
-		      RStructRec,
-		      List.fold_left intern_local_binder (env,[]) bl
-		  | CWfRec c ->
-		      intern_ro_arg c (fun r -> RWfRec r)
-		  | CMeasureRec c ->
-		      intern_ro_arg c (fun r -> RMeasureRec r))
-	    in
-	    let ids'' = List.fold_right Idset.add lf ids' in
+		 | CStructRec -> 
+		     intern_ro_arg None (fun _ -> RStructRec)
+		 | CWfRec c ->
+		     intern_ro_arg (Some c) (fun r -> RWfRec r)
+		 | CMeasureRec c ->
+		     intern_ro_arg (Some c) (fun r -> RMeasureRec r))
+	     in
+	     let ids'' = List.fold_right Idset.add lf ids' in
 	     ((n, ro), List.rev rbl, 
              intern_type (ids',tmp_scope,scopes) ty,
              intern (ids'',None,scopes) bd)) dl in
@@ -1276,45 +1287,43 @@ let my_intern_constr sigma env acc c =
 
 let my_intern_type sigma env acc c = my_intern_constr sigma env (set_type_scope acc) c
 
-let interp_context sigma env params = 
-  let ids, bl =
-    List.fold_left
-      (intern_local_binder_aux (my_intern_constr sigma env) (my_intern_type sigma env))
-      ((extract_ids env,None,[]), []) params
-  in
+let intern_context sigma env params =
+  snd (List.fold_left
+	  (intern_local_binder_aux (my_intern_constr sigma env) (my_intern_type sigma env))
+	  ((extract_ids env,None,[]), []) params)
+
+let interp_context_gen understand_type understand_judgment env bl = 
+  let (env, par, _, impls) =
     List.fold_left
-      (fun (env,params) (na, k, b, t) ->
+      (fun (env,params,n,impls) (na, k, b, t) ->
 	match b with
 	    None ->
 	      let t' = locate_if_isevar (loc_of_rawconstr t) na t in
-	      let t = Default.understand_type sigma env t' in
+	      let t = understand_type env t' in
 	      let d = (na,None,t) in
-		(push_rel d env, d::params)
+	      let impls = 
+		if k = Implicit then
+		  let na = match na with Name n -> Some n | Anonymous -> None in
+		    (ExplByPos (n, na), (true, true)) :: impls
+		else impls
+	      in
+		(push_rel d env, d::params, succ n, impls)
 	  | Some b ->
-	      let c = Default.understand_judgment sigma env b in
+	      let c = understand_judgment env b in
 	      let d = (na, Some c.uj_val, c.uj_type) in
-		(push_rel d env,d::params))
-      (env,[]) (List.rev bl)
+		(push_rel d env,d::params, succ n, impls))
+      (env,[],1,[]) (List.rev bl)
+  in (env, par), impls
 
+let interp_context sigma env params = 
+  let bl = intern_context sigma env params in
+    interp_context_gen (Default.understand_type sigma) 
+      (Default.understand_judgment sigma) env bl
+    
 let interp_context_evars evdref env params =
-  let ids, bl =
-    List.fold_left
-      (intern_local_binder_aux (my_intern_constr evdref env) (my_intern_type evdref env))
-      ((extract_ids env,None,[]), []) params
-  in
-    List.fold_left
-      (fun (env,params) (na, k, b, t) ->
-	match b with
-	    None ->
-	      let t' = locate_if_isevar (loc_of_rawconstr t) na t in
-	      let t = Default.understand_tcc_evars evdref env IsType t' in
-	      let d = (na,None,t) in
-		(push_rel d env, d::params)
-	  | Some b ->
-	      let c = Default.understand_judgment_tcc evdref env b in
-	      let d = (na, Some c.uj_val, c.uj_type) in
-		(push_rel d env,d::params))
-      (env,[]) (List.rev bl)
+  let bl = intern_context (Evd.evars_of !evdref) env params in
+    interp_context_gen (fun env t -> Default.understand_tcc_evars evdref env IsType t)
+      (Default.understand_judgment_tcc evdref) env bl
     
 (**********************************************************************)
 (* Locating reference, possibly via an abbreviation *)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index f81b2ccd16..fb69460c4a 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -49,6 +49,8 @@ type manual_implicits = (explicitation * (bool * bool)) list
 
 type ltac_sign = identifier list * unbound_ltac_var_map
 
+type raw_binder = (name * binding_kind * rawconstr option * rawconstr)
+
 (*s Internalisation performs interpretation of global names and notations *)
 
 val intern_constr : evar_map -> env -> constr_expr -> rawconstr
@@ -63,6 +65,8 @@ val intern_pattern : env -> cases_pattern_expr ->
   Names.identifier list *
     ((Names.identifier * Names.identifier) list * Rawterm.cases_pattern) list
 
+val intern_context : evar_map -> env -> local_binder list -> raw_binder list
+
 (*s Composing internalisation with pretyping *)
 
 (* Main interpretation function *)
@@ -120,10 +124,10 @@ val interp_binder_evars : evar_defs ref -> env -> name -> constr_expr -> types
 
 (* Interpret contexts: returns extended env and context *)
 
-val interp_context : evar_map -> env -> local_binder list -> env * rel_context
+val interp_context : evar_map -> env -> local_binder list -> (env * rel_context) * manual_implicits
 
 val interp_context_evars : 
-  evar_defs ref -> env -> local_binder list -> env * rel_context
+  evar_defs ref -> env -> local_binder list -> (env * rel_context) * manual_implicits
 
 (* Locating references of constructions, possibly via a syntactic definition *)
 
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index e80065dce1..cad9ad602e 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -585,7 +585,7 @@ type constr_expr =
   | CDynamic of loc * Dyn.t
 
 and fixpoint_expr =
-    identifier * (int option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
+    identifier * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
 
 and local_binder =
   | LocalRawDef of name located * constr_expr
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 3094be0e9d..f56550dd5a 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -136,7 +136,7 @@ type constr_expr =
   | CDynamic of loc * Dyn.t
 
 and fixpoint_expr =
-    identifier * (int option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
+    identifier * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
 
 and cofixpoint_expr =
     identifier * local_binder list * constr_expr * constr_expr