Imported Upstream version 8.1.pl1+dfsgupstream/8.1.pl1+dfsg

8 files changed, 96 insertions, 66 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index ffedcfff..349e8629 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: constrextern.ml 9226 2006-10-09 16:11:01Z herbelin $ *)
+(* $Id: constrextern.ml 9976 2007-07-12 11:58:30Z msozeau $ *)
 
 (*i*)
 open Pp
@@ -191,9 +191,11 @@ let rec check_same_type ty1 ty2 =
   | CHole _, CHole _ -> ()
   | CPatVar(_,i1), CPatVar(_,i2) when i1=i2 -> ()
   | CSort(_,s1), CSort(_,s2) when s1=s2 -> ()
-  | CCast(_,a1,_,b1), CCast(_,a2,_,b2) ->
+  | CCast(_,a1,CastConv (_,b1)), CCast(_,a2, CastConv(_,b2)) ->
       check_same_type a1 a2;
       check_same_type b1 b2
+  | CCast(_,a1,CastCoerce), CCast(_,a2, CastCoerce) ->
+      check_same_type a1 a2
   | CNotation(_,n1,e1), CNotation(_,n2,e2) when n1=n2 ->
       List.iter2 check_same_type e1 e2
   | CPrim(_,i1), CPrim(_,i2) when i1=i2 -> ()
@@ -283,8 +285,8 @@ let rec same_raw c d =
   | RSort(_,s1), RSort(_,s2) -> if s1<>s2 then failwith "RSort"
   | RHole _, _ -> ()
   | _, RHole _ -> ()
-  | RCast(_,c1,_,_),r2 -> same_raw c1 r2
-  | r1, RCast(_,c2,_,_) -> same_raw r1 c2
+  | RCast(_,c1,_),r2 -> same_raw c1 r2
+  | r1, RCast(_,c2,_) -> same_raw r1 c2
   | RDynamic(_,d1), RDynamic(_,d2) -> if d1<>d2 then failwith"RDynamic"
   | _ -> failwith "same_raw"
      
@@ -402,7 +404,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
   try 
     if !Options.raw_print or !print_no_symbol then raise No_match;
     let (na,sc,p) = uninterp_prim_token_cases_pattern pat in
-    match availability_of_prim_token sc scopes with
+    match availability_of_prim_token sc scopes p with
     | None -> raise No_match
     | Some key ->
       let loc = cases_pattern_loc pat in
@@ -602,7 +604,7 @@ let rec share_fix_binders n rbl ty def =
 let extern_possible_prim_token scopes r =
   try
     let (sc,n) = uninterp_prim_token r in
-    match availability_of_prim_token sc scopes with
+    match availability_of_prim_token sc scopes n with
     | None -> None
     | Some key -> Some (insert_delimiters (CPrim (loc_of_rawconstr r,n)) key)
   with No_match ->
@@ -744,8 +746,10 @@ let rec extern inctx scopes vars r =
 
   | RHole (loc,e) -> CHole loc
 
-  | RCast (loc,c,k,t) ->
-      CCast (loc,sub_extern true scopes vars c,k,extern_typ scopes vars t)
+  | RCast (loc,c, CastConv (k,t)) ->
+      CCast (loc,sub_extern true scopes vars c, CastConv (k,extern_typ scopes vars t))
+  | RCast (loc,c, CastCoerce) ->
+      CCast (loc,sub_extern true scopes vars c, CastCoerce)
 
   | RDynamic (loc,d) -> CDynamic (loc,d)
 
@@ -813,7 +817,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
 	let (t,args) = match t,n with
 	  | RApp (_,f,args), Some n when List.length args > n ->
 	      let args1, args2 = list_chop n args in
-	      RApp (dummy_loc,f,args1), args2
+	      (if n = 0 then f else RApp (dummy_loc,f,args1)), args2
 	  | _ -> t,[] in
 	(* Try matching ... *)
 	let subst = match_aconstr t pat in
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 4550518d..e1ee5486 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: constrintern.ml 9611 2007-02-07 15:51:01Z herbelin $ *)
+(* $Id: constrintern.ml 9976 2007-07-12 11:58:30Z msozeau $ *)
 
 open Pp
 open Util
@@ -384,7 +384,7 @@ let check_number_of_pattern loc n l =
   if n<>p then raise (InternalisationError (loc,BadPatternsNumber (n,p)))
 
 let check_or_pat_variables loc ids idsl =
