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, 54 insertions, 45 deletions

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 *)