Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

1 files changed, 269 insertions, 213 deletions

diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index a2b6e8b7..82f74f40 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: topconstr.ml,v 1.35.2.3 2004/11/17 09:51:41 herbelin Exp $ *)
+(* $Id: topconstr.ml 8624 2006-03-13 17:38:17Z msozeau $ *)
 
 (*i*)
 open Pp
@@ -16,6 +16,7 @@ open Nameops
 open Libnames
 open Rawterm
 open Term
+open Mod_subst
 (*i*)
 
 (**********************************************************************)
@@ -36,20 +37,19 @@ type aconstr =
   | ALambda of name * aconstr * aconstr
   | AProd of name * aconstr * aconstr
   | ALetIn of name * aconstr * aconstr
-  | ACases of aconstr option * aconstr option *
+  | ACases of aconstr option *
       (aconstr * (name * (inductive * name list) option)) list *
       (identifier list * cases_pattern list * aconstr) list
-  | AOrderedCase of case_style * aconstr option * aconstr * aconstr array
   | ALetTuple of name list * (name * aconstr option) * aconstr * aconstr
   | AIf of aconstr * (name * aconstr option) * aconstr * aconstr
   | ASort of rawsort
-  | AHole of hole_kind
+  | AHole of Evd.hole_kind
   | APatVar of patvar
-  | ACast of aconstr * aconstr
+  | ACast of aconstr * cast_kind * aconstr
   
 let name_app f e = function
-  | Name id -> let (id, e) = f id e in (Name id, e)
-  | Anonymous -> Anonymous, e
+  | Name id -> let (id, e) = f id e in (e, Name id)
+  | Anonymous -> e,Anonymous
 
 let rec subst_rawvars l = function
   | RVar (_,id) as r -> (try List.assoc id l with Not_found -> r)
@@ -67,40 +67,44 @@ let rawconstr_of_aconstr_with_binders loc g f e = function
       let outerl = (ldots_var,inner)::(if swap then [x,RVar(loc,y)] else []) in
       subst_rawvars outerl it
   | ALambda (na,ty,c) ->
-      let na,e = name_app g e na in RLambda (loc,na,f e ty,f e c)
+      let e,na = name_app g e na in RLambda (loc,na,f e ty,f e c)
   | AProd (na,ty,c) ->
-      let na,e = name_app g e na in RProd (loc,na,f e ty,f e c)
+      let e,na = name_app g e na in RProd (loc,na,f e ty,f e c)
   | ALetIn (na,b,c) ->
-      let na,e = name_app g e na in RLetIn (loc,na,f e b,f e c)
-  | ACases (tyopt,rtntypopt,tml,eqnl) ->
-      let cases_predicate_names tml =
-	List.flatten (List.map (function
-	  | (tm,(na,None)) -> [na]
-	  | (tm,(na,Some (_,nal))) -> na::nal) tml) in
-      (* TODO: apply g to na (in fact not used) *)
-      let e' = List.fold_right
-	(fun na e -> snd (name_app g e na)) (cases_predicate_names tml) e in
+      let e,na = name_app g e na in RLetIn (loc,na,f e b,f e c)
+  | ACases (rtntypopt,tml,eqnl) ->
+      let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') ->
+	let e',t' = match t with
+	| None -> e',None
+	| Some (ind,nal) -> 
+	  let e',nal' = List.fold_right (fun na (e',nal) -> 
+	      let e',na' = name_app g e' na in e',na'::nal) nal (e',[]) in
+	  e',Some (loc,ind,nal') in
+	let e',na' = name_app g e' na in
+	(e',(f e tm,(na',t'))::tml')) tml (e,[]) in
       let fold id (idl,e) = let (id,e) = g id e in (id::idl,e) in
