diff options
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 28 |
1 files changed, 14 insertions, 14 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 1716cfad..dc339622 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: constrextern.ml 13967 2011-04-08 14:08:43Z herbelin $ *) +(* $Id: constrextern.ml 14641 2011-11-06 11:59:10Z herbelin $ *) (*i*) open Pp @@ -729,13 +729,13 @@ let rec extern inctx scopes vars r = let listdecl = Array.mapi (fun i fi -> let (bl,ty,def) = blv.(i), tyv.(i), bv.(i) in - let (ids,bl) = extern_local_binder scopes vars bl in + let (assums,ids,bl) = extern_local_binder scopes vars bl in let vars0 = List.fold_right (name_fold Idset.add) ids vars in let vars1 = List.fold_right (name_fold Idset.add) ids vars' in let n = match fst nv.(i) with | None -> None - | Some x -> Some (dummy_loc, out_name (List.nth ids x)) + | Some x -> Some (dummy_loc, out_name (List.nth assums x)) in let ro = extern_recursion_order scopes vars (snd nv.(i)) in ((dummy_loc, fi), (n, ro), bl, extern_typ scopes vars0 ty, @@ -745,7 +745,7 @@ let rec extern inctx scopes vars r = | RCoFix n -> let listdecl = Array.mapi (fun i fi -> - let (ids,bl) = extern_local_binder scopes vars blv.(i) in + let (_,ids,bl) = extern_local_binder scopes vars blv.(i) in let vars0 = List.fold_right (name_fold Idset.add) ids vars in let vars1 = List.fold_right (name_fold Idset.add) ids vars' in ((dummy_loc, fi),bl,extern_typ scopes vars0 tyv.(i), @@ -795,24 +795,24 @@ and factorize_lambda inctx scopes vars aty c = | c -> ([],sub_extern inctx scopes vars c) and extern_local_binder scopes vars = function - [] -> ([],[]) + [] -> ([],[],[]) | (na,bk,Some bd,ty)::l -> - let (ids,l) = + let (assums,ids,l) = extern_local_binder scopes (name_fold Idset.add na vars) l in - (na::ids, + (assums,na::ids, LocalRawDef((dummy_loc,na), extern false scopes vars bd) :: l) | (na,bk,None,ty)::l -> let ty = extern_typ scopes vars (anonymize_if_reserved na ty) in (match extern_local_binder scopes (name_fold Idset.add na vars) l with - (ids,LocalRawAssum(nal,k,ty')::l) + (assums,ids,LocalRawAssum(nal,k,ty')::l) when same ty ty' & match na with Name id -> not (occur_var_constr_expr id ty') | _ -> true -> - (na::ids, + (na::assums,na::ids, LocalRawAssum((dummy_loc,na)::nal,k,ty')::l) - | (ids,l) -> - (na::ids, + | (assums,ids,l) -> + (na::assums,na::ids, LocalRawAssum([(dummy_loc,na)],Default bk,ty) :: l)) and extern_eqn inctx scopes vars (loc,ids,pl,c) = @@ -870,7 +870,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function termlists in let bll = List.map (fun (bl,(scopt,scl)) -> - snd (extern_local_binder (scopt,scl@scopes') vars bl)) + pi3 (extern_local_binder (scopt,scl@scopes') vars bl)) binders in insert_delimiters (make_notation loc ntn (l,ll,bll)) key) | SynDefRule kn -> @@ -1007,4 +1007,4 @@ let extern_constr_pattern env pat = let extern_rel_context where env sign = let a = detype_rel_context where [] (names_of_rel_context env) sign in let vars = vars_of_env env in - snd (extern_local_binder (None,[]) vars a) + pi3 (extern_local_binder (None,[]) vars a) |