MAJ

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

2 files changed, 101 insertions, 94 deletions

diff --git a/.depend b/.depend
index 0e7a2792d..dabc858e5 100644
--- a/.depend
+++ b/.depend
@@ -154,7 +154,6 @@ tactics/hipattern.cmi: kernel/evd.cmi kernel/names.cmi proofs/pattern.cmi \
 tactics/inv.cmi: parsing/coqast.cmi kernel/names.cmi proofs/tacmach.cmi 
 tactics/nbtermdn.cmi: tactics/btermdn.cmi kernel/generic.cmi \
     proofs/pattern.cmi kernel/term.cmi 
-tactics/stock.cmi: kernel/names.cmi 
 tactics/tacentries.cmi: proofs/proof_type.cmi proofs/tacmach.cmi 
 tactics/tacticals.cmi: proofs/clenv.cmi parsing/coqast.cmi kernel/names.cmi \
     proofs/pattern.cmi proofs/proof_type.cmi kernel/reduction.cmi \
@@ -808,52 +807,54 @@ tactics/equality.cmo: parsing/astterm.cmi parsing/coqast.cmi \
     lib/gmapl.cmi tactics/hipattern.cmi kernel/inductive.cmi \
     kernel/instantiate.cmi library/lib.cmi library/libobject.cmi \
     proofs/logic.cmi kernel/names.cmi proofs/pattern.cmi lib/pp.cmi \
-    proofs/proof_type.cmi kernel/reduction.cmi library/summary.cmi \
-    proofs/tacinterp.cmi proofs/tacmach.cmi pretyping/tacred.cmi \
-    tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \
-    kernel/typeops.cmi pretyping/typing.cmi kernel/univ.cmi lib/util.cmi \
-    toplevel/vernacinterp.cmi tactics/wcclausenv.cmi tactics/equality.cmi 
+    proofs/proof_type.cmi kernel/reduction.cmi pretyping/retyping.cmi \
+    library/summary.cmi proofs/tacinterp.cmi proofs/tacmach.cmi \
+    pretyping/tacred.cmi tactics/tacticals.cmi tactics/tactics.cmi \
+    kernel/term.cmi kernel/typeops.cmi pretyping/typing.cmi kernel/univ.cmi \
+    lib/util.cmi toplevel/vernacinterp.cmi tactics/wcclausenv.cmi \
+    tactics/equality.cmi 
 tactics/equality.cmx: parsing/astterm.cmx parsing/coqast.cmx \
     kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx library/global.cmx \
     lib/gmapl.cmx tactics/hipattern.cmx kernel/inductive.cmx \
     kernel/instantiate.cmx library/lib.cmx library/libobject.cmx \
     proofs/logic.cmx kernel/names.cmx proofs/pattern.cmx lib/pp.cmx \
-    proofs/proof_type.cmx kernel/reduction.cmx library/summary.cmx \
-    proofs/tacinterp.cmx proofs/tacmach.cmx pretyping/tacred.cmx \
-    tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \
-    kernel/typeops.cmx pretyping/typing.cmx kernel/univ.cmx lib/util.cmx \
-    toplevel/vernacinterp.cmx tactics/wcclausenv.cmx tactics/equality.cmi 
+    proofs/proof_type.cmx kernel/reduction.cmx pretyping/retyping.cmx \
+    library/summary.cmx proofs/tacinterp.cmx proofs/tacmach.cmx \
+    pretyping/tacred.cmx tactics/tacticals.cmx tactics/tactics.cmx \
+    kernel/term.cmx kernel/typeops.cmx pretyping/typing.cmx kernel/univ.cmx \
+    lib/util.cmx toplevel/vernacinterp.cmx tactics/wcclausenv.cmx \
+    tactics/equality.cmi 
 tactics/hiddentac.cmo: proofs/proof_type.cmi tactics/tacentries.cmi \
     proofs/tacmach.cmi kernel/term.cmi tactics/hiddentac.cmi 
 tactics/hiddentac.cmx: proofs/proof_type.cmx tactics/tacentries.cmx \
     proofs/tacmach.cmx kernel/term.cmx tactics/hiddentac.cmi 
 tactics/hipattern.cmo: parsing/astterm.cmi proofs/clenv.cmi \
