diff options
| -rw-r--r-- | contrib/interface/ascent.mli | 5 | ||||
| -rw-r--r-- | contrib/interface/vtp.ml | 5 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 13 |
3 files changed, 17 insertions, 6 deletions
diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli index 30c11770af..36b9b678de 100644 --- a/contrib/interface/ascent.mli +++ b/contrib/interface/ascent.mli @@ -78,7 +78,7 @@ and ct_COMMAND = | CT_hint_extern of ct_INT * ct_FORMULA * ct_TACTIC_COM * ct_ID_LIST | CT_hintrewrite of ct_ORIENTATION * ct_FORMULA_NE_LIST * ct_ID * ct_TACTIC_COM | CT_hints of ct_ID * ct_ID_NE_LIST * ct_ID_LIST - | CT_implicits of ct_ID * ct_ID_LIST + | CT_implicits of ct_ID * ct_ID_LIST_OPT | CT_import_id of ct_ID_NE_LIST | CT_ind_scheme of ct_SCHEME_SPEC_LIST | CT_infix of ct_STRING * ct_ID * ct_MODIFIER_LIST * ct_ID_OPT @@ -321,6 +321,9 @@ and ct_ID_LIST = CT_id_list of ct_ID list and ct_ID_LIST_LIST = CT_id_list_list of ct_ID_LIST list +and ct_ID_LIST_OPT = + CT_coerce_ID_LIST_to_ID_LIST_OPT of ct_ID_LIST + | CT_coerce_NONE_to_ID_LIST_OPT of ct_NONE and ct_ID_NE_LIST = CT_id_ne_list of ct_ID * ct_ID list and ct_ID_NE_LIST_OR_STAR = diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml index 55a1488465..94d338b10d 100644 --- a/contrib/interface/vtp.ml +++ b/contrib/interface/vtp.ml @@ -251,7 +251,7 @@ and fCOMMAND = function fNODE "hints" 3 | CT_implicits(x1, x2) -> fID x1; - fID_LIST x2; + fID_LIST_OPT x2; fNODE "implicits" 2 | CT_import_id(x1) -> fID_NE_LIST x1; @@ -871,6 +871,9 @@ and fID_LIST_LIST = function | CT_id_list_list l -> (List.iter fID_LIST l); fNODE "id_list_list" (List.length l) +and fID_LIST_OPT = function +| CT_coerce_ID_LIST_to_ID_LIST_OPT x -> fID_LIST x +| CT_coerce_NONE_to_ID_LIST_OPT x -> fNONE x and fID_NE_LIST = function | CT_id_ne_list(x,l) -> fID x; diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 07c59aa769..f09a8595bb 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -481,9 +481,13 @@ let xlate_hyp_location = CT_intype(xlate_ident id, nums_to_int_list nums) | AI (_,id), nums, (InHypValueOnly,_) -> CT_invalue(xlate_ident id, nums_to_int_list nums) - | AI (_,id), _, (InHyp,_) -> + | AI (_,id), [], (InHyp,_) -> CT_coerce_UNFOLD_to_HYP_LOCATION (CT_coerce_ID_to_UNFOLD (xlate_ident id)) + | AI (_,id), a::l, (InHyp,_) -> + CT_coerce_UNFOLD_to_HYP_LOCATION + (CT_unfold_occ (xlate_ident id, + CT_int_ne_list(CT_int a, nums_to_int_list_aux l))) | MetaId _, _,_ -> xlate_error "MetaId not supported in xlate_hyp_location (should occur only in quotations)" @@ -1970,14 +1974,15 @@ let rec xlate_vernac = CT_implicits (reference_to_ct_ID id, match opt_positions with - None -> CT_id_list[] + None -> CT_coerce_NONE_to_ID_LIST_OPT CT_none | Some l -> - CT_id_list + CT_coerce_ID_LIST_to_ID_LIST_OPT + (CT_id_list (List.map (function ExplByPos x -> xlate_error "explication argument by rank is obsolete" - | ExplByName id -> CT_ident (string_of_id id)) l)) + | ExplByName id -> CT_ident (string_of_id id)) l))) | VernacReserve((_,a)::l, f) -> CT_reserve(CT_id_ne_list(xlate_ident a, List.map (fun (_,x) -> xlate_ident x) l), |