-  if List.exists ((<>) ids) idsl then
+  if List.exists (fun ids' -> not (list_eq_set ids ids')) idsl then
     user_err_loc (loc, "", str 
     "The components of this disjunctive pattern must bind the same variables")
 
@@ -424,17 +424,17 @@ let rec subst_pat_iterator y t (subst,p) = match p with
       let pl = simple_product_of_cases_patterns l' in
       List.map (fun (subst',pl) -> subst'@subst,PatCstr (loc,id,pl,alias)) pl
 
-let subst_cases_pattern loc (ids,asubst as aliases) intern subst scopes a =
-  let rec aux aliases subst = function
+let subst_cases_pattern loc alias intern subst scopes a =
+  let rec aux alias subst = function
   | AVar id ->
       begin
 	(* subst remembers the delimiters stack in the interpretation *)
 	(* of the notations *)
 	try 
 	  let (a,(scopt,subscopes)) = List.assoc id subst in
-	  intern (subscopes@scopes) ([],[]) scopt a
+	    intern (subscopes@scopes) ([],[]) scopt a
 	with Not_found -> 
-	  if id = ldots_var then [],[[], PatVar (loc,Name id)] else
+	  if id = ldots_var then [], [[], PatVar (loc,Name id)] else
 	  anomaly ("Unbound pattern notation variable: "^(string_of_id id))
 	  (*
 	  (* Happens for local notation joint with inductive/fixpoint defs *)
@@ -444,33 +444,34 @@ let subst_cases_pattern loc (ids,asubst as aliases) intern subst scopes a =
 	  *)
       end
   | ARef (ConstructRef c) ->
-      (ids,[asubst, PatCstr (loc,c, [], alias_of aliases)])
+      ([],[[], PatCstr (loc,c, [], alias)])
   | AApp (ARef (ConstructRef (ind,_ as c)),args) ->
       let nparams = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
       let _,args = list_chop nparams args in
-      let idslpll = List.map (aux ([],[]) subst) args in
-      let ids',pll = product_of_cases_patterns ids idslpll in
+      let idslpll = List.map (aux Anonymous subst) args in
+      let ids',pll = product_of_cases_patterns [] idslpll in
       let pl' = List.map (fun (subst,pl) -> 
-        subst,PatCstr (loc,c,pl,alias_of aliases)) pll in
-      ids', pl'
+        subst,PatCstr (loc,c,pl,alias)) pll in
+	ids', pl'
   | AList (x,_,iter,terminator,lassoc) ->
       (try 
         (* All elements of the list are in scopes (scopt,subscopes) *)
 	let (a,(scopt,subscopes)) = List.assoc x subst in
-        let termin = aux ([],[]) subst terminator in
+        let termin = aux Anonymous subst terminator in
         let l = decode_patlist_value a in
         let idsl,v =
 	  List.fold_right (fun a (tids,t) -> 
-            let uids,u = aux ([],[]) ((x,(a,(scopt,subscopes)))::subst) iter in
+            let uids,u = aux Anonymous ((x,(a,(scopt,subscopes)))::subst) iter in
             let pll = List.map (subst_pat_iterator ldots_var t) u in
             tids@uids, List.flatten pll)
             (if lassoc then List.rev l else l) termin in
-        ids@idsl, v
+        idsl, List.map (fun ((subst, pl) as x) -> 
+	  match pl with PatCstr (loc, c, pl, Anonymous) -> (subst, PatCstr (loc, c, pl, alias)) | _ -> x) v
       with Not_found -> 
           anomaly "Inconsistent substitution of recursive notation")
   | t -> user_err_loc (loc,"",str "Invalid notation for pattern")
-  in aux aliases subst a
-
+  in aux alias subst a
+    
 (* Differentiating between constructors and matching variables *)
 type pattern_qualid_kind =
   | ConstrPat of (constructor * cases_pattern list)
@@ -565,11 +566,12 @@ let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope =
       intern_cases_pattern genv scopes aliases tmp_scope a
   | CPatNotation (loc, ntn, args) ->
       let ntn,args = contract_pat_notation ntn args in