-    kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi library/global.cmi \
-    kernel/names.cmi proofs/pattern.cmi parsing/pcoq.cmi lib/pp.cmi \
-    parsing/printer.cmi proofs/proof_trees.cmi kernel/reduction.cmi \
-    kernel/sosub.cmi proofs/stock.cmi kernel/term.cmi lib/util.cmi \
-    tactics/hipattern.cmi 
+    library/declare.cmi kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \
+    library/global.cmi library/library.cmi kernel/names.cmi \
+    proofs/pattern.cmi parsing/pcoq.cmi lib/pp.cmi parsing/printer.cmi \
+    proofs/proof_trees.cmi kernel/reduction.cmi kernel/sosub.cmi \
+    proofs/stock.cmi kernel/term.cmi lib/util.cmi tactics/hipattern.cmi 
 tactics/hipattern.cmx: parsing/astterm.cmx proofs/clenv.cmx \
-    kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx library/global.cmx \
-    kernel/names.cmx proofs/pattern.cmx parsing/pcoq.cmx lib/pp.cmx \
-    parsing/printer.cmx proofs/proof_trees.cmx kernel/reduction.cmx \
-    kernel/sosub.cmx proofs/stock.cmx kernel/term.cmx lib/util.cmx \
-    tactics/hipattern.cmi 
+    library/declare.cmx kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \
+    library/global.cmx library/library.cmx kernel/names.cmx \
+    proofs/pattern.cmx parsing/pcoq.cmx lib/pp.cmx parsing/printer.cmx \
+    proofs/proof_trees.cmx kernel/reduction.cmx kernel/sosub.cmx \
+    proofs/stock.cmx kernel/term.cmx lib/util.cmx tactics/hipattern.cmi 
 tactics/inv.cmo: tactics/auto.cmi proofs/clenv.cmi tactics/elim.cmi \
     kernel/environ.cmi tactics/equality.cmi kernel/evd.cmi kernel/generic.cmi \
     library/global.cmi library/indrec.cmi kernel/names.cmi proofs/pattern.cmi \
-    lib/pp.cmi parsing/printer.cmi proofs/proof_trees.cmi \
-    kernel/reduction.cmi pretyping/retyping.cmi kernel/sign.cmi \
-    proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \
-    kernel/term.cmi kernel/typeops.cmi pretyping/typing.cmi lib/util.cmi \
+    lib/pp.cmi parsing/printer.cmi proofs/proof_type.cmi kernel/reduction.cmi \
+    pretyping/retyping.cmi kernel/sign.cmi proofs/tacmach.cmi \
+    tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \
+    kernel/typeops.cmi pretyping/typing.cmi lib/util.cmi \
     tactics/wcclausenv.cmi tactics/inv.cmi 
 tactics/inv.cmx: tactics/auto.cmx proofs/clenv.cmx tactics/elim.cmx \
     kernel/environ.cmx tactics/equality.cmx kernel/evd.cmx kernel/generic.cmx \
     library/global.cmx library/indrec.cmx kernel/names.cmx proofs/pattern.cmx \
-    lib/pp.cmx parsing/printer.cmx proofs/proof_trees.cmx \
-    kernel/reduction.cmx pretyping/retyping.cmx kernel/sign.cmx \
-    proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
-    kernel/term.cmx kernel/typeops.cmx pretyping/typing.cmx lib/util.cmx \
+    lib/pp.cmx parsing/printer.cmx proofs/proof_type.cmx kernel/reduction.cmx \
+    pretyping/retyping.cmx kernel/sign.cmx proofs/tacmach.cmx \
+    tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \
+    kernel/typeops.cmx pretyping/typing.cmx lib/util.cmx \
     tactics/wcclausenv.cmx tactics/inv.cmi 
 tactics/leminv.cmo: proofs/clenv.cmi library/declare.cmi \
     toplevel/discharge.cmi kernel/environ.cmi tactics/equality.cmi \
@@ -879,10 +880,6 @@ tactics/nbtermdn.cmx: tactics/btermdn.cmx kernel/generic.cmx lib/gmap.cmx \
     library/libobject.cmx library/library.cmx kernel/names.cmx \
     proofs/pattern.cmx kernel/term.cmx tactics/termdn.cmx lib/util.cmx \
     tactics/nbtermdn.cmi 
-tactics/stock.cmo: lib/bij.cmi lib/gmap.cmi lib/gmapl.cmi library/library.cmi \
-    kernel/names.cmi lib/pp.cmi lib/util.cmi tactics/stock.cmi 
-tactics/stock.cmx: lib/bij.cmx lib/gmap.cmx lib/gmapl.cmx library/library.cmx \
-    kernel/names.cmx lib/pp.cmx lib/util.cmx tactics/stock.cmi 
 tactics/tacentries.cmo: proofs/proof_trees.cmi proofs/tacmach.cmi \
     tactics/tacticals.cmi tactics/tactics.cmi tactics/tacentries.cmi 
 tactics/tacentries.cmx: proofs/proof_trees.cmx proofs/tacmach.cmx \
