diff options
| author | bertot | 2004-02-26 13:35:24 +0000 |
|---|---|---|
| committer | bertot | 2004-02-26 13:35:24 +0000 |
| commit | 67fe536720c5ef5bb509249b9a30cbc6f2cebd92 (patch) | |
| tree | 54964d8e58b41b401d097f044d50b03ee68da118 /translate | |
| parent | e6370d38bd56ccd070cb33d257147ace238efc8b (diff) | |
Keep structure information for Fixpoint declaration and Fix terms
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5386 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'translate')
| -rw-r--r-- | translate/ppconstrnew.ml | 2 | ||||
| -rw-r--r-- | translate/ppvernacnew.ml | 6 |
2 files changed, 4 insertions, 4 deletions
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml index 9b2faf4ba9..b98be6c6c7 100644 --- a/translate/ppconstrnew.ml +++ b/translate/ppconstrnew.ml @@ -354,7 +354,7 @@ let name_of_binder = function | LocalRawAssum (nal,_) -> nal | LocalRawDef (_,_) -> [] -let pr_fixdecl pr (id,n,t0,c0) = +let pr_fixdecl pr (id,n,_,t0,c0) = let (bl,c,t) = extract_def_binders c0 t0 in let (bl,t,c) = let ids = List.flatten (List.map name_of_binder bl) in diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index 85dae24ae3..44599e72f5 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -755,7 +755,7 @@ let rec pr_vernac = function let notations = List.fold_right (fun (_,ntnopt) l -> option_cons ntnopt l) recs [] in let impl = List.map - (fun ((recname,_,arityc,_),_) -> + (fun ((recname,_, _, arityc,_),_) -> let arity = Constrintern.interp_type sigma env0 arityc in let impl_in = if Impargs.is_implicit_args() @@ -777,7 +777,7 @@ let rec pr_vernac = function let rec_sign = List.fold_left - (fun env ((recname,_,arityc,_),_) -> + (fun env ((recname,_,_,arityc,_),_) -> let arity = Constrintern.interp_type sigma env0 arityc in Environ.push_named (recname,None,arity) env) (Global.env()) recs in @@ -786,7 +786,7 @@ let rec pr_vernac = function | LocalRawAssum (nal,_) -> nal | LocalRawDef (_,_) -> [] in let pr_onerec = function - | (id,n,type_0,def0),ntn -> + | (id,n,_,type_0,def0),ntn -> let (bl,def,type_) = extract_def_binders def0 type_0 in let ids = List.flatten (List.map name_of_binder bl) in let (bl,def,type_) = |