-      let eqnl = List.map (fun (idl,pat,rhs) ->
-        let (idl,e) = List.fold_right fold idl ([],e) in (loc,idl,pat,f e rhs)) eqnl in
-      RCases (loc,(option_app (f e) tyopt, ref (option_app (f e') rtntypopt)),
-        List.map (fun (tm,(na,x)) -> 
-	  (f e tm,ref (na,option_app (fun (x,y) -> (loc,x,y)) x))) tml,eqnl)
-  | AOrderedCase (b,tyopt,tm,bv) ->
-      ROrderedCase (loc,b,option_app (f e) tyopt,f e tm,Array.map (f e) bv,ref None)
+      let eqnl' = List.map (fun (idl,pat,rhs) ->
+        let (idl,e) = List.fold_right fold idl ([],e) in
+	(loc,idl,pat,f e rhs)) eqnl in
+      RCases (loc,option_app (f e') rtntypopt,tml',eqnl')
   | ALetTuple (nal,(na,po),b,c) ->
-      let e,nal = list_fold_map (fun e na -> let (na,e) = name_app g e na in e,na) e nal in 
-      let na,e = name_app g e na in
+      let e,nal = list_fold_map (name_app g) e nal in 
+      let e,na = name_app g e na in
       RLetTuple (loc,nal,(na,option_app (f e) po),f e b,f e c)
   | AIf (c,(na,po),b1,b2) ->
-      let na,e = name_app g e na in
+      let e,na = name_app g e na in
       RIf (loc,f e c,(na,option_app (f e) po),f e b1,f e b2)
-  | ACast (c,t) -> RCast (loc,f e c,f e t)
+  | ACast (c,k,t) -> RCast (loc,f e c,k,f e t)
   | ASort x -> RSort (loc,x)
   | AHole x  -> RHole (loc,x)
   | APatVar n -> RPatVar (loc,(false,n))
   | ARef x -> RRef (loc,x)
 
+let rec rawconstr_of_aconstr loc x =
+  let rec aux () x = 
+    rawconstr_of_aconstr_with_binders loc (fun id () -> (id,())) aux () x
+  in aux () x
+
 let rec subst_pat subst pat = 
   match pat with
   | PatVar _ -> pat
@@ -110,100 +114,6 @@ let rec subst_pat subst pat =
         if kn' == kn && cpl' == cpl then pat else
           PatCstr (loc,((kn',i),j),cpl',n)
 
-let rec subst_aconstr subst raw =
-  match raw with
-  | ARef ref -> 
-      let ref' = subst_global subst ref in 
-	if ref' == ref then raw else
-	  ARef ref'
-
-  | AVar _ -> raw
-
-  | AApp (r,rl) -> 
-      let r' = subst_aconstr subst r 
-      and rl' = list_smartmap (subst_aconstr subst) rl in
-	if r' == r && rl' == rl then raw else
-	  AApp(r',rl')
-
-  | AList (id1,id2,r1,r2,b) -> 
-      let r1' = subst_aconstr subst r1 and r2' = subst_aconstr subst r2 in
-	if r1' == r1 && r2' == r2 then raw else
-	  AList (id1,id2,r1',r2',b)
-
-  | ALambda (n,r1,r2) -> 
-      let r1' = subst_aconstr subst r1 and r2' = subst_aconstr subst r2 in
-	if r1' == r1 && r2' == r2 then raw else
-	  ALambda (n,r1',r2')
-
-  | AProd (n,r1,r2) -> 
-      let r1' = subst_aconstr subst r1 and r2' = subst_aconstr subst r2 in
-	if r1' == r1 && r2' == r2 then raw else
-	  AProd (n,r1',r2')
-
-  | ALetIn (n,r1,r2) -> 
-      let r1' = subst_aconstr subst r1 and r2' = subst_aconstr subst r2 in
-	if r1' == r1 && r2' == r2 then raw else
-	  ALetIn (n,r1',r2')
-
-  | ACases (ro,rtntypopt,rl,branches) -> 
-      let ro' = option_smartmap (subst_aconstr subst) ro 
-      and rtntypopt' = option_smartmap (subst_aconstr subst) rtntypopt
-      and rl' = list_smartmap
-        (fun (a,(n,signopt) as x) -> 
-	  let a' = subst_aconstr subst a in
-	  let signopt' = option_app (fun ((indkn,i),nal as z) ->
-	    let indkn' = subst_kn subst indkn in
-	    if indkn == indkn' then z else ((indkn',i),nal)) signopt in
-	  if a' == a && signopt' == signopt then x else (a',(n,signopt')))
-        rl
-      and branches' = list_smartmap 
-                        (fun (idl,cpl,r as branch) ->
-                           let cpl' = list_smartmap (subst_pat subst) cpl
-                           and r' = subst_aconstr subst r in
-                             if cpl' == cpl && r' == r then branch else
-                               (idl,cpl',r'))
-                        branches
-      in
-        if ro' == ro && rtntypopt == rtntypopt' &
-          rl' == rl && branches' == branches then raw else
-          ACases (ro',rtntypopt',rl',branches')
-
-  | AOrderedCase (b,ro,r,ra) -> 
-      let ro' = option_smartmap (subst_aconstr subst) ro
-      and r' = subst_aconstr subst r 
-      and ra' = array_smartmap (subst_aconstr subst) ra in
-	if ro' == ro && r' == r && ra' == ra then raw else
-	  AOrderedCase (b,ro',r',ra')
-
-  | ALetTuple (nal,(na,po),b,c) ->
-      let po' = option_smartmap (subst_aconstr subst) po
-      and b' = subst_aconstr subst b 
-      and c' = subst_aconstr subst c in
-	if po' == po && b' == b && c' == c then raw else
-	  ALetTuple (nal,(na,po'),b',c')
-
-  | AIf (c,(na,po),b1,b2) ->
-      let po' = option_smartmap (subst_aconstr subst) po
-      and b1' = subst_aconstr subst b1
-      and b2' = subst_aconstr subst b2 
-      and c' = subst_aconstr subst c in
-	if po' == po && b1' == b1 && b2' == b2 && c' == c then raw else
-	  AIf (c',(na,po'),b1',b2')
-
-  | APatVar _ | ASort _ -> raw
-
-  | AHole (ImplicitArg (ref,i)) ->
-      let ref' = subst_global subst ref in 
-	if ref' == ref then raw else
-	  AHole (ImplicitArg (ref',i))
-  | AHole (BinderType _ | QuestionMark | CasesType |
-      InternalHole | TomatchTypeParameter _) -> raw
-
-  | ACast (r1,r2) -> 
-      let r1' = subst_aconstr subst r1 and r2' = subst_aconstr subst r2 in
-	if r1' == r1 && r2' == r2 then raw else
-	  ACast (r1',r2')
-
 let add_name r = function
   | Anonymous -> ()
   | Name id -> r := id :: !r
@@ -222,9 +132,9 @@ let compare_rawconstr f t1 t2 = match t1,t2 with
       f ty1 ty2 & f c1 c2
   | RHole _, RHole _ -> true
   | RSort (_,s1), RSort (_,s2) -> s1 = s2
-  | (RLetIn _ | RCases _ | ROrderedCase _ | RRec _ | RDynamic _
+  | (RLetIn _ | RCases _ | RRec _ | RDynamic _
     | RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _),_
-  | _,(RLetIn _ | RCases _ | ROrderedCase _ | RRec _ | RDynamic _
+  | _,(RLetIn _ | RCases _ | RRec _ | RDynamic _
       | RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _)
       -> error "Unsupported construction in recursive notations"
   | (RRef _ | RVar _ | RApp _ | RLambda _ | RProd _ | RHole _ | RSort _), _
@@ -232,7 +142,7 @@ let compare_rawconstr f t1 t2 = match t1,t2 with
 
 let rec eq_rawconstr t1 t2 = compare_rawconstr eq_rawconstr t1 t2
 
-let discriminate_patterns nl l1 l2 =
+let discriminate_patterns foundvars nl l1 l2 =
   let diff = ref None in
   let rec aux n c1 c2 = match c1,c2 with
   | RVar (_,v1), RVar (_,v2) when v1<>v2 ->
@@ -245,42 +155,48 @@ let discriminate_patterns nl l1 l2 =
   let l = list_map2_i aux 0 l1 l2 in
   if not (List.for_all ((=) true) l) then
     error "Both ends of the recursive pattern differ";
-  !diff
+  match !diff with
+    | None ->  error "Both ends of the recursive pattern are the same"
+    | Some (x,y,_ as discr) ->
+	List.iter (fun id ->
+          if List.mem id !foundvars
+          then error "Variables used in the recursive part of a pattern are not allowed to occur outside of the recursive part";
+          foundvars := id::!foundvars) [x;y];
+	discr
 
 let aconstr_and_vars_of_rawconstr a =
   let found = ref [] in
-  let bound_binders = ref [] in
   let rec aux = function
-  | RVar (_,id) -> 
-      if not (List.mem id !bound_binders) then found := id::!found;
-      AVar id
+  | RVar (_,id) -> found := id::!found; AVar id
   | RApp (_,f,args) when has_ldots args -> make_aconstr_list f args 
+  | RApp (_,RVar (_,f),[RApp (_,t,[c]);d]) when f = ldots_var ->
+      (* Special case for alternative (recursive) notation of application *)
+      let x,y,lassoc = discriminate_patterns found 0 [c] [d] in
+      found := ldots_var :: !found; assert lassoc;
+      AList (x,y,AApp (AVar ldots_var,[AVar x]),aux t,lassoc)
   | RApp (_,g,args) -> AApp (aux g, List.map aux args)
-  | RLambda (_,na,ty,c) -> add_name bound_binders na; ALambda (na,aux ty,aux c)
-  | RProd (_,na,ty,c) -> add_name bound_binders na; AProd (na,aux ty,aux c)
-  | RLetIn (_,na,b,c) -> add_name bound_binders na; ALetIn (na,aux b,aux c)
-  | RCases (_,(tyopt,rtntypopt),tml,eqnl) ->
+  | RLambda (_,na,ty,c) -> add_name found na; ALambda (na,aux ty,aux c)
+  | RProd (_,na,ty,c) -> add_name found na; AProd (na,aux ty,aux c)
+  | RLetIn (_,na,b,c) -> add_name found na; ALetIn (na,aux b,aux c)
+  | RCases (_,rtntypopt,tml,eqnl) ->
       let f (_,idl,pat,rhs) =
-        bound_binders := idl@(!bound_binders);
+        found := idl@(!found);
         (idl,pat,aux rhs) in
-      ACases (option_app aux tyopt,
-        option_app aux !rtntypopt,
-        List.map (fun (tm,{contents = (na,x)}) ->
-	  add_name bound_binders na;
+      ACases (option_app aux rtntypopt,
+        List.map (fun (tm,(na,x)) ->
+	  add_name found na;
 	  option_iter
-	    (fun (_,_,nl) -> List.iter (add_name bound_binders) nl) x;
+	    (fun (_,_,nl) -> List.iter (add_name found) nl) x;
           (aux tm,(na,option_app (fun (_,ind,nal) -> (ind,nal)) x))) tml,
         List.map f eqnl)
-  | ROrderedCase (_,b,tyopt,tm,bv,_) ->
-      AOrderedCase (b,option_app aux tyopt,aux tm, Array.map aux bv)
   | RLetTuple (loc,nal,(na,po),b,c) ->
-      add_name bound_binders na;
-      List.iter (add_name bound_binders) nal;
+      add_name found na;
+      List.iter (add_name found) nal;
       ALetTuple (nal,(na,option_app aux po),aux b,aux c)
   | RIf (loc,c,(na,po),b1,b2) ->
-      add_name bound_binders na;
+      add_name found na;
       AIf (aux c,(na,option_app aux po),aux b1,aux b2)
-  | RCast (_,c,t) -> ACast (aux c,aux t)
+  | RCast (_,c,k,t) -> ACast (aux c,k,aux t)
   | RSort (_,s) -> ASort s
   | RHole (_,w) -> AHole w
   | RRef (_,r) -> ARef r
@@ -300,13 +216,7 @@ allowed in abbreviatable expressions"
 	error "Both ends of the recursive pattern have different lengths";
       let ll2,l2' = list_chop nl l2 in
       let t = List.hd l2' and lr2 = List.tl l2' in
-      let discr = discriminate_patterns nl (ll1@lr1) (ll2@lr2) in
-      let x,y,order = match discr with Some z -> z | None -> 
-	error "Both ends of the recursive pattern are the same" in
-      List.iter (fun id ->
-        if List.mem id !bound_binders or List.mem id !found 
-        then error "Variables used in the recursive part of a pattern are not allowed to occur outside of the recursive part";
-        found := id::!found) [x;y];
+      let x,y,order = discriminate_patterns found nl (ll1@lr1) (ll2@lr2) in
       let iter =
         if order then RApp (loc,f2,ll2@RVar (loc,ldots_var)::lr2)
         else RApp (loc,f1,ll1@RVar (loc,ldots_var)::lr1) in
@@ -326,20 +236,126 @@ allowed in abbreviatable expressions"
   in
   let t = aux a in
   (* Side effect *)
-  t, !found, !bound_binders
+  t, !found
 
 let aconstr_of_rawconstr vars a =
-  let a,notbindingvars,binders = aconstr_and_vars_of_rawconstr a in
+  let a,foundvars = aconstr_and_vars_of_rawconstr a in
   let check_type x =
-    if not (List.mem x notbindingvars or List.mem x binders) then
+    if not (List.mem x foundvars) then
       error ((string_of_id x)^" is unbound in the right-hand-side") in
   List.iter check_type vars;
   a
 
+let aconstr_of_constr avoiding t =
+ aconstr_of_rawconstr [] (Detyping.detype false avoiding [] t)
+
+let rec subst_aconstr subst bound raw =
+  match raw with
+  | ARef ref -> 
+      let ref',t = subst_global subst ref in 
+	if ref' == ref then raw else
+	  aconstr_of_constr bound t
+
+  | AVar _ -> raw
+
+  | AApp (r,rl) -> 
+      let r' = subst_aconstr subst bound r 
+      and rl' = list_smartmap (subst_aconstr subst bound) rl in
+	if r' == r && rl' == rl then raw else
+	  AApp(r',rl')
+
+  | AList (id1,id2,r1,r2,b) -> 
+      let r1' = subst_aconstr subst bound r1 and r2' = subst_aconstr subst bound r2 in
+	if r1' == r1 && r2' == r2 then raw else
+	  AList (id1,id2,r1',r2',b)
+
+  | ALambda (n,r1,r2) -> 
+      let r1' = subst_aconstr subst bound r1 and r2' = subst_aconstr subst bound r2 in
+	if r1' == r1 && r2' == r2 then raw else
+	  ALambda (n,r1',r2')
+
+  | AProd (n,r1,r2) -> 
+      let r1' = subst_aconstr subst bound r1 and r2' = subst_aconstr subst bound r2 in
+	if r1' == r1 && r2' == r2 then raw else
+	  AProd (n,r1',r2')
+
+  | ALetIn (n,r1,r2) -> 
+      let r1' = subst_aconstr subst bound r1 and r2' = subst_aconstr subst bound r2 in
+	if r1' == r1 && r2' == r2 then raw else
+	  ALetIn (n,r1',r2')
+
+  | ACases (rtntypopt,rl,branches) -> 
+      let rtntypopt' = option_smartmap (subst_aconstr subst bound) rtntypopt
+      and rl' = list_smartmap
+        (fun (a,(n,signopt) as x) -> 
+	  let a' = subst_aconstr subst bound a in
+	  let signopt' = option_app (fun ((indkn,i),nal as z) ->
+	    let indkn' = subst_kn subst indkn in
+	    if indkn == indkn' then z else ((indkn',i),nal)) signopt in
+	  if a' == a && signopt' == signopt then x else (a',(n,signopt')))
+        rl
+      and branches' = list_smartmap 
+                        (fun (idl,cpl,r as branch) ->
+                           let cpl' = list_smartmap (subst_pat subst) cpl
+                           and r' = subst_aconstr subst bound r in
+                             if cpl' == cpl && r' == r then branch else
+                               (idl,cpl',r'))
+                        branches
+      in
+        if rtntypopt' == rtntypopt && rtntypopt == rtntypopt' &
+          rl' == rl && branches' == branches then raw else
+          ACases (rtntypopt',rl',branches')
+
+  | ALetTuple (nal,(na,po),b,c) ->
+      let po' = option_smartmap (subst_aconstr subst bound) po
+      and b' = subst_aconstr subst bound b 
+      and c' = subst_aconstr subst bound c in
+	if po' == po && b' == b && c' == c then raw else
+	  ALetTuple (nal,(na,po'),b',c')
+
+  | AIf (c,(na,po),b1,b2) ->
+      let po' = option_smartmap (subst_aconstr subst bound) po
+      and b1' = subst_aconstr subst bound b1
+      and b2' = subst_aconstr subst bound b2 
+      and c' = subst_aconstr subst bound c in
+	if po' == po && b1' == b1 && b2' == b2 && c' == c then raw else
+	  AIf (c',(na,po'),b1',b2')
+
+  | APatVar _ | ASort _ -> raw
+
+  | AHole (Evd.ImplicitArg (ref,i)) ->
+      let ref',t = subst_global subst ref in 
+	if ref' == ref then raw else
+	  AHole (Evd.InternalHole)
+  | AHole (Evd.BinderType _ | Evd.QuestionMark | Evd.CasesType |
+      Evd.InternalHole | Evd.TomatchTypeParameter _) -> raw
+
+  | ACast (r1,k,r2) -> 
+      let r1' = subst_aconstr subst bound r1 and r2' = subst_aconstr subst bound r2 in
+	if r1' == r1 && r2' == r2 then raw else
+	  ACast (r1',k,r2')
+
+
 let encode_list_value l = RApp (dummy_loc,RVar (dummy_loc,ldots_var),l)
 
 (* Pattern-matching rawconstr and aconstr *)
 
+let abstract_return_type_context pi mklam tml rtno =
+  option_app (fun rtn ->
+    let nal =
+      List.flatten (List.map (fun (_,(na,t)) ->
+	match t with Some x -> (pi x)@[na] | None -> [na]) tml) in
+    List.fold_right mklam nal rtn)
+    rtno
+
+let abstract_return_type_context_rawconstr =
+  abstract_return_type_context pi3
+    (fun na c -> RLambda(dummy_loc,na,RHole(dummy_loc,Evd.InternalHole),c))
+
+let abstract_return_type_context_aconstr =
+  abstract_return_type_context snd
+    (fun na c -> ALambda(na,AHole Evd.InternalHole,c))
+
 let rec adjust_scopes = function
   | _,[] -> []
   | [],a::args -> (None,a) :: adjust_scopes ([],args)
@@ -366,6 +382,18 @@ let bind_env alp sigma var v =
     (* TODO: handle the case of multiple occs in different scopes *)
     (var,v)::sigma
 
+let match_opt f sigma t1 t2 = match (t1,t2) with
+  | None, None -> sigma
+  | Some t1, Some t2 -> f sigma t1 t2
+  | _ -> raise No_match
+
+let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
+  | (Name id1,Name id2) when List.mem id2 metas ->
+      alp, bind_env alp sigma id2 (RVar (dummy_loc,id1))
+  | (Name id1,Name id2) -> (id1,id2)::alp,sigma
+  | (Anonymous,Anonymous) -> alp,sigma
+  | _ -> raise No_match
+
 let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
   | r1, AVar id2 when List.mem id2 metas -> bind_env alp sigma id2 r1
   | RVar (_,id1), AVar id2 when alpha_var id1 id2 alp -> sigma
@@ -377,28 +405,34 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
       when List.length l1 = List.length l2 ->
       match_alist alp metas sigma (f1::l1) (f2::l2) x iter termin lassoc
   | RLambda (_,na1,t1,b1), ALambda (na2,t2,b2) ->
-     match_binders alp metas (match_ alp metas sigma t1 t2) b1 b2 na1 na2
+     match_binders alp metas na1 na2 (match_ alp metas sigma t1 t2) b1 b2
   | RProd (_,na1,t1,b1), AProd (na2,t2,b2) ->
-     match_binders alp metas (match_ alp metas sigma t1 t2) b1 b2 na1 na2
+     match_binders alp metas na1 na2 (match_ alp metas sigma t1 t2) b1 b2
   | RLetIn (_,na1,t1,b1), ALetIn (na2,t2,b2) ->
-     match_binders alp metas (match_ alp metas sigma t1 t2) b1 b2 na1 na2
-  | RCases (_,(po1,rtno1),tml1,eqnl1), ACases (po2,rtno2,tml2,eqnl2) 
+     match_binders alp metas na1 na2 (match_ alp metas sigma t1 t2) b1 b2
+  | RCases (_,rtno1,tml1,eqnl1), ACases (rtno2,tml2,eqnl2) 
       when List.length tml1 = List.length tml2 ->
-     let sigma = option_fold_left2 (match_ alp metas) sigma po1 po2 in
-     (* TODO: match rtno' with their contexts *)
-     let sigma = List.fold_left2 
+      let rtno1' = abstract_return_type_context_rawconstr tml1 rtno1 in
+      let rtno2' = abstract_return_type_context_aconstr tml2 rtno2 in
+      let sigma = option_fold_left2 (match_ alp metas) sigma rtno1' rtno2' in
+      let sigma = List.fold_left2 
        (fun s (tm1,_) (tm2,_) -> match_ alp metas s tm1 tm2) sigma tml1 tml2 in
-     List.fold_left2 (match_equations alp metas) sigma eqnl1 eqnl2
-  | ROrderedCase (_,st,po1,c1,bl1,_), AOrderedCase (st2,po2,c2,bl2) 
-      when Array.length bl1 = Array.length bl2 ->
-     let sigma = option_fold_left2 (match_ alp metas) sigma po1 po2 in
-     array_fold_left2 (match_ alp metas) (match_ alp metas sigma c1 c2) bl1 bl2
-  | RCast(_,c1,t1), ACast(c2,t2) ->
+      List.fold_left2 (match_equations alp metas) sigma eqnl1 eqnl2
+  | RIf (_,a1,(na1,to1),b1,c1), AIf (a2,(na2,to2),b2,c2) ->
+      let sigma = match_opt (match_binders alp metas na1 na2) sigma to1 to2 in
+      List.fold_left2 (match_ alp metas) sigma [a1;b1;c1] [a2;b2;c2]
+  | RLetTuple (_,nal1,(na1,to1),b1,c1), ALetTuple (nal2,(na2,to2),b2,c2) 
+      when List.length nal1 = List.length nal2 ->
+      let sigma = match_opt (match_binders alp metas na1 na2) sigma to1 to2 in
+      let sigma = match_ alp metas sigma b1 b2 in
+      let (alp,sigma) =
+	List.fold_left2 (match_names metas) (alp,sigma) nal1 nal2 in
+      match_ alp metas sigma c1 c2
+  | RCast(_,c1,_,t1), ACast(c2,_,t2) ->
       match_ alp metas (match_ alp metas sigma c1 c2) t1 t2
   | RSort (_,s1), ASort s2 when s1 = s2 -> sigma
   | RPatVar _, AHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match
-  | a, AHole _ when not(Options.do_translate()) -> sigma
-  | RHole _, AHole _ -> sigma
+  | a, AHole _ -> sigma
   | (RDynamic _ | RRec _ | REvar _), _ 
   | _,_ -> raise No_match
 
@@ -423,13 +457,9 @@ and match_alist alp metas sigma l1 l2 x iter termin lassoc =
   let tl,sigma = match_alist_tail alp metas sigma [t1] rest in
   (x,encode_list_value (if lassoc then List.rev tl else tl))::sigma
 
-and match_binders alp metas sigma b1 b2 na1 na2 = match (na1,na2) with
-  | (Name id1,Name id2) when List.mem id2 metas ->
-      let sigma = bind_env alp sigma id2 (RVar (dummy_loc,id1)) in 
-      match_ alp metas sigma b1 b2
-  | (Name id1,Name id2) -> match_ ((id1,id2)::alp) metas sigma b1 b2
-  | (Anonymous,Anonymous) -> match_  alp metas sigma b1 b2
-  | _ -> raise No_match
+and match_binders alp metas na1 na2 sigma b1 b2 =
+  let (alp,sigma) = match_names metas (alp,sigma) na1 na2 in
+  match_ alp metas sigma b1 b2
 
 and match_equations alp metas sigma (_,idl1,pat1,rhs1) (idl2,pat2,rhs2) =
   if idl1 = idl2 & pat1 = pat2 (* Useful to reason up to alpha ?? *) then
@@ -461,12 +491,15 @@ type explicitation = ExplByPos of int | ExplByName of identifier
 
 type proj_flag = int option (* [Some n] = proj of the n-th visible argument *)
 
+type prim_token = Numeral of Bigint.bigint | String of string
+
 type cases_pattern_expr =
   | CPatAlias of loc * cases_pattern_expr * identifier
   | CPatCstr of loc * reference * cases_pattern_expr list
   | CPatAtom of loc * reference option
+  | CPatOr of loc * cases_pattern_expr list
   | CPatNotation of loc * notation * cases_pattern_expr list
-  | CPatNumeral of loc * Bignat.bigint
+  | CPatPrim of loc * prim_token
   | CPatDelimiters of loc * string * cases_pattern_expr
 
 type constr_expr =
@@ -480,11 +513,9 @@ type constr_expr =
   | CAppExpl of loc * (proj_flag * reference) * constr_expr list
   | CApp of loc * (proj_flag * constr_expr) * 
       (constr_expr * explicitation located option) list
-  | CCases of loc * (constr_expr option * constr_expr option) *
+  | CCases of loc * constr_expr option *
       (constr_expr * (name option * constr_expr option)) list *
       (loc * cases_pattern_expr list * constr_expr) list
-  | COrderedCase of loc * case_style * constr_expr option * constr_expr
-      * constr_expr list
   | CLetTuple of loc * name list * (name option * constr_expr option) *
       constr_expr * constr_expr
   | CIf of loc * constr_expr * (name option * constr_expr option)
@@ -493,14 +524,15 @@ type constr_expr =
   | CPatVar of loc * (bool * patvar)
   | CEvar of loc * existential_key
   | CSort of loc * rawsort
-  | CCast of loc * constr_expr * constr_expr
+  | CCast of loc * constr_expr * cast_kind * constr_expr
   | CNotation of loc * notation * constr_expr list
-  | CNumeral of loc * Bignat.bigint
+  | CPrim of loc * prim_token
   | CDelimiters of loc * string * constr_expr
   | CDynamic of loc * Dyn.t
 
+
 and fixpoint_expr =
-    identifier * int * local_binder list * constr_expr * constr_expr
+    identifier * (int * recursion_order_expr) * local_binder list * constr_expr * constr_expr
 
 and local_binder =
   | LocalRawDef of name located * constr_expr
@@ -509,6 +541,10 @@ and local_binder =
 and cofixpoint_expr =
     identifier * local_binder list * constr_expr * constr_expr
 
+and recursion_order_expr = 
+  | CStructRec
+  | CWfRec of constr_expr
+
 (***********************)
 (* For binders parsing *)
 
@@ -520,6 +556,9 @@ let rec local_binders_length = function
 let names_of_local_assums bl =
   List.flatten (List.map (function LocalRawAssum(l,_)->l|_->[]) bl)
 
+let names_of_local_binders bl =
+  List.flatten (List.map (function LocalRawAssum(l,_)->l|LocalRawDef(l,_)->[l]) bl)
+
 (**********************************************************************)
 (* Functions on constr_expr *)
 
@@ -535,16 +574,15 @@ let constr_loc = function
   | CAppExpl (loc,_,_) -> loc
   | CApp (loc,_,_) -> loc
   | CCases (loc,_,_,_) -> loc
-  | COrderedCase (loc,_,_,_,_) -> loc
   | CLetTuple (loc,_,_,_,_) -> loc
   | CIf (loc,_,_,_,_) -> loc
   | CHole loc -> loc
   | CPatVar (loc,_) -> loc
   | CEvar (loc,_) -> loc
   | CSort (loc,_) -> loc
-  | CCast (loc,_,_) -> loc
+  | CCast (loc,_,_,_) -> loc
   | CNotation (loc,_,_) -> loc
-  | CNumeral (loc,_) -> loc
+  | CPrim (loc,_) -> loc
   | CDelimiters (loc,_,_) -> loc
   | CDynamic _ -> dummy_loc
 
@@ -552,8 +590,9 @@ let cases_pattern_loc = function
   | CPatAlias (loc,_,_) -> loc
   | CPatCstr (loc,_,_) -> loc
   | CPatAtom (loc,_) -> loc
+  | CPatOr (loc,_) -> loc
   | CPatNotation (loc,_,_) -> loc
-  | CPatNumeral (loc,_) -> loc
+  | CPatPrim (loc,_) -> loc
   | CPatDelimiters (loc,_,_) -> loc
 
 let occur_var_constr_ref id = function
@@ -571,12 +610,12 @@ let rec occur_var_constr_expr id = function
   | CProdN (_,l,b) -> occur_var_binders id b l
   | CLambdaN (_,l,b) -> occur_var_binders id b l
   | CLetIn (_,na,a,b) -> occur_var_binders id b [[na],a]
-  | CCast (loc,a,b) -> occur_var_constr_expr id a or occur_var_constr_expr id b
+  | CCast (loc,a,_,b) -> 
+    occur_var_constr_expr id a or occur_var_constr_expr id b
   | CNotation (_,_,l) -> List.exists (occur_var_constr_expr id) l
   | CDelimiters (loc,_,a) -> occur_var_constr_expr id a
-  | CHole _ | CEvar _ | CPatVar _ | CSort _ | CNumeral _ | CDynamic _ -> false
+  | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CDynamic _ -> false
   | CCases (loc,_,_,_) 
-  | COrderedCase (loc,_,_,_,_) 
   | CLetTuple (loc,_,_,_,_) 
   | CIf (loc,_,_,_,_) 
   | CFix (loc,_,_) 
@@ -593,26 +632,45 @@ and occur_var_binders id b = function
 let mkIdentC id  = CRef (Ident (dummy_loc, id))
 let mkRefC r     = CRef r
 let mkAppC (f,l) = CApp (dummy_loc, (None,f), List.map (fun x -> (x,None)) l)
-let mkCastC (a,b)  = CCast (dummy_loc,a,b)
+let mkCastC (a,k,b)  = CCast (dummy_loc,a,k,b)
 let mkLambdaC (idl,a,b) = CLambdaN (dummy_loc,[idl,a],b)
 let mkLetInC (id,a,b)   = CLetIn (dummy_loc,id,a,b)
 let mkProdC (idl,a,b)   = CProdN (dummy_loc,[idl,a],b)
 
+let rec abstract_constr_expr c = function
+  | [] -> c
+  | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_constr_expr c bl)
+  | LocalRawAssum (idl,t)::bl ->
+      List.fold_right (fun x b -> mkLambdaC([x],t,b)) idl
+      (abstract_constr_expr c bl)
+      
+let rec prod_constr_expr c = function
+  | [] -> c
+  | LocalRawDef (x,b)::bl -> mkLetInC(x,b,prod_constr_expr c bl)
+  | LocalRawAssum (idl,t)::bl ->
+      List.fold_right (fun x b -> mkProdC([x],t,b)) idl
+      (prod_constr_expr c bl)
+
+let coerce_to_id = function
+  | CRef (Ident (loc,id)) -> (loc,id)
+  | a -> user_err_loc
+        (constr_loc a,"coerce_to_id",
+         str "This expression should be a simple identifier")
+
 (* Used in correctness and interface *)
 
 
 let names_of_cases_indtype =
-  let rec vars_of ids t =
-    match t with
-      (* We deal only with the regular cases *)
-      | CApp (_,_,l) -> List.fold_left (fun ids (a,_) -> vars_of ids a) [] l
-      | CRef (Ident (_,id)) -> id::ids
-      | CNotation (_,_,l)
-      (* assume the ntn is applicative and does not instantiate the head !! *)
-      | CAppExpl (_,_,l) -> List.fold_left vars_of [] l
-      | CDelimiters(_,_,c) -> vars_of ids c
-      | _ -> ids in
-  vars_of []
+  let add_var ids = function CRef (Ident (_,id)) -> id::ids | _ -> ids in
+  let rec vars_of = function
+    (* We deal only with the regular cases *)
+    | CApp (_,_,l) -> List.fold_left add_var [] (List.map fst l)
+    | CNotation (_,_,l)
+    (* assume the ntn is applicative and does not instantiate the head !! *)
+    | CAppExpl (_,_,l) -> List.fold_left add_var [] l
+    | CDelimiters(_,_,c) -> vars_of c
+    | _ -> [] in
+  vars_of
 
 let map_binder g e nal = List.fold_right (fun (_,na) -> name_fold g na) nal e
 
@@ -642,12 +700,12 @@ let map_constr_expr_with_binders f g e = function
   | CLambdaN (loc,bl,b) ->
       let (e,bl) = map_binders f g e bl in CLambdaN (loc,bl,f e b)
   | CLetIn (loc,na,a,b) -> CLetIn (loc,na,f e a,f (name_fold g (snd na) e) b)
-  | CCast (loc,a,b) -> CCast (loc,f e a,f e b)
+  | CCast (loc,a,k,b) -> CCast (loc,f e a,k,f e b)
   | CNotation (loc,n,l) -> CNotation (loc,n,List.map (f e) l)
   | CDelimiters (loc,s,a) -> CDelimiters (loc,s,f e a)
   | CHole _ | CEvar _ | CPatVar _ | CSort _ 
-  | CNumeral _ | CDynamic _ | CRef _ as x -> x
-  | CCases (loc,(po,rtnpo),a,bl) ->
+  | CPrim _ | CDynamic _ | CRef _ as x -> x
+  | CCases (loc,rtnpo,a,bl) ->
       (* TODO: apply g on the binding variables in pat... *)
       let bl = List.map (fun (loc,pat,rhs) -> (loc,pat,f e rhs)) bl in
       let e' = 
@@ -660,10 +718,8 @@ let map_constr_expr_with_binders f g e = function
             indnal (option_fold_right (name_fold g) na e))
 	  a e
       in
-      CCases (loc,(option_app (f e) po, option_app (f e') rtnpo),
+      CCases (loc,option_app (f e') rtnpo,
          List.map (fun (tm,x) -> (f e tm,x)) a,bl)
-  | COrderedCase (loc,s,po,a,bl) ->
-      COrderedCase (loc,s,option_app (f e) po,f e a,List.map (f e) bl)
   | CLetTuple (loc,nal,(ona,po),b,c) ->
       let e' = List.fold_right (name_fold g) nal e in
       let e'' = option_fold_right (name_fold g) ona e in
@@ -698,8 +754,8 @@ let rec replace_vars_constr_expr l = function
 (* Concrete syntax for modules and modules types *)
 
 type with_declaration_ast = 
-  | CWith_Module of identifier located * qualid located
-  | CWith_Definition of identifier located * constr_expr
+  | CWith_Module of identifier list located * qualid located
+  | CWith_Definition of identifier list located * constr_expr
 
 type module_type_ast = 
   | CMTEident of qualid located