diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-05-21 13:12:34 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-05-21 13:12:34 +0000 |
| commit | 1e160525650bb03c286d78f061f73dcd865b0937 (patch) | |
| tree | 04af7b15a7767262167f11b2627f110e272dc79f /contrib/interface | |
| parent | 215f42dae466bbbdb865303af05c7e70b5fb3d15 (diff) | |
MAJ
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4044 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/xlate.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index a011416f1..9fbd1158f 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -536,9 +536,7 @@ let xlate_context_pattern = function let xlate_match_context_hyps = function - | NoHypId b -> CT_premise_pattern(ctv_ID_OPT_NONE, xlate_context_pattern b) - | Hyp ((_,id),b) -> CT_premise_pattern(ctf_ID_OPT_SOME (xlate_ident id), - xlate_context_pattern b) + | Hyp (na,b) -> CT_premise_pattern(xlate_id_opt na, xlate_context_pattern b) let xlate_largs_to_id_unit largs = @@ -1554,7 +1552,8 @@ let xlate_vernac = (CT_co_ind co_or_ind, CT_ind_spec_list (List.map strip_mutind lmi)) | VernacFixpoint [] -> xlate_error "mutual recursive" | VernacFixpoint (lm :: lmi) -> - let strip_mutrec (fid, n, arf, ardef) = + let strip_mutrec ((fid, n, arf, ardef), ntn) = + (* TODO: handle ntn in mutual recursive *) let (bl,arf,ardef) = Ppconstr.split_fix (n+1) arf ardef in let arf = xlate_formula arf in let ardef = xlate_formula ardef in |