Temporary fix to compensate the loss of descent on dependent

conjunctions (defined records now supported again but not unregistered ones).



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

1 files changed, 30 insertions, 12 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index af81c7302..86f4eba43 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -863,18 +863,32 @@ 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 =
-  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
+  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 descend_in_conjunctions tac exit c gl =
   try
@@ -888,7 +902,11 @@ 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 = pf_apply build_case_analysis_scheme gl ind false sort 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
 	tclFIRST
 	  (list_tabulate (fun i gl ->
 	    match make_projection params cstr sign elim i n c with