@@ -943,8 +940,10 @@ tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx kernel/evd.cmx \
     lib/pp.cmx proofs/proof_trees.cmx kernel/reduction.cmx kernel/sign.cmx \
     proofs/tacmach.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \
     tactics/wcclausenv.cmi 
-tools/coqdep.cmo: config/coq_config.cmi 
-tools/coqdep.cmx: config/coq_config.cmx 
+tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo 
+tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx 
+tools/coqdep_lexer.cmo: config/coq_config.cmi 
+tools/coqdep_lexer.cmx: config/coq_config.cmx 
 toplevel/command.cmo: parsing/ast.cmi parsing/astterm.cmi kernel/constant.cmi \
     parsing/coqast.cmi library/declare.cmi kernel/environ.cmi kernel/evd.cmi \
     kernel/generic.cmi library/global.cmi library/indrec.cmi \
@@ -1105,14 +1104,14 @@ contrib/omega/coq_omega.cmo: parsing/ast.cmi proofs/clenv.cmi \
     library/declare.cmi kernel/environ.cmi tactics/equality.cmi \
     kernel/generic.cmi library/global.cmi kernel/inductive.cmi \
     proofs/logic.cmi kernel/names.cmi contrib/omega/omega.cmo lib/pp.cmi \
-    parsing/printer.cmi proofs/proof_trees.cmi kernel/reduction.cmi \
+    parsing/printer.cmi proofs/proof_type.cmi kernel/reduction.cmi \
     kernel/sign.cmi proofs/tacmach.cmi tactics/tactics.cmi kernel/term.cmi \
     lib/util.cmi 
 contrib/omega/coq_omega.cmx: parsing/ast.cmx proofs/clenv.cmx \
     library/declare.cmx kernel/environ.cmx tactics/equality.cmx \
     kernel/generic.cmx library/global.cmx kernel/inductive.cmx \
     proofs/logic.cmx kernel/names.cmx contrib/omega/omega.cmx lib/pp.cmx \
-    parsing/printer.cmx proofs/proof_trees.cmx kernel/reduction.cmx \
+    parsing/printer.cmx proofs/proof_type.cmx kernel/reduction.cmx \
     kernel/sign.cmx proofs/tacmach.cmx tactics/tactics.cmx kernel/term.cmx \
     lib/util.cmx 
 contrib/omega/omega.cmo: lib/util.cmi 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 72f02e720..02944443a 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -13,6 +13,7 @@ open Reduction
 open Instantiate
 open Typeops
 open Typing
+open Retyping
 open Tacmach
 open Proof_type
 open Logic
@@ -181,6 +182,13 @@ type leibniz_eq = {
   congr: marked_term;
   sym  : marked_term }
 
+type sigma_type = {
+  proj1 : constr;
+  proj2 : constr;
+  elim  : constr;
+  intro : constr;
+  ex    : constr }
+
 let mmk = make_module_marker [ "Prelude"; "Logic_Type"; "Specif"; "Logic" ]
 
 (* Patterns *)
@@ -684,43 +692,45 @@ let h_discrHyp   = hide_ident_tactic  "DiscrHyp"   discrHyp
  *  re-lift it. *)
 
 let bind_ith na i t = lift i (DLAM(na,lift (-(i-1)) t))
-
+(*
 let existS_term = put_squel mmk "existS"
-let existS_pattern = put_pat mmk "(existS ? ? ? ?)"
 let sigS_term = put_squel mmk "sigS"
 let projS1_term = put_squel mmk "projS1"
 let projS2_term = put_squel mmk "projS2"
 let sigS_rec_term = put_squel mmk "sigS_rec"
-
+*)
+let existS_pattern = put_pat mmk "(existS ? ? ? ?)"
+(*
 let existT_term = put_squel mmk "existT"
-let existT_pattern = put_pat mmk "(existT ? ? ? ?)"
 let sigT_term = put_squel mmk "sigT"
 let projT1_term = put_squel mmk "projT1"
 let projT2_term = put_squel mmk "projT2"
 let sigT_rect_term = put_squel mmk "sigT_rect"
+*)
+let existT_pattern = put_pat mmk "(existT ? ? ? ?)"
 
