- Déplacement des types paramétriques prod, sum, option, identity,

  sig, sig2, sumor, list et vector dans Type
- Branchement de prodT/listT vers les nouveaux prod/list
- Abandon sigS/sigS2 au profit de sigT et du nouveau sigT2
- Changements en conséquence dans les théories (notamment Field_Tactic),
  ainsi que dans les modules ML Coqlib/Equality/Hipattern/Field


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

3 files changed, 7 insertions, 10 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 6239879c99..34cfefd5d4 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -547,8 +547,7 @@ let discrHyp id gls = discrClause (onHyp id) gls
 
 let find_sigma_data s =
   match s with  
-    | Prop Pos  -> build_sigma_set ()                    (* Set *) 
-    | Type _    -> build_sigma_type ()                   (* Type *)
+    | Prop Pos  | Type _    -> build_sigma_type ()          (* Set/Type *)
     | Prop Null -> error "find_sigma_data"
 
 (* [make_tuple env sigma (rterm,rty) lind] assumes [lind] is the lesser
@@ -556,7 +555,7 @@ let find_sigma_data s =
 
    Then we build the term
 
-     [(existS A P (mkRel lind) rterm)] of type [(sigS A P)]
+     [(existT A P (mkRel lind) rterm)] of type [(sigS A P)]
 
    where [A] is the type of [mkRel lind] and [P] is [\na:A.rty{1/lind}]
  *)
@@ -687,7 +686,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
    [make_iterated_tuple sigma env (term,typ) (z,zty)] is to build the
    tuple
 
-   [existS [xn]Pn Rel(in) .. (existS [x2]P2 Rel(i2) (existS [x1]P1 Rel(i1) z))]
+   [existT [xn]Pn Rel(in) .. (existT [x2]P2 Rel(i2) (existT [x1]P1 Rel(i1) z))]
 
    where P1 is zty[i1/x1], P2 is {x1 | P1[i2/x2]} etc.
 
@@ -702,7 +701,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
    need also to construct a default value for the other branches of
    the destructor. As default value, we take a tuple of the form
 
-    [existS [xn]Pn ?n (... existS [x2]P2 ?2 (existS [x1]P1 ?1 term))]
+    [existT [xn]Pn ?n (... existT [x2]P2 ?2 (existT [x1]P1 ?1 term))]
 
    but for this we have to solve the following unification problem:
 
@@ -917,7 +916,7 @@ let bareRevSubstInConcl lbeq body (t,e1,e2) gls =
 
    Given that dep_pair looks like:
 
-   (existS e1 (existS e2 ... (existS en en+1) ... ))
+   (existT e1 (existT e2 ... (existT en en+1) ... ))
 
    and B might contain instances of the ei, we will return the term:
 
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index e35623b522..302d9a9926 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -279,7 +279,6 @@ let dest_nf_eq gls eqn =
 
 (* Patterns "(existS ?1 ?2 ?3 ?4)" and "(existT ?1 ?2 ?3 ?4)" *)
 let coq_ex_pattern_gen ex = lazy PATTERN [ %ex ?X1 ?X2 ?X3 ?X4 ]
-let coq_existS_pattern = coq_ex_pattern_gen coq_existS_ref
 let coq_existT_pattern = coq_ex_pattern_gen coq_existT_ref
 
 let match_sigma ex ex_pat =
@@ -292,8 +291,7 @@ let match_sigma ex ex_pat =
 
 let find_sigma_data_decompose ex = (* fails with PatternMatchingFailure *)
   first_match (match_sigma ex) 
-    [coq_existS_pattern, build_sigma_set; 
-     coq_existT_pattern, build_sigma_type]
+    [coq_existT_pattern, build_sigma_type]
 
 (* Pattern "(sig ?1 ?2)" *)
 let coq_sig_pattern = lazy PATTERN [ %coq_sig_ref ?X1 ?X2 ]
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 67040c15dc..6dde098cff 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -101,7 +101,7 @@ open Coqlib
 val find_eq_data_decompose : constr -> 
   coq_leibniz_eq_data * (constr * constr * constr)
 
-(* Match a term of the form [(existS A P t p)] or [(existT A P t p)] *)
+(* Match a term of the form [(existT A P t p)] *)
 (* Returns associated lemmas and [A,P,t,p] *)
 val find_sigma_data_decompose : constr -> 
   coq_sigma_data * (constr * constr * constr * constr)