-      let ((ids,c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in
+      let ((ids',c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in
       if !dump then dump_notation_location (patntn_loc loc args ntn) df;
-      let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in
-      subst_cases_pattern loc aliases (intern_cases_pattern genv) subst scopes 
+      let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids' args in
+      let ids'',pl = subst_cases_pattern loc (alias_of aliases) (intern_cases_pattern genv) subst scopes 
 	c
+      in ids@ids'', pl
   | CPatPrim (loc, p) ->
       let a = alias_of aliases in
       let (c,df) = Notation.interp_prim_token_cases_pattern loc p a 
@@ -915,7 +917,7 @@ let internalise sigma globalenv env allow_soapp lvar c =
         let p' = option_map (intern_type env'') po in
         RIf (loc, c', (na', p'), intern env b1, intern env b2)
     | CHole loc -> 
-	RHole (loc, Evd.QuestionMark)
+	RHole (loc, Evd.QuestionMark true)
     | CPatVar (loc, n) when allow_soapp ->
 	RPatVar (loc, n)
     | CPatVar (loc, (false,n)) ->
@@ -926,8 +928,10 @@ let internalise sigma globalenv env allow_soapp lvar c =
 	REvar (loc, n, None)
     | CSort (loc, s) ->
 	RSort(loc,s)
-    | CCast (loc, c1, k, c2) ->
-	RCast (loc,intern env c1,k,intern_type env c2)
+    | CCast (loc, c1, CastConv (k, c2)) ->
+	RCast (loc,intern env c1, CastConv (k, intern_type env c2))
+    | CCast (loc, c1, CastCoerce) ->
+	RCast (loc,intern env c1, CastCoerce)
 
     | CDynamic (loc,d) -> RDynamic (loc,d)
 
@@ -1087,6 +1091,8 @@ let intern_gen isarity sigma env
 
 let intern_constr sigma env c = intern_gen false sigma env c 
 
+let intern_type sigma env c = intern_gen true sigma env c 
+
 let intern_pattern env patt =
   try
     intern_cases_pattern env [] ([],[]) None patt 
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index d88a058d..4479fcd4 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: constrintern.mli 9154 2006-09-20 17:18:18Z corbinea $ i*)
+(*i $Id: constrintern.mli 9976 2007-07-12 11:58:30Z msozeau $ i*)
 
 (*i*)
 open Names
@@ -51,6 +51,8 @@ type ltac_sign = identifier list * unbound_ltac_var_map
 
 val intern_constr : evar_map -> env -> constr_expr -> rawconstr
 
+val intern_type : evar_map -> env -> constr_expr -> rawconstr
+
 val intern_gen : bool -> evar_map -> env ->
   ?impls:full_implicits_env -> ?allow_soapp:bool -> ?ltacvars:ltac_sign ->
   constr_expr -> rawconstr
@@ -59,10 +61,6 @@ val intern_pattern : env -> cases_pattern_expr ->
   Names.identifier list *
     ((Names.identifier * Names.identifier) list * Rawterm.cases_pattern) list
 
-val intern_pattern : env -> cases_pattern_expr ->
-  Names.identifier list *
-    ((Names.identifier * Names.identifier) list * Rawterm.cases_pattern) list
-
 (*s Composing internalisation with pretyping *)
 
 (* Main interpretation function *)
diff --git a/interp/notation.ml b/interp/notation.ml
index 7d70b296..08c6f31f 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: notation.ml 9481 2007-01-11 19:17:56Z herbelin $ *)
+(* $Id: notation.ml 9694 2007-03-09 18:09:53Z herbelin $ *)
 
 (*i*)
 open Util
@@ -393,8 +393,14 @@ let uninterp_prim_token_cases_pattern c =
       | Some n -> (na,sc,n)
   with Not_found -> raise No_match
 
-let availability_of_prim_token printer_scope local_scopes =
-  let f scope = Hashtbl.mem prim_token_interpreter_tab scope in
+let availability_of_prim_token printer_scope local_scopes t =
+  let f scope =
+    try
+      (* raise Not_found if no primitive interpreter for scope *)
+      let interp = Hashtbl.find prim_token_interpreter_tab scope in
+      (* raise Not_found if no primitive interpreter for this token in scope *)
+      let _ = interp dummy_loc t in true
+    with Not_found -> false in
   let scopes = make_current_scopes local_scopes in
   option_map snd (find_without_delimiters f (Some printer_scope,None) scopes)
 
diff --git a/interp/notation.mli b/interp/notation.mli
index 7be1f9fe..f5c8bdac 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: notation.mli 9481 2007-01-11 19:17:56Z herbelin $ i*)
+(*i $Id: notation.mli 9694 2007-03-09 18:09:53Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -93,7 +93,7 @@ val uninterp_prim_token_cases_pattern :
   cases_pattern -> name * scope_name * prim_token
 
 val availability_of_prim_token : 
-  scope_name -> local_scopes -> delimiters option option
+  scope_name -> local_scopes -> prim_token -> delimiters option option
 
 (*s Declare and interpret back and forth a notation *)
 
diff --git a/interp/reserve.ml b/interp/reserve.ml
index aee981bd..3ec0182b 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: reserve.ml 8752 2006-04-27 19:37:33Z herbelin $ i*)
+(*i $Id: reserve.ml 9976 2007-07-12 11:58:30Z msozeau $ i*)
 
 (* Reserved names *)
 
@@ -73,7 +73,8 @@ let rec unloc = function
               bl,
             Array.map unloc tyl,
             Array.map unloc bv)
-  | RCast (_,c,k,t) -> RCast (dummy_loc,unloc c,k,unloc t)
+  | RCast (_,c, CastConv (k,t)) -> RCast (dummy_loc,unloc c, CastConv (k,unloc t))
+  | RCast (_,c, CastCoerce) -> RCast (dummy_loc,unloc c, CastCoerce)
   | RSort (_,x) -> RSort (dummy_loc,x)
   | RHole (_,x)  -> RHole (dummy_loc,x)
   | RRef (_,x) -> RRef (dummy_loc,x)
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 936b6830..af147866 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: topconstr.ml 9226 2006-10-09 16:11:01Z herbelin $ *)
+(* $Id: topconstr.ml 9976 2007-07-12 11:58:30Z msozeau $ *)
 
 (*i*)
 open Pp
