Fix bug# 2994, 2971 about better error messages.

Fix bug# 2956, porting fix from 8.4 branch


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

4 files changed, 14 insertions, 9 deletions

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 80207f6524..34f8f07f9d 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -382,7 +382,9 @@ let add_class cl =
   List.iter (fun (n, inst, body) ->
 	     match inst with
 	     | Some (Backward, pri) ->
-	       declare_instance pri false (ConstRef (Option.get body))
+	       (match body with
+	       | None -> Errors.error "Non-definable projection can not be declared as a subinstance"
+	       | Some b -> declare_instance pri false (ConstRef b))
 	     | _ -> ())
   cl.cl_projs
 
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index a3006e99cc..ad8517c32a 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -142,11 +142,14 @@ let build_signature evars env m (cstrs : (types * types option) option list)
     new_cstr_evar evars env
       (* ~src:(Loc.ghost, ImplicitArg (ConstRef (Lazy.force respectful), (n, Some na))) *) t
   in
-  let mk_relty evars env ty obj =
+  let mk_relty evars newenv ty obj =
     match obj with
       | None | Some (_, None) ->
 	  let relty = mk_relation ty in
-	    new_evar evars env relty
+	    if closed0 ty then 
+	      let env' = Environ.reset_with_named_context (Environ.named_context_val env) env in
+		new_evar evars env' relty
+	    else new_evar evars newenv relty
       | Some (x, Some rel) -> evars, rel
   in
   let rec aux env evars ty l =
@@ -484,7 +487,7 @@ let rec apply_pointwise rel = function
   | [] -> rel
 
 let pointwise_or_dep_relation n t car rel =
-  if noccurn 1 car then
+  if noccurn 1 car && noccurn 1 rel then
     mkApp (Lazy.force pointwise_relation, [| t; lift (-1) car; lift (-1) rel |])
   else
     mkApp (Lazy.force forall_relation, 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 06aa351b5e..420de5d204 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -69,7 +69,7 @@ let red_constant_entry n ce = function
       { ce with const_entry_body =
         under_binders (Global.env()) (fst (reduction_of_red_expr red)) n body }
 
-let interp_definition bl red_option c ctypopt =
+let interp_definition bl red_option fail_evar c ctypopt =
   let env = Global.env() in
   let evdref = ref Evd.empty in
   let impls, ((env_bl, ctx), imps1) = interp_context_evars evdref env bl in
@@ -77,7 +77,7 @@ let interp_definition bl red_option c ctypopt =
   let imps,ce =
     match ctypopt with
       None ->
-	let c, imps2 = interp_constr_evars_impls ~impls ~evdref ~fail_evar:false env_bl c in
+	let c, imps2 = interp_constr_evars_impls ~impls ~evdref ~fail_evar env_bl c in
 	let body = nf_evar !evdref (it_mkLambda_or_LetIn c ctx) in
 	imps1@(Impargs.lift_implicits nb_args imps2),
 	{ const_entry_body = body;
@@ -88,7 +88,7 @@ let interp_definition bl red_option c ctypopt =
 	}
     | Some ctyp ->
 	let ty, impsty = interp_type_evars_impls ~impls ~evdref ~fail_evar:false env_bl ctyp in
-	let c, imps2 = interp_casted_constr_evars_impls ~impls ~evdref ~fail_evar:false env_bl c ty in
+	let c, imps2 = interp_casted_constr_evars_impls ~impls ~evdref ~fail_evar env_bl c ty in
 	let body = nf_evar !evdref (it_mkLambda_or_LetIn c ctx) in
 	let typ = nf_evar !evdref (it_mkProd_or_LetIn ty ctx) in
         let beq b1 b2 = if b1 then b2 else not b2 in
@@ -155,7 +155,7 @@ let declare_definition ident (local, k) ce imps hook =
 let _ = Obligations.declare_definition_ref := declare_definition
 
 let do_definition ident k bl red_option c ctypopt hook =
-  let (ce, evd, imps as def) = interp_definition bl red_option c ctypopt in
+  let (ce, evd, imps as def) = interp_definition bl red_option (not (Flags.is_program_mode ())) c ctypopt in
     if Flags.is_program_mode () then
       let env = Global.env () in
       let c = ce.const_entry_body in
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 08151c859e..7e7586c5cc 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -32,7 +32,7 @@ val set_declare_assumptions_hook : (types -> unit) -> unit
 (** {6 Definitions/Let} *)
 
 val interp_definition :
-  local_binder list -> red_expr option -> constr_expr ->
+  local_binder list -> red_expr option -> bool (* Fail if evars remain *) -> constr_expr ->
   constr_expr option -> definition_entry * Evd.evar_map * Impargs.manual_implicits
 
 val declare_definition : Id.t -> definition_kind ->