diff options
| author | filliatr | 2001-03-05 15:54:53 +0000 |
|---|---|---|
| committer | filliatr | 2001-03-05 15:54:53 +0000 |
| commit | 663f5bf4f519914998cf6a0ffcd58e737bab2ffb (patch) | |
| tree | 9e08a1b35400efafc95531aa2bc3612740629d04 | |
| parent | c667fdf87764215d02b21feab4a10a8863c2105b (diff) | |
ocamlweb
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1427 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/extraction/extraction.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index cfc337d288..948d11b0d8 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -102,7 +102,7 @@ let signature_of_arity = in sign_of [] -(* [list_of_ml_arrows] applied to the ML type [a->b->]\cdots[z->t] +(* [list_of_ml_arrows] applied to the ML type [a->b->]\dots[z->t] returns the list [[a;b;...;z]]. *) let rec list_of_ml_arrows = function | Tarr (a, b) -> a :: list_of_ml_arrows b @@ -226,7 +226,7 @@ let rec extract_type env sign c = | Tprop -> (Miniml.Tprop :: args, fl) | Tmltype (mla,_,fl') -> (mla :: args, fl')) (List.combine (list_firstn nargs (List.rev sc)) args) - (* FIXME: List.rev before list_firstn? *) + (* FIXME: [List.rev] before [list_firstn]? *) ([],fl) in let flc = List.map (fun i -> Tvar i) flc in @@ -370,7 +370,9 @@ and extract_mib sp = | Tarity | Tprop -> assert false | Tmltype (mlt, s, f) -> let l = list_of_ml_arrows mlt in - (*let (l,s) = extract_params mib.mind_nparams (l,s) in*) + (*i + let (l,s) = extract_params mib.mind_nparams (l,s) in + i*) add_constructor_extraction ((sp,i),succ j) (l,s); f @ fl) ib.mind_nf_lc fl) |