@@ -45,7 +45,7 @@ type aconstr =
   | ASort of rawsort
   | AHole of Evd.hole_kind
   | APatVar of patvar
-  | ACast of aconstr * cast_type * aconstr
+  | ACast of aconstr * aconstr cast_type
 
 (**********************************************************************)
 (* Re-interpret a notation as a rawconstr, taking care of binders     *)
@@ -102,7 +102,10 @@ let rawconstr_of_aconstr_with_binders loc g f e = function
   | AIf (c,(na,po),b1,b2) ->
       let e,na = name_fold_map g e na in
       RIf (loc,f e c,(na,option_map (f e) po),f e b1,f e b2)
-  | ACast (c,k,t) -> RCast (loc,f e c, k,f e t)
+  | ACast (c,k) -> RCast (loc,f e c, 
+			  match k with 
+			    | CastConv (k,t) -> CastConv (k,f e t)
+			    | CastCoerce -> CastCoerce)
   | ASort x -> RSort (loc,x)
   | AHole x  -> RHole (loc,x)
   | APatVar n -> RPatVar (loc,(false,n))
@@ -196,7 +199,9 @@ let aconstr_and_vars_of_rawconstr a =
   | RIf (loc,c,(na,po),b1,b2) ->
       add_name found na;
       AIf (aux c,(na,option_map aux po),aux b1,aux b2)
-  | RCast (_,c,k,t) -> ACast (aux c,k,aux t)
+  | RCast (_,c,k) -> ACast (aux c, 
+			    match k with CastConv (k,t) -> CastConv (k,aux t) 
+			      | CastCoerce -> CastCoerce)
   | RSort (_,s) -> ASort s
   | RHole (_,w) -> AHole w
   | RRef (_,r) -> ARef r
@@ -342,15 +347,21 @@ let rec subst_aconstr subst bound raw =
       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')
-
+  | AHole (Evd.BinderType _ | Evd.QuestionMark _ | Evd.CasesType 
+    | Evd.InternalHole | Evd.TomatchTypeParameter _) -> raw
+
+  | ACast (r1,k) -> 
+      match k with
+	  CastConv (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',CastConv (k,r2'))
+	| CastCoerce ->
+	    let r1' = subst_aconstr subst bound r1 in
+	      if r1' == r1 then raw else
+		ACast (r1',CastCoerce)
+		  
 
 let encode_list_value l = RApp (dummy_loc,RVar (dummy_loc,ldots_var),l)
 
@@ -454,8 +465,10 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
       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) ->
+  | RCast(_,c1, CastConv(_,t1)), ACast(c2, CastConv (_,t2)) ->
       match_ alp metas (match_ alp metas sigma c1 c2) t1 t2
