revert commit 12650 for the moment, since it breaks MSetAVL

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

2 files changed, 12 insertions, 47 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 86f4eba435..af81c7302e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -863,32 +863,18 @@ let simplest_case c = general_case_analysis false (c,NoBindings)
 
 (* Apply a tactic below the products of the conclusion of a lemma *)
 
-type conjunction_status =
-  | DefinedRecord of constant option list
-  | NotADefinedRecordUseScheme of constr
-
 let make_projection params cstr sign elim i n c =
-  match elim with
-  | NotADefinedRecordUseScheme elim ->
-      let (na,b,t) = List.nth cstr.cs_args i in
-      let b = match b with None -> mkRel (i+1) | Some b -> b in
-      let branch = it_mkLambda_or_LetIn b cstr.cs_args in
-      if noccur_between 1 (n-i-1) t then
-	let t = lift (i+1-n) t in
-	let args = params@[t;branch;mkApp (c,extended_rel_vect 0 sign)] in
-	let p = it_mkLambda_or_LetIn (beta_applist (elim,args)) sign in
-	let pt = it_mkProd_or_LetIn t sign in
-	Some (p,pt)
-      else
-	None
-  | DefinedRecord l ->
-      match List.nth l i with
-      | Some proj ->
-	  let t = Typeops.type_of_constant (Global.env()) proj in
-	  let args = params@[c] in
-	  Some (applist (mkConst proj,args),prod_applist t args)
-      | None -> None
-
+  let (na,b,t) = List.nth cstr.cs_args i in
+  let b = match b with None -> mkRel (i+1) | Some b -> b in
+  let branch = it_mkLambda_or_LetIn b cstr.cs_args in
+  if noccur_between 1 (n-i-1) t then
+    let t = lift (i+1-n) t in
+    let args = params@[t;branch;mkApp (c,extended_rel_vect 0 sign)] in
+    let p = it_mkLambda_or_LetIn (beta_applist (elim,args)) sign in
+    let pt = it_mkProd_or_LetIn t sign in
+    Some (p,pt)
+  else
+    None
 
 let descend_in_conjunctions tac exit c gl =
   try
@@ -902,11 +888,7 @@ let descend_in_conjunctions tac exit c gl =
 	let IndType (indf,_) = pf_apply find_rectype gl ccl in
 	let params = snd (dest_ind_family indf) in
 	let cstr = (get_constructors (pf_env gl) indf).(0) in
-	let elim =
-	  try DefinedRecord (Recordops.lookup_projections ind)
-	  with Not_found ->
-	    let elim = pf_apply build_case_analysis_scheme gl ind false sort in
-	    NotADefinedRecordUseScheme elim in
+	let elim = pf_apply build_case_analysis_scheme gl ind false sort in
 	tclFIRST
 	  (list_tabulate (fun i gl ->
 	    match make_projection params cstr sign elim i n c with
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index cb55432fb7..3fc8a97922 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -348,20 +348,3 @@ Goal True.
 eapply (fun (A:Prop) (x:A) => conj I x).
 exact I.
 Qed.
-
-(* The following was not accepted from r12612 to r12649 *)
-
-Record sig0 := { p1 : nat; p2 : p1 = 0 }.
-
-Goal forall x : sig0, p1 x = 0.
-intro x;
-apply x.
-Qed.
-
-(* The following was accepted before r12612 but is still not accepted in r12650
-
-Goal forall x : { x:nat | x = 0}, proj1_sig x = 0.
-intro x;
-apply x.
-
-*)