diff options
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/ascent.mli | 1 | ||||
| -rw-r--r-- | contrib/interface/parse.ml | 6 | ||||
| -rw-r--r-- | contrib/interface/vtp.ml | 3 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 9 |
4 files changed, 14 insertions, 5 deletions
diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli index b6cc55f6..ef1d095e 100644 --- a/contrib/interface/ascent.mli +++ b/contrib/interface/ascent.mli @@ -642,6 +642,7 @@ and ct_TACTIC_COM = | CT_elim_type of ct_FORMULA | CT_exact of ct_FORMULA | CT_exact_no_check of ct_FORMULA + | CT_vm_cast_no_check of ct_FORMULA | CT_exists of ct_SPEC_LIST | CT_fail of ct_ID_OR_INT * ct_STRING_OPT | CT_first of ct_TACTIC_COM * ct_TACTIC_COM list diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml index 4d4df59f..8cca7614 100644 --- a/contrib/interface/parse.ml +++ b/contrib/interface/parse.ml @@ -315,21 +315,21 @@ let parse_file_action reqid file_name = fnl () ++ Cerrors.explain_exn e));; let add_rec_path_action reqid string_arg ident_arg = - let directory_name = glob string_arg in + let directory_name = expand_path_macros string_arg in begin add_rec_path directory_name (Libnames.dirpath_of_string ident_arg) end;; let add_path_action reqid string_arg = - let directory_name = glob string_arg in + let directory_name = expand_path_macros string_arg in begin add_path directory_name Names.empty_dirpath end;; let print_version_action () = msgnl (mt ()); - msgnl (str "$Id: parse.ml 7844 2006-01-11 16:36:14Z bertot $");; + msgnl (str "$Id: parse.ml 9397 2006-11-21 21:50:54Z herbelin $");; let load_syntax_action reqid module_name = msg (str "loading " ++ str module_name ++ str "... "); diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml index fe227f99..166a0cbf 100644 --- a/contrib/interface/vtp.ml +++ b/contrib/interface/vtp.ml @@ -1549,6 +1549,9 @@ and fTACTIC_COM = function | CT_exact_no_check(x1) -> fFORMULA x1; fNODE "exact_no_check" 1 +| CT_vm_cast_no_check(x1) -> + fFORMULA x1; + fNODE "vm_cast_no_check" 1 | CT_exists(x1) -> fSPEC_LIST x1; fNODE "exists" 1 diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 6c9e8239..60195229 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1060,6 +1060,7 @@ and xlate_tac = | TacAssumption -> CT_assumption | TacExact c -> CT_exact (xlate_formula c) | TacExactNoCheck c -> CT_exact_no_check (xlate_formula c) + | TacVmCastNoCheck c -> CT_vm_cast_no_check (xlate_formula c) | TacDestructHyp (true, (_,id)) -> CT_cdhyp (xlate_ident id) | TacDestructHyp (false, (_,id)) -> CT_dhyp (xlate_ident id) | TacDestructConcl -> CT_dconcl @@ -1978,7 +1979,7 @@ let rec xlate_vernac = | VernacOpenCloseScope(false, true, s) -> CT_open_scope(CT_ident s) | VernacOpenCloseScope(true, false, s) -> CT_local_close_scope(CT_ident s) | VernacOpenCloseScope(false, false, s) -> CT_close_scope(CT_ident s) - | VernacArgumentsScope(qid, l) -> + | VernacArgumentsScope(true, qid, l) -> CT_arguments_scope(loc_qualid_to_ct_ID qid, CT_id_opt_list (List.map @@ -1986,6 +1987,8 @@ let rec xlate_vernac = match x with None -> ctv_ID_OPT_NONE | Some x -> ctf_ID_OPT_SOME(CT_ident x)) l)) + | VernacArgumentsScope(false, qid, l) -> + xlate_error "TODO: Arguments Scope Global" | VernacDelimiters(s1,s2) -> CT_delim_scope(CT_ident s1, CT_ident s2) | VernacBindScope(id, a::l) -> let xlate_class_rawexpr = function @@ -2060,7 +2063,7 @@ let rec xlate_vernac = | VernacNop -> CT_proof_no_op | VernacComments l -> CT_scomments(CT_scomment_content_list (List.map xlate_comment l)) - | VernacDeclareImplicits(id, opt_positions) -> + | VernacDeclareImplicits(true, id, opt_positions) -> CT_implicits (reference_to_ct_ID id, match opt_positions with @@ -2073,6 +2076,8 @@ let rec xlate_vernac = -> xlate_error "explication argument by rank is obsolete" | ExplByName id -> CT_ident (string_of_id id)) l))) + | VernacDeclareImplicits(false, id, opt_positions) -> + xlate_error "TODO: Implicit Arguments Global" | VernacReserve((_,a)::l, f) -> CT_reserve(CT_id_ne_list(xlate_ident a, List.map (fun (_,x) -> xlate_ident x) l), |