- Fix solve_simpl_eqn which was cheking instances types in the wrong environment sometimes.

- Remove compilation warning in classes.ml due to (as yet) unused code.

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

3 files changed, 27 insertions, 48 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index b88ea03e1..1df6a3d4e 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1295,24 +1295,6 @@ let status_changed lev (pbty,_,t1,t2) =
   (try ExistentialSet.mem (head_evar t1) lev with NoHeadEvar -> false) or
   (try ExistentialSet.mem (head_evar t2) lev with NoHeadEvar -> false)
 
-(* Util *)
-
-let check_instance_type conv_algo pbty env evd ev1 t2 =
-  let t2 = nf_evar evd t2 in
-  if has_undefined_evars_or_sorts evd t2 then
-    (* May contain larger constraints than needed: don't want to
-       commit to an equal solution while only subtyping is requested *)
-    evd
-  else
-    let typ2 = Retyping.get_type_of env evd (refresh_universes t2) in
-    if isEvar typ2 then (* Don't want to commit too early too *) evd
-    else
-      let typ1 = existential_type evd ev1 in
-      let evd,b = conv_algo env evd Reduction.CUMUL typ2 typ1 in
-	if b then evd else
-	  user_err_loc (fst (evar_source (fst ev1) evd),"",
-			str "Unable to find a well-typed instantiation")
-
 (* Tries to solve problem t1 = t2.
  * Precondition: t1 is an uninstantiated evar
  * Returns an optional list of evars that were instantiated, or None
@@ -1334,19 +1316,23 @@ let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1)
 	    else
 	      add_conv_pb (Reduction.CUMUL,env,t2,mkEvar ev1) evd
       | _ ->
-	  let evd = check_instance_type conv_algo pbty env evd ev1 t2 in
 	  let evd = evar_define ~choose env ev1 t2 evd in
 	  let evi = Evd.find evd evk1 in
-	    if occur_existential evd evi.evar_concl then
-	      let evenv = evar_unfiltered_env evi in
-	      let evc = nf_evar evd evi.evar_concl in
-		match evi.evar_body with
-		| Evar_defined body ->
-		    let ty = nf_evar evd (Retyping.get_type_of evenv evd body) in
-		      add_conv_pb (Reduction.CUMUL,evenv,ty,evc) evd
-		| Evar_empty -> (* Resulted in a constraint *)
-		    evd
-	    else evd
+	  let evenv = evar_unfiltered_env evi in
+	  let evc = nf_evar evd evi.evar_concl in
+	    match evi.evar_body with
+	    | Evar_defined body ->
+		let ty = nf_evar evd (Retyping.get_type_of evenv evd body) in
+		  if occur_existential evd evi.evar_concl
+		    || occur_existential evd ty 
+		  then add_conv_pb (Reduction.CUMUL,evenv,ty,evc) evd
+		  else
+		    let evd,b = conv_algo evenv evd Reduction.CUMUL ty evc in
+		      if b then evd else
+			user_err_loc (fst (evar_source (fst ev1) evd),"",
+				      str "Unable to find a well-typed instantiation")
+	    | Evar_empty -> (* Resulted in a constraint *)
+		evd
     in
     let (evd,pbs) = extract_changed_conv_pbs evd status_changed in
       List.fold_left
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index d26af7876..cac37ae28 100644
--- a/theories/Vectors/VectorDef.v
+++ b/theories/Vectors/VectorDef.v
@@ -38,11 +38,7 @@ Definition rectS {A} (P:forall {n}, t A (S n) -> Type)
  (bas: forall a: A, P (a :: []))
  (rect: forall a {n} (v: t A (S n)), P v -> P (a :: v)) :=
  fix rectS_fix {n} (v: t A (S n)) : P v :=
- match v in t _  n' return match n' return t _ n' -> Type with
-                                    | 0 => fun _ => ID
-                                    | S n => fun v => P v
-                                  end v
- with
+ match v with
  |nil => @id
  |cons a 0 v =>
    match v as vnn in t _ nn
@@ -67,9 +63,7 @@ fix rect2_fix {n} (v1:t A n):
 match v1 as v1' in t _ n1
   return forall v2 : t B n1, P v1' v2 with
   |[] => fun v2 =>
-     match v2 as v2' in t _ n2
-       return match n2 as n2' return t B n2' -> Type with
-         |0 => fun v2 => P [] v2 |S _ => fun _ => @ID end v2' with
+     match v2 with
        |[] => bas
        |_ :: _ => @id
      end
@@ -89,15 +83,14 @@ end.
 
 (** A vector of length [0] is [nil] *)
 Definition case0 {A} (P:t A 0 -> Type) (H:P (nil A)) v:P v :=
-match v as v0 in t _ n return match n return t _ n -> Type with 0 => fun v => P v | S n => fun v => ID end v0 with
+match v with
   |[] => H
-  | _ => @id
 end.
 
 (** A vector of length [S _] is [cons] *)
 Definition caseS {A} (P : forall n, t A (S n) -> Type)
   (H : forall h {n} t, @P n (h :: t)) {n} v : P n v :=
-match v as v0 in t _ n return match n return t _ n -> Type with 0 => fun v => ID | S n => fun v => P n v end v0 with 
+match v with
   |[] => @id (* Why needed ? *)
   |h :: t => H h t
 end.
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 4f1df4bb9..7786b200b 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -310,7 +310,7 @@ let rec declare_subclasses gr (rels, (tc, args)) =
 	  add_instance (Typeclasses.new_instance tc None false (ConstRef cst));
 	  declare_subclasses (ConstRef cst) cl
       | None -> ()
-  in () (* List.iter declare_proj projs *)
+  in List.iter declare_proj projs
 
 let context l =
   let env = Global.env() in
@@ -328,9 +328,9 @@ let context l =
 	(ParameterEntry (t,None), IsAssumption Logical)
       in
 	match class_of_constr t with
-	| Some (rels, (tc, args) as cl) ->
-	    add_instance (Typeclasses.new_instance tc None false (ConstRef cst));
-	    declare_subclasses (ConstRef cst) cl
+	| Some (rels, (tc, args) as _cl) ->
+	    add_instance (Typeclasses.new_instance tc None false (ConstRef cst))
+	    (* declare_subclasses (ConstRef cst) cl *)
 	| None -> ()
     else (
       let impl = List.exists 
@@ -338,9 +338,9 @@ let context l =
 	   match x with ExplByPos (_, Some id') -> id = id' | _ -> false) impls
       in
 	Command.declare_assumption false (Local (* global *), Definitional) t
-	  [] impl (* implicit *) None (* inline *) (dummy_loc, id);
-	match class_of_constr t with
-	| None -> ()
-	| Some tc -> declare_subclasses (VarRef id) tc)
+	  [] impl (* implicit *) None (* inline *) (dummy_loc, id))
+(* 	match class_of_constr t with *)
+(* 	| None -> () *)
+(* 	| Some tc -> declare_subclasses (VarRef id) tc) *)
   in List.iter fn (List.rev ctx)