diff options
| author | bertot | 2004-02-12 12:19:43 +0000 |
|---|---|---|
| committer | bertot | 2004-02-12 12:19:43 +0000 |
| commit | 61de148a1b0c357c54e7fecb9152c1f153552cf3 (patch) | |
| tree | fbcbadda4dbc6e661764ed286551b02c8d786918 | |
| parent | d117e24469c991e3e3ff9e5defc0d9d9aff00865 (diff) | |
Implicits can have an optional list of argument, which is different
from an empty list of arguments.
in H at 2 |- * was badly translated in clauses (for replacement tactics)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5318 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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), |