Fix bug #1943 and restrict the inference optimisation of Program to

cases where coercion could not occur as well.


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

9 files changed, 96 insertions, 71 deletions

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 11d8d7a0b4..3421125369 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1737,6 +1737,8 @@ let rec xlate_vernac =
 	  (fst::rest) -> CT_formula_ne_list(fst,rest)
 	| _ -> assert false in
       CT_hintrewrite(ct_orient, f_ne_list, CT_ident base, xlate_tactic t)
+  | VernacCreateHintDb (local,dbname,b) ->
+      xlate_error "TODO: VernacCreateHintDb"
   | VernacHints (local,dbnames,h) ->
       let dblist = CT_id_list(List.map (fun x -> CT_ident x) dbnames) in
       (match h with
diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index 289e64c299..56bd40d30f 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -103,9 +103,11 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Class
 	  let loc, id, par = Implicit_quantifiers.destClassAppExpl cl in
 	  let k = class_info (Nametab.global id) in
 	  let applen = List.fold_left (fun acc (x, y) -> if y = None then succ acc else acc) 0 par in
-	  let needlen = List.fold_left (fun acc (x, y) -> if x = None then succ acc else acc) 0 k.cl_context in
+	  let needlen = List.fold_left (fun acc x -> if x = None then succ acc else acc) 0 (fst k.cl_context) in
 	    if needlen <> applen then 
-	      Classes.mismatched_params env (List.map fst par) (List.map snd k.cl_context);
+	      Classes.mismatched_params env (List.map fst par) (snd k.cl_context);
+	    let (ci, rd) = k.cl_context in
+	    let pars = List.rev (List.combine ci rd) in
 	    let pars, _ = Implicit_quantifiers.combine_params Idset.empty (* need no avoid *)
 	      (fun avoid (clname, (id, _, t)) -> 
 		match clname with 
@@ -117,7 +119,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Class
 			else CHole (Util.dummy_loc, None)
 		      in t, avoid
 		  | None -> failwith ("new instance: under-applied typeclass"))
-	      par (List.rev k.cl_context)
+	      par pars
 	    in Topconstr.CAppExpl (loc, (None, id), pars)
 
       | Explicit -> cl
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index 4b68f1fc78..519626a3a3 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -33,37 +33,36 @@ open Pp
 let pair_of_array a = (a.(0), a.(1))
 let make_name s = Name (id_of_string s)
 
+let rec disc_subset x = 
+  match kind_of_term x with
+  | App (c, l) ->
+      (match kind_of_term c with
+      Ind i ->
+	let len = Array.length l in
+	let sig_ = Lazy.force sig_ in
+	  if len = 2 && i = Term.destInd sig_.typ
+	  then
+	    let (a, b) = pair_of_array l in
+	      Some (a, b)
+	  else None
+      | _ -> None)
+  | _ -> None
+      
+and disc_exist env x =
+  match kind_of_term x with
+  | App (c, l) ->
+      (match kind_of_term c with
+      Construct c ->	       
+	if c = Term.destConstruct (Lazy.force sig_).intro
+	then Some (l.(0), l.(1), l.(2), l.(3))
+	else None
+      | _ -> None)
+  | _ -> None
+      
 module Coercion = struct
-
+    
   exception NoSubtacCoercion
-
-  let rec disc_subset x = 
-    match kind_of_term x with
-      | App (c, l) ->
-	  (match kind_of_term c with
-	       Ind i ->
-		 let len = Array.length l in
-		 let sig_ = Lazy.force sig_ in
-		   if len = 2 && i = Term.destInd sig_.typ
-		   then
-		     let (a, b) = pair_of_array l in
-		       Some (a, b)
-		   else None
-	     | _ -> None)
-      | _ -> None
-	  
-  and disc_exist env x =
-    match kind_of_term x with
-      | App (c, l) ->
-	  (match kind_of_term c with
-	       Construct c ->	       
-		 if c = Term.destConstruct (Lazy.force sig_).intro
-		 then Some (l.(0), l.(1), l.(2), l.(3))
-		 else None
-	     | _ -> None)
-      | _ -> None
-
-
+    
   let disc_proj_exist env x =
     match kind_of_term x with
       | App (c, l) ->
diff --git a/contrib/subtac/subtac_coercion.mli b/contrib/subtac/subtac_coercion.mli
index 53a8d21338..5678c10e69 100644
--- a/contrib/subtac/subtac_coercion.mli
+++ b/contrib/subtac/subtac_coercion.mli
@@ -1 +1,4 @@
+open Term
+val disc_subset : types -> (types * types) option
+
 module Coercion : Coercion.S
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index b5f9f99c1b..8201e8fdcc 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -276,14 +276,19 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 
     | RApp (loc,f,args) -> 
 	let length = List.length args in 
-	let ftycon = 
-	  if length > 0 then
-	    match tycon with
-	    | None -> None
-	    | Some (None, ty) -> mk_abstr_tycon length ty
-	    | Some (Some (init, cur), ty) ->
-		Some (Some (length + init, length + cur), ty)
-	  else tycon
+	let ftycon =
+	  let ty = 
+	    if length > 0 then
+	      match tycon with
+	      | None -> None
+	      | Some (None, ty) -> mk_abstr_tycon length ty
+	      | Some (Some (init, cur), ty) ->
+		  Some (Some (length + init, length + cur), ty)
+ 	    else tycon
+	  in 
+	    match ty with
+	    | Some (_, t) when Subtac_coercion.disc_subset t = None -> ty
+	    | _ -> None
 	in
 	let fj = pretype ftycon env isevars lvar f in
  	let floc = loc_of_rawconstr f in
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index d084a3f7d0..8bacbcd8cf 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -169,7 +169,9 @@ let full_class_binders env l =
 	    let gr = Nametab.global id in
 	      (try
 		  let c = class_info gr in
-		  let args, avoid = combine_params_freevar avoid l (List.rev c.cl_context) in
+		  let (ci, rd) = c.cl_context in
+		  let pars = List.rev (List.combine ci rd) in
+		  let args, avoid = combine_params_freevar avoid l pars in
 		    (iid, bk, CAppExpl (loc, (None, id), args)) :: l', avoid
 		with Not_found -> not_a_class (Global.env ()) (constr_of_global gr))
 	| Explicit -> (x :: l', avoid))
@@ -206,7 +208,9 @@ let full_class_binder env (iid, (bk, bk'), cl as c) =
 	let gr = Nametab.global id in
 	  (try
 	      let c = class_info gr in
-	      let args, avoid = combine_params_freevar avoid l (List.rev c.cl_context) in
+	      let (ci, rd) = c.cl_context in
+	      let pars = List.rev (List.combine ci rd) in
+	      let args, avoid = combine_params_freevar avoid l pars in
 		(iid, bk, CAppExpl (loc, (None, id), args)), avoid
 	    with Not_found -> not_a_class (Global.env ()) (constr_of_global gr))
     | Explicit -> ((iid,bk,cl), avoid)
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 783bb50fd5..347dfe157c 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -35,7 +35,7 @@ type typeclass = {
   cl_impl : global_reference; 
 
   (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *)
-  cl_context : ((global_reference * bool) option * rel_declaration) list; 
+  cl_context : (global_reference * bool) option list * rel_context; 
 
   (* Context of definitions and properties on defs, will not be shared *)
   cl_props : rel_context;
@@ -137,23 +137,21 @@ let subst (_,subst,(cl,m,inst)) =
   and do_subst c = Mod_subst.subst_mps subst c
   and do_subst_gr gr = fst (subst_global subst gr)
   in
-  let do_subst_named ctx = 
+  let do_subst_ctx ctx = 
     list_smartmap (fun (na, b, t) ->
       (na, Option.smartmap do_subst b, do_subst t))
       ctx
   in
-  let do_subst_ctx ctx = 
-    list_smartmap (fun (cl, (na, b, t)) ->
-      (Option.smartmap (fun (gr,b) -> do_subst_gr gr, b) cl,
-      (na, Option.smartmap do_subst b, do_subst t)))
-      ctx
+  let do_subst_context (grs,ctx) = 
+    list_smartmap (Option.smartmap (fun (gr,b) -> do_subst_gr gr, b)) grs,
+    do_subst_ctx ctx
   in
   let do_subst_projs projs = list_smartmap (fun (x, y) -> (x, Option.smartmap do_subst_con y)) projs in
   let subst_class k cl classes = 
     let k = do_subst_gr k in
     let cl' = { cl_impl = k;
-		cl_context = do_subst_ctx cl.cl_context;
-		cl_props = do_subst_named cl.cl_props;
+		cl_context = do_subst_context cl.cl_context;
+		cl_props = do_subst_ctx cl.cl_props;
 		cl_projs = do_subst_projs cl.cl_projs; }
     in 
     let cl' = if cl' = cl then cl else cl' in
@@ -172,14 +170,18 @@ let subst (_,subst,(cl,m,inst)) =
   let instances = Gmap.fold subst_inst inst Gmap.empty in
     (classes, m, instances)
 
+let rel_of_variable_context ctx = 
+  List.fold_right (fun (n,_,b,t) (ctx', subst)->
+    let decl = (Name n, Option.map (substn_vars 1 subst) b, substn_vars 1 subst t) in
+      (decl :: ctx', n :: subst)) ctx ([], [])
+    
 let discharge (_,(cl,m,inst)) =
-  let discharge_context subst rel =
+  let discharge_rel_context subst n rel =
     let ctx, _ =
       List.fold_right
-	(fun (gr, (id, b, t)) (ctx, k) -> 
-	  let gr' = Option.smartmap (fun (gr, b) -> Lib.discharge_global gr, b) gr in
-	    ((gr', (id, Option.smartmap (substn_vars k subst) b, substn_vars k subst t)) :: ctx), succ k)
-	rel ([], 0)
+	(fun (id, b, t) (ctx, k) -> 
+	  (id, Option.smartmap (substn_vars k subst) b, substn_vars k subst t) :: ctx, succ k)
+	rel ([], n)
     in ctx
   in
   let abs_context cl =
@@ -188,17 +190,22 @@ let discharge (_,(cl,m,inst)) =
     | ConstRef cst -> Lib.section_segment_of_constant cst
     | IndRef (ind,_) -> Lib.section_segment_of_mutual_inductive ind
   in
+  let discharge_context ctx' subst (grs, ctx) =
+    let grs' = List.map (fun _ -> None) subst @ 
+      list_smartmap (Option.smartmap (fun (gr, b) -> Lib.discharge_global gr, b)) grs
+    in grs', discharge_rel_context subst 1 ctx @ ctx'
+  in
   let subst_class k cl acc = 
     let cl_impl' = Lib.discharge_global cl.cl_impl in
     let cl' =
       if cl_impl' == cl.cl_impl then cl
       else
 	let ctx = abs_context cl in
-	{ cl with cl_impl = cl_impl';
-	  cl_context = 
-	    List.map (fun (na,impl,b,t) -> None, (Name na,b,t)) ctx @
-	      (discharge_context (List.map (fun (na, _, _, _) -> na) ctx) cl.cl_context);
-	  cl_projs = list_smartmap (fun (x, y) -> x, Option.smartmap Lib.discharge_con y) cl.cl_projs }
+	let ctx', subst = rel_of_variable_context ctx in
+	  { cl_impl = cl_impl';
+	    cl_context = discharge_context ctx' subst cl.cl_context;
+	    cl_props = discharge_rel_context subst (succ (List.length (fst cl.cl_context))) cl.cl_props;
+	    cl_projs = list_smartmap (fun (x, y) -> x, Option.smartmap Lib.discharge_con y) cl.cl_projs }
     in Gmap.add cl_impl' cl' acc
   in
   let classes = Gmap.fold subst_class cl Gmap.empty in
@@ -257,7 +264,7 @@ let class_info c =
   with _ -> not_a_class (Global.env()) (constr_of_global c)
 
 let instance_constructor cl args = 
-  let pars = fst (list_chop (List.length cl.cl_context) args) in
+  let pars = fst (list_chop (List.length (fst cl.cl_context)) args) in
     match cl.cl_impl with
       | IndRef ind -> applistc (mkConstruct (ind, 1)) args,
 	  applistc (mkInd ind) pars
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 706f116563..97fbae075b 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -29,8 +29,9 @@ type typeclass = {
   cl_impl : global_reference; 
 
   (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. 
-     The boolean indicates if the typeclass argument is a direct superclass. *)
-  cl_context : ((global_reference * bool) option * rel_declaration) list; 
+     The boolean indicates if the typeclass argument is a direct superclass and the global reference
+     gives a direct link to the class itselft. *)
+  cl_context : (global_reference * bool) option list * rel_context; 
 
   (* Context of definitions and properties on defs, will not be shared *)
   cl_props : rel_context;
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 4a8ce920f2..702d9efb09 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -244,11 +244,11 @@ let new_class id par ar sup props =
 			       (List.rev fields) (Recordops.lookup_projections (kn,0)))
   in
   let ctx_context =
-    List.map (fun ((na, b, t) as d) -> 
+    List.map (fun (na, b, t) -> 
       match Typeclasses.class_of_constr t with
-      | Some cl -> (Some (cl.cl_impl, List.exists (fun (_, n) -> n = na) supnames), d)
-      | None -> (None, d))
-      ctx_params
+      | Some cl -> Some (cl.cl_impl, List.exists (fun (_, n) -> n = na) supnames)
+      | None -> None)
+      ctx_params, ctx_params
   in
   let k =
     { cl_impl = impl;
@@ -352,9 +352,11 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau
 	  let loc, id, par = Implicit_quantifiers.destClassAppExpl cl in
 	  let k = class_info (Nametab.global id) in
 	  let applen = List.fold_left (fun acc (x, y) -> if y = None then succ acc else acc) 0 par in
-	  let needlen = List.fold_left (fun acc (x, y) -> if x = None then succ acc else acc) 0 k.cl_context in
+	  let needlen = List.fold_left (fun acc x -> if x = None then succ acc else acc) 0 (fst k.cl_context) in
 	    if needlen <> applen then 
-	      mismatched_params env (List.map fst par) (List.map snd k.cl_context);
+	      mismatched_params env (List.map fst par) (snd k.cl_context);
+	    let (ci, rd) = k.cl_context in
+	    let pars = List.rev (List.combine ci rd) in
 	    let pars, _ = Implicit_quantifiers.combine_params Idset.empty (* need no avoid *)
 	      (fun avoid (clname, (id, _, t)) -> 
 		match clname with 
@@ -366,7 +368,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau
 			else CHole (Util.dummy_loc, None)
 		      in t, avoid
 		  | None -> failwith ("new instance: under-applied typeclass"))
-	      par (List.rev k.cl_context)
+	      par pars
 	    in Topconstr.CAppExpl (loc, (None, id), pars)
 
       | Explicit -> cl