+  | RCast(_,c1, CastCoerce), ACast(c2, CastCoerce) ->
+      match_ alp metas sigma c1 c2
   | RSort (_,s1), ASort s2 when s1 = s2 -> sigma
   | RPatVar _, AHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match
   | a, AHole _ -> sigma
@@ -554,7 +567,7 @@ type constr_expr =
   | CPatVar of loc * (bool * patvar)
   | CEvar of loc * existential_key
   | CSort of loc * rawsort
-  | CCast of loc * constr_expr * cast_type * constr_expr
+  | CCast of loc * constr_expr * constr_expr cast_type
   | CNotation of loc * notation * constr_expr list
   | CPrim of loc * prim_token
   | CDelimiters of loc * string * constr_expr
@@ -616,7 +629,7 @@ let constr_loc = function
   | CPatVar (loc,_) -> loc
   | CEvar (loc,_) -> loc
   | CSort (loc,_) -> loc
-  | CCast (loc,_,_,_) -> loc
+  | CCast (loc,_,_) -> loc
   | CNotation (loc,_,_) -> loc
   | CPrim (loc,_) -> loc
   | CDelimiters (loc,_,_) -> loc
@@ -694,7 +707,8 @@ let fold_constr_expr_with_binders g f n acc = function
   | CApp (loc,(_,t),l) -> List.fold_left (f n) (f n acc t) (List.map fst l)
   | CProdN (_,l,b) | CLambdaN (_,l,b) -> fold_constr_expr_binders g f n acc b l
   | CLetIn (_,na,a,b) -> fold_constr_expr_binders g f n acc b [[na],a]
-  | CCast (loc,a,_,b) -> f n (f n acc a) b
+  | CCast (loc,a,CastConv(_,b)) -> f n (f n acc a) b
+  | CCast (loc,a,CastCoerce) -> f n acc a
   | CNotation (_,_,l) -> List.fold_left (f n) acc l
   | CDelimiters (loc,_,a) -> f n acc a
   | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CDynamic _  | CRef _ ->
@@ -731,7 +745,7 @@ let occur_var_constr_expr id c = Idset.mem id (free_vars_of_constr_expr c)
 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,k,b)  = CCast (dummy_loc,a,k,b)
+let mkCastC (a,k)  = CCast (dummy_loc,a,k)
 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)
@@ -786,7 +800,8 @@ let map_constr_expr_with_binders g f 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,k,b) -> CCast (loc,f e a,k,f e b)
+  | CCast (loc,a,CastConv (k,b)) -> CCast (loc,f e a,CastConv(k, f e b))
+  | CCast (loc,a,CastCoerce) -> CCast (loc,f e a,CastCoerce)
   | 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 _ 
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 131e4170..3c359bd5 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: topconstr.mli 9226 2006-10-09 16:11:01Z herbelin $ i*)
+(*i $Id: topconstr.mli 9976 2007-07-12 11:58:30Z msozeau $ i*)
 
 (*i*)
 open Pp
@@ -41,7 +41,7 @@ type aconstr =
   | ASort of rawsort
   | AHole of Evd.hole_kind
   | APatVar of patvar
-  | ACast of aconstr * cast_type * aconstr
+  | ACast of aconstr * aconstr cast_type
 
 (**********************************************************************)
 (* Translate a rawconstr into a notation given the list of variables  *)
@@ -127,7 +127,7 @@ type constr_expr =
   | CPatVar of loc * (bool * patvar)
   | CEvar of loc * existential_key
   | CSort of loc * rawsort
-  | CCast of loc * constr_expr * cast_type * constr_expr
+  | CCast of loc * constr_expr * constr_expr cast_type
   | CNotation of loc * notation * constr_expr list
   | CPrim of loc * prim_token
   | CDelimiters of loc * string * constr_expr
@@ -167,7 +167,7 @@ val ids_of_cases_indtype : constr_expr -> identifier list
 val mkIdentC : identifier -> constr_expr
 val mkRefC : reference -> constr_expr
 val mkAppC : constr_expr * constr_expr list -> constr_expr
-val mkCastC : constr_expr * cast_type * constr_expr -> constr_expr
+val mkCastC : constr_expr * constr_expr cast_type -> constr_expr
 val mkLambdaC : name located list * constr_expr * constr_expr -> constr_expr
 val mkLetInC : name located * constr_expr * constr_expr -> constr_expr
 val mkProdC : name located list * constr_expr * constr_expr -> constr_expr