Debug implementation of dependent induction/dependent destruction and document it.

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

1 files changed, 14 insertions, 35 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index dbd3aacbff..3be4f0f137 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1708,15 +1708,17 @@ let lift_together l = lift_togethern 0 l
 
 let lift_list l = List.map (lift 1) l
 
-let make_abstract_generalize gl id concl ctx c eqs args refls coe = 
+let make_abstract_generalize gl id concl ctx c eqs args refls = 
   let meta = Evarutil.new_meta() in
   let cstr = 
-    (* Substitute the coerced term using equalities into the conclusion. *)
-    let concl = subst1 coe (subst_var id concl) in
     (* Abstract by equalitites *)
     let abseqs = it_mkProd_or_LetIn ~init:concl (List.map (fun x -> (Anonymous, None, x)) eqs) in 
-    (* Abstract by the "generalized" hypothesis *)
-    let abshyp = mkProd (Name id, c, abseqs) in
+    (* Abstract by the "generalized" hypothesis and its equality proof *)
+    let term, typ = mkVar id, pf_get_hyp_typ gl id in
+    let abshyp = 
+      let abshypeq = mkProd (Anonymous, mkHEq (lift 1 c) (mkRel 1) typ term, lift 1 abseqs) in
+	mkProd (Name id, c, abshypeq)
+    in
     (* Abstract by the extension of the context *)
     let genctyp = it_mkProd_or_LetIn ~init:abshyp ctx in
     (* The goal will become this product. *)
@@ -1725,7 +1727,9 @@ let make_abstract_generalize gl id concl ctx c eqs args refls coe =
     let instc = mkApp (genc, Array.of_list args) in
     (* Then apply to the original instanciated hyp. *)
     let newc = mkApp (instc, [| mkVar id |]) in
-    (* Finaly, apply the reflexivity proofs, to get a term of type gl again *)
+    (* Apply the reflexivity proof for the original hyp. *)
+    let newc = mkApp (newc, [| mkHRefl typ term |]) in
+    (* Finaly, apply the remaining reflexivity proofs on the index, to get a term of type gl again *)
     let appeqs = mkApp (newc, Array.of_list refls) in
       appeqs
   in cstr
@@ -1781,40 +1785,15 @@ let abstract_args gl id =
 	let arity, ctx, ctxenv, c', args, eqs, refls, finalargs, env = 
 	  Array.fold_left aux (pf_type_of gl f,[],env,f,[],[],[],[],env) args
 	in
-	let _, _, _, coe = 
-	  let alleqslen = List.length eqs in
-	  let ctxlen = List.length ctx in
-	  let n_lift = alleqslen + ctxlen + 1 in
-	  let aux (prod, c, eqsrel, coe) (name, arg, oldarg) after =
-	    let (name, ty, arity) = destProd prod in
-	      match kind_of_term oldarg with
-		| Var _ | Rel _ -> 
-		    (subst1 arg arity, mkApp (c, [|arg|]), eqsrel, coe)
-		| _ ->
-		    let c' = mkApp (c, [|arg|]) in
-		    let pred = 
-		      mkLambda (name, ty, applist (lift 1 c, (mkRel 1) :: 
-			List.map (fun (_, x, _) -> lift 1 x) after))
-		    in
-		    let coe' =
-		      mkCoe ty arg pred coe oldarg (mkRel eqsrel)
-		    in
-		      (arity, c', eqsrel - 1, coe')
-	  in 
-	  let rec fold acc l =
-	    match l with
-	      | hd :: tl -> fold (aux acc hd tl) tl
-	      | [] -> acc
-	  in
-	    fold (lift n_lift (pf_type_of gl f), lift n_lift f, alleqslen, mkRel (succ alleqslen)) 
-	      (List.rev_map (fun (x, y, z) -> x, lift (alleqslen + 1) y, lift (alleqslen + 1) z) finalargs)
-	in
 	let eqs = lift_togethern 1 eqs in
 	let args, refls = List.rev args, List.rev refls in
-	  Some (make_abstract_generalize gl id concl ctx c' eqs args refls coe)
+	  Some (make_abstract_generalize gl id concl ctx c' eqs args refls)
     | _ -> None
 
 let abstract_generalize id gl =
+  Coqlib.check_required_library ["Coq";"Logic";"JMeq"];
+(*   let qualid = (dummy_loc, qualid_of_dirpath (dirpath_of_string "Coq.Logic.JMeq")) in *)
+(*   Library.require_library [qualid] None; *)
   let newc = abstract_args gl id in
     match newc with
       | None -> tclIDTAC gl