-let build_sigma_prop () =
-  (fst (destConst (get_squel projS1_term)),
-   fst (destConst (get_squel projS2_term)),
-   fst (destConst (get_squel sigS_rec_term)),
-   get_squel existS_term,
-   get_squel sigS_term)
+let build_sigma_set () =
+  { proj1 = get_reference ["Specif"] "projS1";
+    proj2 = get_reference ["Specif"] "projS2";
+    elim = get_reference ["Specif"] "sigS_rec";
+    intro = get_reference ["Specif"] "existS";
+    ex = get_reference ["Specif"] "sigS" }
 
 let build_sigma_type () =
-  (fst (destConst (get_squel projT1_term)),
-   fst (destConst (get_squel projT2_term)),
-   fst (destConst (get_squel sigT_rect_term)),
-   get_squel existT_term,
-   get_squel sigT_term)
+  { proj1 = get_reference ["Specif"] "projT1";
+    proj2 = get_reference ["Specif"] "projT2";
+    elim = get_reference ["Specif"] "sigT_rec";
+    intro = get_reference ["Specif"] "existT";
+    ex = get_reference ["Specif"] "sigT" }
 
 (* returns the sigma type (sigS, sigT) with the respective
     constructor depending on the sort *)
 
 let find_sigma_data s =
-  match strip_outer_cast s with  
-    | DOP0(Sort(Prop Pos)) -> build_sigma_prop ()                  (* Set *) 
-    | DOP0(Sort(Type(_))) -> build_sigma_type ()                   (* Type *)
-    |   _     -> error "find_sigma_data"
+  match s with  
+    | Prop Pos  -> build_sigma_set ()                    (* Set *) 
+    | Type _    -> build_sigma_type ()                   (* Type *)
+    | Prop Null -> error "find_sigma_data"
 
 (* [make_tuple env na lind rterm rty]
 
@@ -740,8 +750,8 @@ let find_sigma_data s =
 
 let make_tuple sigma env na lind rterm rty =
   if dependent (Rel lind) rty then
-    let (_,_,_,exist_term,sig_term) =
-      find_sigma_data (type_of env sigma rty) in
+    let {intro = exist_term; ex = sig_term} =
+      find_sigma_data (get_sort_of env sigma rty) in
     let a = type_of env sigma (Rel lind) in
     let p = DOP2(Lambda,a,
                  bind_ith (fst(lookup_rel lind env)) lind rty) in
@@ -787,7 +797,7 @@ let minimal_free_rels env sigma (c,cty) =
  *)
 
 let sig_clausale_forme env sigma sort_of_ty siglen ty (dFLT,dFLTty) =
-  let (_,_,_,exist_term,_) = find_sigma_data sort_of_ty in 
+  let { ex = exist_term } = find_sigma_data sort_of_ty in 
   let rec sigrec_clausale_forme siglen ty =
     if siglen = 0 then
       (* We obtain the components dependent in dFLT by matching *)
@@ -850,7 +860,7 @@ let sig_clausale_forme env sigma sort_of_ty siglen ty (dFLT,dFLTty) =
 
 let make_iterated_tuple sigma env (dFLT,dFLTty) (c,cty) =
   let (cty,rels) = minimal_free_rels env sigma (c,cty) in
-  let sort_of_cty = type_of env sigma cty in
+  let sort_of_cty = get_sort_of env sigma cty in
   let sorted_rels = Sort.list (>=) (Intset.elements rels) in
   let (tuple,tuplety) =
     List.fold_left (fun (rterm,rty) lind ->
@@ -1167,12 +1177,13 @@ let bareRevSubstInConcl lbeq body (t,e1,e2) gls =
 
  *)
 
-(* squeletons *)
+(*
 let comp_carS_squeleton = put_squel mmk "<<x>>(projS1 ? ? (?)@[x])"
 let comp_cdrS_squeleton = put_squel mmk "<<x>>(projS2 ? ? (?)@[x])"
 
 let comp_carT_squeleton = put_squel mmk "<<x>>(projT1 ? ? (?)@[x])"
 let comp_cdrT_squeleton = put_squel mmk "<<x>>(projT2 ? ? (?)@[x])"
+*)
 
 let match_sigma ex ex_pat =
   match matches (get_pat ex_pat) ex with
@@ -1181,48 +1192,45 @@ let match_sigma ex ex_pat =
 	anomaly "match_sigma: a successful sigma pattern should match 4 terms"
 
 let find_sigma_data_decompose ex =
