Fix a bunch of bugs related to setoid_rewrite, unification and evars:

- Really unify with types of metas when they contain metas
_or_ evars (why not always?) (fixes bug #2027).
- Better handling of evars in rewrite lemmas when using setoid_rewrite
through rewrite (reported by Ralf Hinze).
- Use retyping with metas when possible (check?) and improve an
obscure error message in retyping.


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

4 files changed, 29 insertions, 29 deletions

diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 532c258fa..2460c7642 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -49,7 +49,7 @@ let retype sigma metamap =
     match kind_of_term cstr with
     | Meta n ->
           (try strip_outer_cast (List.assoc n metamap)
-           with Not_found -> anomaly "type_of: this is not a well-typed term")
+           with Not_found -> anomaly ("type_of: unknown meta " ^ string_of_int n))
     | Rel n ->
         let (_,_,ty) = lookup_rel n env in
         lift n ty
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index e072af362..6c7ca8af2 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -481,7 +481,7 @@ let w_coerce_to_type env evd c cty mvty =
     try_to_coerce env evd c cty tycon
 
 let w_coerce env evd mv c =
-  let cty = get_type_of env (evars_of evd) c in
+  let cty = get_type_of_with_meta env (evars_of evd) (metas_of evd) c in
   let mvty = Typing.meta_type evd mv in
   w_coerce_to_type env evd c cty mvty
 
@@ -496,7 +496,7 @@ let unify_to_type env evd flags c u =
 
 let unify_type env evd flags mv c =
   let mvty = Typing.meta_type evd mv in
-  if occur_meta mvty then
+  if occur_meta_or_existential mvty then
     unify_to_type env evd flags c mvty
   else ([],[])
 
@@ -589,7 +589,7 @@ let w_merge env with_types flags (metas,evars) evd =
     let (evd', c) = applyHead sp_env evd nargs hdc in
     let (mc,ec) =
       unify_0 sp_env (evars_of evd') Cumul flags
-        (Retyping.get_type_of sp_env (evars_of evd') c) ev.evar_concl in
+        (Retyping.get_type_of_with_meta sp_env (evars_of evd') (metas_of evd') c) ev.evar_concl in
     let evd'' = w_merge_rec evd' mc ec [] in
     if (evars_of evd') == (evars_of evd'')
     then Evd.evar_define sp c evd''
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index b6272115a..e38b9a6e6 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -814,23 +814,7 @@ let unify_eqn env sigma hypinfo t =
       let left = if l2r then c1 else c2 in
 	match abs with
 	    Some (absprf, absprfty) -> 
-	      (*if convertible env cl.evd left t then
-		cl, prf, c1, c2, car, rel
-	      else raise Not_found*)
 	      let env' = clenv_unify allowK ~flags:rewrite2_unif_flags CONV left t cl in
-	      let env' =
-		let mvs = clenv_dependent false env' in
-		  clenv_pose_metas_as_evars env' mvs
-	      in
-	      let evd' = Typeclasses.resolve_typeclasses ~fail:false env'.env env'.evd in
-	      let env' = { env' with evd = evd' } in
-	      let c1 = Clenv.clenv_nf_meta env' c1
-	      and c2 = Clenv.clenv_nf_meta env' c2
-	      and car = Clenv.clenv_nf_meta env' car
-	      and rel = Clenv.clenv_nf_meta env' rel in
-		hypinfo := { !hypinfo with
-		  cl = env';
-		  abs = Some (Clenv.clenv_value env', Clenv.clenv_type env') };
 		env', prf, c1, c2, car, rel
 	  | None ->
 	      let env' =
@@ -1573,25 +1557,30 @@ let check_evar_map_of_evars_defs evd =
    ) metas
 
 let unification_rewrite l2r c1 c2 cl car rel but gl = 
-  let (env',c') =
+  let env = pf_env gl in
+  let (evd',c') =
     try
       (* ~flags:(false,true) to allow to mark occurrences that must not be
          rewritten simply by replacing them with let-defined definitions
          in the context *)
-      Unification.w_unify_to_subterm ~flags:rewrite_unif_flags (pf_env gl) ((if l2r then c1 else c2),but) cl.evd
+      Unification.w_unify_to_subterm ~flags:rewrite_unif_flags env ((if l2r then c1 else c2),but) cl.evd
     with
 	Pretype_errors.PretypeError _ ->
 	  (* ~flags:(true,true) to make Ring work (since it really
              exploits conversion) *)
 	  Unification.w_unify_to_subterm ~flags:rewrite2_unif_flags
-	    (pf_env gl) ((if l2r then c1 else c2),but) cl.evd
+	    env ((if l2r then c1 else c2),but) cl.evd
+  in
+  let evd' = Typeclasses.resolve_typeclasses ~fail:false env evd' in
+  let cl' = {cl with evd = evd'} in
+  let cl' =
+    let mvs = clenv_dependent false cl' in
+      clenv_pose_metas_as_evars cl' mvs
   in
-  let cl' = {cl with evd = env'} in
-  let c1 = Clenv.clenv_nf_meta cl' c1 
-  and c2 = Clenv.clenv_nf_meta cl' c2 in
-  check_evar_map_of_evars_defs env';
-  let prf = Clenv.clenv_value cl' in
-  let prfty = Clenv.clenv_type cl' in
+  let nf c = Evarutil.nf_evar (Evd.evars_of cl'.evd) (Clenv.clenv_nf_meta cl' c) in
+  let c1 = nf c1 and c2 = nf c2 and car = nf car and rel = nf rel in
+  check_evar_map_of_evars_defs cl'.evd;
+  let prf = nf (Clenv.clenv_value cl') and prfty = nf (Clenv.clenv_type cl') in
   let cl' = { cl' with templval = mk_freelisted prf ; templtyp = mk_freelisted prfty } in
     {cl=cl'; prf=(mkRel 1); car=car; rel=rel; l2r=l2r; c1=c1; c2=c2; c=None; abs=Some (prf, prfty)}
 
diff --git a/test-suite/bugs/closed/shouldsucceed/2027.v b/test-suite/bugs/closed/shouldsucceed/2027.v
new file mode 100644
index 000000000..fb53c6ef4
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2027.v
@@ -0,0 +1,11 @@
+
+Parameter T : Type -> Type.
+Parameter f : forall {A}, T A -> T A.
+Parameter P : forall {A}, T A -> Prop.
+Axiom f_id : forall {A} (l : T A), f l = l.
+
+Goal forall A (p : T A), P p.
+Proof.
+  intros.
+  rewrite <- f_id.
+Admitted.
\ No newline at end of file