diff options
| author |  Samuel Mimram <smimram@debian.org> | 2006-07-13 14:28:31 +0000 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2006-07-13 14:28:31 +0000 |
| commit | de0085539583f59dc7c4bf4e272e18711d565466 (patch) | |
| tree | 347e1d95a2df56f79a01b303e485563588179e91 /interp/constrextern.ml | |
| parent | e978da8c41d8a3c19a29036d9c569fbe2a4616b0 (diff) | |
Imported Upstream version 8.0pl3+8.1beta.2upstream/8.0pl3+8.1beta.2
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index daa57b77..570d113d 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: constrextern.ml 8831 2006-05-19 09:29:54Z herbelin $ *) +(* $Id: constrextern.ml 8997 2006-07-03 16:40:20Z herbelin $ *) (*i*) open Pp @@ -186,7 +186,7 @@ let rec check_same_type ty1 ty2 = | CCases(_,_,a1,brl1), CCases(_,_,a2,brl2) -> List.iter2 (fun (tm1,_) (tm2,_) -> check_same_type tm1 tm2) a1 a2; List.iter2 (fun (_,pl1,r1) (_,pl2,r2) -> - List.iter2 check_same_pattern pl1 pl2; + List.iter2 (List.iter2 check_same_pattern) pl1 pl2; check_same_type r1 r2) brl1 brl2 | CHole _, CHole _ -> () | CPatVar(_,i1), CPatVar(_,i2) when i1=i2 -> () @@ -797,7 +797,7 @@ and extern_local_binder scopes vars = function LocalRawAssum([(dummy_loc,na)],ty) :: l)) and extern_eqn inctx scopes vars (loc,ids,pl,c) = - (loc,List.map (extern_cases_pattern_in_scope scopes vars) pl, + (loc,[List.map (extern_cases_pattern_in_scope scopes vars) pl], extern inctx scopes vars c) and extern_symbol (tmp_scope,scopes as allscopes) vars t = function @@ -843,6 +843,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function and extern_recursion_order scopes vars = function RStructRec -> CStructRec | RWfRec c -> CWfRec (extern true scopes vars c) + | RMeasureRec c -> CMeasureRec (extern true scopes vars c) let extern_rawconstr vars c = |