Imported Upstream version 8.1+dfsgupstream/8.1+dfsg

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),