-  try 
-    (comp_carS_squeleton, comp_cdrS_squeleton,
-     match_sigma ex existS_pattern)
-  with PatternMatchingFailure -> 
+  try
+    let subst = match_sigma ex existS_pattern in
+    (build_sigma_set (),subst)
+  with PatternMatchingFailure ->
     (try 
-       (comp_carT_squeleton,comp_cdrT_squeleton,
-        match_sigma ex existT_pattern)   
+       let subst = match_sigma ex existT_pattern in
+       (build_sigma_type (),subst)
      with PatternMatchingFailure -> 
        errorlabstrm "find_sigma_data_decompose" [< >])
 
-let decomp_tuple_term env = 
-  let rec decomprec to_here_fun ex =
+let decomp_tuple_term env c t = 
+  let rec decomprec inner_code ex exty =
     try
-      let (comp_car_squeleton,comp_cdr_squeleton,(a,p,car,cdr)) =
-	find_sigma_data_decompose  ex in
-      let car_code = soinstance comp_car_squeleton [a;p;to_here_fun]
-      and cdr_code = soinstance comp_cdr_squeleton [a;p;to_here_fun] in
-      (car,named_hd env a Anonymous,car_code)::(decomprec cdr_code cdr)
+      let {proj1 = p1; proj2 = p2 },(a,p,car,cdr) =
+	find_sigma_data_decompose ex in
+      let car_code = applist (p1,[a;p;inner_code])
+      and cdr_code = applist (p2,[a;p;inner_code]) in
+      let cdrtyp = beta_applist (p,[car]) in
+      ((car,a),car_code)::(decomprec cdr_code cdr cdrtyp)
     with e when catchable_exception e ->
-      [(ex,named_hd env ex Anonymous,to_here_fun)]
+      [((ex,exty),inner_code)]
   in
-  decomprec (DLAM(Anonymous,Rel 1))
+  List.split (decomprec (Rel 1) c t)
 
 let subst_tuple_term env sigma dep_pair b =
-  let sort_of_dep_pair =
-    type_of env sigma (type_of env sigma dep_pair) in
-  let (proj1_sp,proj2_sp,sig_elim_sp,_,_) =
-    find_sigma_data sort_of_dep_pair in 
-  let e_list = decomp_tuple_term env dep_pair in
+  let typ = get_type_of env sigma dep_pair in
+  let e_list,proj_list = decomp_tuple_term env dep_pair typ in
   let abst_B =
-    List.fold_right (fun (e,na,_) b ->
-                       let body = subst_term e b in
-                       let pB = DLAM(na,body) in
-		       DOP2(Lambda,type_of env sigma e,pB))
-      e_list b 
-  in
-  let app_B = 
-    applist(abst_B,(List.map (fun (_,_,c) -> (sAPP c (Rel 1))) e_list)) in
+    List.fold_right
+      (fun (e,t) body -> lambda_create env (t,subst_term e body)) e_list b in
+  let app_B = applist(abst_B,proj_list) in
+  (* inutile ?? les projs sont appliquées à (Rel 1) ?? *)
+(*
+  let { proj1 = proj1_sp; proj2 = proj2_sp; elim = sig_elim_sp } =
+    find_sigma_data (get_sort_of env sigma typ) in
   strong (fun _ _ -> 
 	    compose (whd_betaiota env sigma)
 	      (whd_const [proj1_sp;proj2_sp;sig_elim_sp] env sigma)) 
-    env sigma app_B
+    env sigma*) app_B
     
 (* |- (P e2)
      BY RevSubstInConcl (eq T e1 e2)
@@ -1232,7 +1240,7 @@ let subst_tuple_term env sigma dep_pair b =
 let revSubstInConcl eqn gls =
   let (lbeq,(t,e1,e2)) = find_eq_data_decompose eqn in
   let body = subst_tuple_term (pf_env gls) (project gls) e2 (pf_concl gls) in
-  if not (dependent (Rel 1) body) then errorlabstrm  "RevSubstInConcl" [<>];
+  assert (not (dependent (Rel 1) body));
   bareRevSubstInConcl lbeq body (t,e1,e2) gls
 
 (* |- (P e1)
@@ -1610,9 +1618,9 @@ let substHypInConcl_RL_tac =
     id:a=b H:(P a) |- G
 *)
 
-(***************)
-(* AutoRewrite *)
-(***************)
+(**********************************************************************)
+(*                    AutoRewrite                                     *)
+(**********************************************************************)
 
 (****Dealing with the rewriting rules****)