Réforme de l'interprétation des termes :

- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t"
- "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième
  pretty-printer dans ppconstr.ml est basé sur "constr_expr".
- Nouveau répertoire "interp" qui hérite de la partie interprétation qui
  se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml;
  constrextern.ml est l'équivalent de termast.ml pour le nouveau
  printer; topconstr.ml; contient la définition de "constr_expr";
  modintern.ml remplace astmod.ml)
- Libnames.reference tend à remplacer Libnames.qualid


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

1 files changed, 3 insertions, 3 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 4c6e5bb014..5c129efa90 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -591,10 +591,10 @@ let occur_rawconstr id =
     | RLambda (loc,na,ty,c) -> (occur ty) or ((na <> Name id) & (occur c))
     | RProd (loc,na,ty,c) -> (occur ty) or ((na <> Name id) & (occur c))
     | RLetIn (loc,na,b,c) -> (occur b) or ((na <> Name id) & (occur c))
-    | RCases (loc,prinfo,tyopt,tml,pl) ->
+    | RCases (loc,tyopt,tml,pl) ->
 	(occur_option tyopt) or (List.exists occur tml)
 	or (List.exists occur_pattern pl)
-    | ROldCase (loc,b,tyopt,tm,bv) -> 
+    | ROrderedCase (loc,b,tyopt,tm,bv) -> 
 	(occur_option tyopt) or (occur tm) or (array_exists occur bv)
     | RRec (loc,fk,idl,tyl,bv) ->
 	(array_exists occur tyl) or
@@ -1369,7 +1369,7 @@ and match_current pb ((current,typ as ct),deps) =
 	  let (pred,typ,s) =
 	    find_predicate pb.caseloc pb.env pb.isevars 
 	      pb.pred brtyps cstrs current indt in
-	  let ci = make_case_info pb.env mind None tags in
+	  let ci = make_case_info pb.env mind RegularStyle tags in
 	  let case = mkCase (ci,nf_betaiota pred,current,brvals) in
 	  let inst = List.map mkRel deps in
 	  pattern_status tags,