aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/interface/Centaur.v7
-rw-r--r--contrib/interface/ascent.mli1
-rw-r--r--contrib/interface/centaur.ml16
-rw-r--r--contrib/interface/ctast.ml69
-rw-r--r--contrib/interface/dad.ml12
-rw-r--r--contrib/interface/dad.mli6
-rw-r--r--contrib/interface/name_to_ast.ml23
-rw-r--r--contrib/interface/parse.ml57
-rw-r--r--contrib/interface/pbp.ml8
-rw-r--r--contrib/interface/pbp.mli2
-rw-r--r--contrib/interface/translate.ml4
-rw-r--r--contrib/interface/xlate.ml14
-rw-r--r--contrib/interface/xlate.mli16
13 files changed, 155 insertions, 80 deletions
diff --git a/contrib/interface/Centaur.v b/contrib/interface/Centaur.v
index f2e1686455..5cca616a53 100644
--- a/contrib/interface/Centaur.v
+++ b/contrib/interface/Centaur.v
@@ -1,3 +1,4 @@
+Declare ML Module "ctast".
Declare ML Module "paths".
Declare ML Module "name_to_ast".
Declare ML Module "xlate".
@@ -73,10 +74,10 @@ Grammar tactic simple_tactic : ast :=
procedure changed from V6.1 and does not reprint the command anymore. *)
Grammar vernac vernac : ast :=
text_proof_flag_on [ "Text" "Mode" "fr" "." ] ->
- [(TEXT_MODE (AST {fr}))]
+ [(TEXT_MODE (AST "fr"))]
| text_proof_flag_on [ "Text" "Mode" "en" "." ] ->
- [(TEXT_MODE (AST {en}))]
+ [(TEXT_MODE (AST "en"))]
| text_proof_flag_on [ "Text" "Mode" "Off" "." ] ->
- [(TEXT_MODE (AST {off}))].
+ [(TEXT_MODE (AST "off"))].
diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index d6eaf0c6d1..3dff01937c 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -1,3 +1,4 @@
+
type ct_ASSOC =
CT_coerce_NONE_to_ASSOC of ct_NONE
| CT_lefta
diff --git a/contrib/interface/centaur.ml b/contrib/interface/centaur.ml
index 6e1555d591..e4c852f7fd 100644
--- a/contrib/interface/centaur.ml
+++ b/contrib/interface/centaur.ml
@@ -302,12 +302,12 @@ and ntyp = nf_betaiota typ in
(* The following function is copied from globpr in env/printer.ml *)
let globcv = function
- | Node(_,"MUTIND", (Path(_,sl,s))::(Num(_,tyi))::_) ->
+ | Node(_,"MUTIND", (Path(_,sp))::(Num(_,tyi))::_) ->
convert_qualid
- (Global.qualid_of_global (IndRef(section_path sl s,tyi)))
- | Node(_,"MUTCONSTRUCT",(Path(_,sl,s))::(Num(_,tyi))::(Num(_,i))::_) ->
+ (Global.qualid_of_global (IndRef(sp,tyi)))
+ | Node(_,"MUTCONSTRUCT",(Path(_,sp))::(Num(_,tyi))::(Num(_,i))::_) ->
convert_qualid
- (Global.qualid_of_global (ConstructRef ((section_path sl s, tyi), i)))
+ (Global.qualid_of_global (ConstructRef ((sp, tyi), i)))
| _ -> failwith "globcv : unexpected value";;
let pbp_tac_pcoq =
@@ -446,7 +446,7 @@ let logical_kill n =
let command_changes = [
("TEXT_MODE",
(function
- | [VARG_AST (Id(_,x))] ->
+ | [VARG_AST (Str(_,x))] ->
(match x with
"fr" -> (function () -> text_proof_flag := "fr")
| "en" -> (function () -> text_proof_flag := "en")
@@ -626,7 +626,7 @@ let command_changes = [
(function
| [VARG_QUALID qid] ->
(function () ->
- let results = xlate_vernac_list (name_to_ast qid) in
+ let results = xlate_vernac_list (Ctast.ast_to_ct (name_to_ast qid)) in
output_results
[<'fNL; 'sTR "message"; 'fNL; 'sTR "PRINT_VALUE"; 'fNL >]
(Some (P_cl results)))
@@ -653,7 +653,7 @@ let command_changes = [
| VARG_TACTIC_ARG(Redexp redexp):: VARG_CONSTR c :: g ->
let evmap, env = Vernacentries.get_current_context_of_args g in
let redfun =
- ct_print_eval c (Tacred.reduction_of_redexp redexp env evmap) env in
+ ct_print_eval (Ctast.ast_to_ct c) (Tacred.reduction_of_redexp redexp env evmap) env in
fun () ->
let strm, vtp = redfun evmap (judgment_of_rawconstr evmap env c) in
output_results strm vtp
@@ -728,7 +728,7 @@ let command_creations = [
let start_pcoq_mode debug =
begin
start_dad();
- set_xlate_mut_stuff globcv;
+ set_xlate_mut_stuff (fun x ->Ctast.ast_to_ct (globcv (Ctast.ct_to_ast x)));
declare_in_coq();
add_tactic "PcoqPbp" pbp_tac_pcoq;
add_tactic "Dad" dad_tac_pcoq;
diff --git a/contrib/interface/ctast.ml b/contrib/interface/ctast.ml
new file mode 100644
index 0000000000..4ed6dbcd9e
--- /dev/null
+++ b/contrib/interface/ctast.ml
@@ -0,0 +1,69 @@
+(* A copy of pre V7 ast *)
+
+open Names
+
+type loc = int * int
+
+type t =
+ | Node of loc * string * t list
+ | Nvar of loc * string
+ | Slam of loc * string option * t
+ | Num of loc * int
+ | Id of loc * string
+ | Str of loc * string
+ | Path of loc * string list* string
+ | Dynamic of loc * Dyn.t
+
+let section_path sl k =
+ match List.rev sl with
+ | s::pa -> make_path (List.rev (List.map id_of_string pa)) (id_of_string s) (kind_of_string k)
+ | [] -> invalid_arg "section_path"
+
+let is_meta s = String.length s > 0 && s.[0] == '$'
+
+let purge_str s =
+ if String.length s == 0 || s.[0] <> '$' then s
+ else String.sub s 1 (String.length s - 1)
+
+let rec ct_to_ast = function
+ | Node (loc,a,b) -> Coqast.Node (loc,a,List.map ct_to_ast b)
+ | Nvar (loc,a) ->
+ if is_meta a then Coqast.Nmeta (loc,purge_str a)
+ else Coqast.Nvar (loc,id_of_string a)
+ | Slam (loc,Some a,b) ->
+ if is_meta a then Coqast.Smetalam (loc,purge_str a,ct_to_ast b)
+ else Coqast.Slam (loc,Some (id_of_string a),ct_to_ast b)
+ | Slam (loc,None,b) -> Coqast.Slam (loc,None,ct_to_ast b)
+ | Num (loc,a) -> Coqast.Num (loc,a)
+ | Id (loc,a) -> Coqast.Id (loc,a)
+ | Str (loc,a) -> Coqast.Str (loc,a)
+ | Path (loc,sl,k) -> Coqast.Path (loc,section_path sl k)
+ | Dynamic (loc,a) -> Coqast.Dynamic (loc,a)
+
+let rec ast_to_ct = function
+ | Coqast.Node (loc,a,b) -> Node (loc,a,List.map ast_to_ct b)
+ | Coqast.Nvar (loc,a) -> Nvar (loc,string_of_id a)
+ | Coqast.Nmeta (loc,a) -> Nvar (loc,"$"^a)
+ | Coqast.Slam (loc,Some a,b) ->
+ Slam (loc,Some (string_of_id a),ast_to_ct b)
+ | Coqast.Slam (loc,None,b) -> Slam (loc,None,ast_to_ct b)
+ | Coqast.Smetalam (loc,a,b) -> Slam (loc,Some ("$"^a),ast_to_ct b)
+ | Coqast.Num (loc,a) -> Num (loc,a)
+ | Coqast.Id (loc,a) -> Id (loc,a)
+ | Coqast.Str (loc,a) -> Str (loc,a)
+ | Coqast.Path (loc,a) ->
+ let (sl,bn,pk) = repr_path a in
+ Path(loc, (List.map string_of_id sl) @ [string_of_id bn],(* Bidon *) "CCI")
+ | Coqast.Dynamic (loc,a) -> Dynamic (loc,a)
+
+let loc = function
+ | Node (loc,_,_) -> loc
+ | Nvar (loc,_) -> loc
+ | Slam (loc,_,_) -> loc
+ | Num (loc,_) -> loc
+ | Id (loc,_) -> loc
+ | Str (loc,_) -> loc
+ | Path (loc,_,_) -> loc
+ | Dynamic (loc,_) -> loc
+
+let str s = Str(Ast.dummy_loc,s)
diff --git a/contrib/interface/dad.ml b/contrib/interface/dad.ml
index c26a8039d4..f84fe33ef3 100644
--- a/contrib/interface/dad.ml
+++ b/contrib/interface/dad.ml
@@ -11,7 +11,7 @@ open Tactics;;
open Tacticals;;
open Pattern;;
open Reduction;;
-open Coqast;;
+open Ctast;;
open Termast;;
open Astterm;;
open Vernacinterp;;
@@ -36,10 +36,10 @@ open Paths;;
*)
-type dad_rule = Coqast.t * int list * int list * int * int list * Coqast.t;;
+type dad_rule = Ctast.t * int list * int list * int * int list * Ctast.t;;
(* This value will be used systematically when constructing objects of
- type Coqast.t, the value is stupid and meaningless, but it is needed
+ type Ctast.t, the value is stupid and meaningless, but it is needed
to construct well-typed terms. *)
let zz = (0,0);;
@@ -66,7 +66,7 @@ let map_subst (env :env)
let rec map_subst_aux = function
Node(_, "META", [Num(_, i)]) ->
let constr = List.assoc i subst in
- ast_of_constr false env constr
+ Ctast.ast_to_ct (ast_of_constr false env constr)
| Node(loc, s, l) -> Node(loc, s, List.map map_subst_aux l)
| ast -> ast in
map_subst_aux;;
@@ -89,7 +89,7 @@ let rec find_cmd (l:(string * dad_rule) list) env constr p p1 p2 =
Failure s -> failwith "internal" in
let _, constr_pat =
interp_constrpattern Evd.empty (Global.env())
- pat in
+ (ct_to_ast pat) in
let subst = matches constr_pat term_to_match in
if (is_prefix p_f (p_r@p1)) & (is_prefix p_l (p_r@p2)) then
map_subst env subst cmd
@@ -251,7 +251,7 @@ vinterp_add "AddDadRule"
VARG_NUMBERLIST p2; VARG_TACTIC com] ->
(function () ->
let pr = match decompose_path (p1, p2) with pr, _, _ -> pr in
- (add_dad_rule name pat p1 p2 (List.length pr) pr com))
+ (add_dad_rule name (Ctast.ast_to_ct pat) p1 p2 (List.length pr) pr (Ctast.ast_to_ct com)))
| _ -> errorlabstrm "AddDadRule1"
[< 'sTR "AddDadRule2">]);
add_dad_rule "distributivity-inv"
diff --git a/contrib/interface/dad.mli b/contrib/interface/dad.mli
index 1d097804a5..9f8f7354b2 100644
--- a/contrib/interface/dad.mli
+++ b/contrib/interface/dad.mli
@@ -4,7 +4,7 @@ open Tacmach;;
val dad_rule_names : unit -> string list;;
val start_dad : unit -> unit;;
-val dad_tac : (Coqast.t -> 'a) -> tactic_arg list -> goal sigma ->
+val dad_tac : (Ctast.t -> 'a) -> tactic_arg list -> goal sigma ->
goal list sigma * validation;;
-val add_dad_rule : string -> Coqast.t -> (int list) -> (int list) ->
- int -> (int list) -> Coqast.t -> unit;;
+val add_dad_rule : string -> Ctast.t -> (int list) -> (int list) ->
+ int -> (int list) -> Ctast.t -> unit;;
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index 20122d5762..6f1be02fb4 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -26,7 +26,7 @@ let convert_env =
match na with
| Name id ->
ope("BINDER",
- [ast_of_constr true env c;nvar(string_of_id id)])
+ [ast_of_constr true env c;nvar id])
| Anonymous -> failwith "anomaly: Anonymous variables in inductives" in
let rec cvrec env = function
[] -> []
@@ -85,9 +85,9 @@ let implicit_args_to_ast_list sp mipv =
let convert_qualid qid =
let d, id = Nametab.repr_qualid qid in
match d with
- [] -> nvar(string_of_id id)
+ [] -> nvar id
| _ -> ope("QUALID", List.fold_right (fun s l -> (nvar s)::l) d
- [nvar (string_of_id id)]);;
+ [nvar id]);;
(* This function converts constructors for an inductive definition to a
Coqast.t. It is obtained directly from print_constructors in pretty.ml *)
@@ -96,7 +96,7 @@ let convert_constructors envpar names types =
let array_idC =
array_map2
(fun n t -> ope("BINDER",
- [ast_of_constr true envpar t; nvar(string_of_id n)]))
+ [ast_of_constr true envpar t; nvar n]))
names types in
Node((0,0), "BINDERLIST", Array.to_list array_idC);;
@@ -163,9 +163,9 @@ let constant_to_ast_list sp =
let l = constant_implicits_list sp in
(match c with
None ->
- make_variable_ast (string_of_id (basename sp)) typ l
+ make_variable_ast (basename sp) typ l
| Some c1 ->
- make_definition_ast (string_of_id (basename sp)) c1 typ l)
+ make_definition_ast (basename sp) c1 typ l)
else
errorlabstrm "print" [< 'sTR "printing of FW terms not implemented" >];;
@@ -174,9 +174,9 @@ let variable_to_ast_list sp =
let l = implicits_of_var sp in
(match c with
None ->
- make_variable_ast (string_of_id id) v l
+ make_variable_ast id v l
| Some c1 ->
- make_definition_ast (string_of_id id) c1 v l);;
+ make_definition_ast id c1 v l);;
(* this function is taken from print_inductive in file pretty.ml *)
@@ -208,7 +208,7 @@ let leaf_entry_to_ast_list (sp,lobj) =
let name_to_ast (qid:Nametab.qualid) =
let l =
try
- let sp,_ = Nametab.locate_obj qid in
+ let sp = Nametab.locate_obj qid in
let (sp,lobj) =
let (sp,entry) =
List.find (fun en -> (fst en) = sp) (Lib.contents_after None)
@@ -231,9 +231,8 @@ let name_to_ast (qid:Nametab.qualid) =
if dir <> [] then raise Not_found;
let (c,typ) = Global.lookup_named name in
(match c with
- None -> make_variable_ast (string_of_id name) typ []
- | Some c1 -> make_definition_ast
- (string_of_id name) c1 typ [])
+ None -> make_variable_ast name typ []
+ | Some c1 -> make_definition_ast name c1 typ [])
with Not_found ->
try
let sp = Syntax_def.locate_syntactic_definition qid in
diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml
index bdda47e38f..ff76f2c753 100644
--- a/contrib/interface/parse.ml
+++ b/contrib/interface/parse.ml
@@ -4,7 +4,7 @@ open System;;
open Pp;;
-open Coqast;;
+open Ctast;;
open Library;;
@@ -58,14 +58,14 @@ let ctf_FileErrorMessage reqid pps =
function has no effect on parsing *)
let try_require_module import specif name fname =
try Library.require_module (if specif = "UNSPECIFIED" then None
- else Some (specif = "SPECIFICATION")) name fname (import = "IMPORT")
+ else Some (specif = "SPECIFICATION")) (Nametab.make_qualid [] (Names.id_of_string name)) fname (import = "IMPORT")
with
| e -> mSGNL [< 'sTR "Reinterning of "; 'sTR name; 'sTR " failed" >];;
let execute_when_necessary ast =
(match ast with
| Node (_, "GRAMMAR", ((Nvar (_, s)) :: ((Node (_, "ASTLIST", al)) :: []))) ->
- Metasyntax.add_grammar_obj s al
+ Metasyntax.add_grammar_obj s (List.map Ctast.ct_to_ast al)
| Node (_, "TOKEN", ((Str (_, s)) :: [])) -> Metasyntax.add_token_obj s
| Node (_, "Require",
((Str (_, import)) ::
@@ -91,9 +91,9 @@ let rec discard_to_dot stream =
let rec decompose_string s n =
try let index = String.index_from s n '\n' in
- (Ast.str (String.sub s n (index - n)))::
+ (Ctast.str (String.sub s n (index - n)))::
(decompose_string s (index + 1))
- with Not_found -> [Ast.str(String.sub s n ((String.length s) - n))];;
+ with Not_found -> [Ctast.str(String.sub s n ((String.length s) - n))];;
let make_string_list file_chan fst_pos snd_pos =
let len = (snd_pos - fst_pos) in
@@ -140,11 +140,12 @@ let rec get_substring_list string_list fst_pos snd_pos =
(* When parsing a list of commands, we try to recover error messages for
each individual command. *)
+
let parse_command_list reqid stream string_list =
let rec parse_whole_stream () =
let this_pos = Stream.count stream in
let first_ast =
- try Gram.Entry.parse Pcoq.main_entry (Gram.parsable stream)
+ try option_app Ctast.ast_to_ct (Gram.Entry.parse Pcoq.main_entry (Gram.parsable stream))
with
| (Stdpp.Exc_located(l, Stream.Error txt)) as e ->
begin
@@ -154,7 +155,7 @@ let parse_command_list reqid stream string_list =
mSGNL [< 'sTR "debug"; 'fNL; 'iNT this_pos; 'fNL; 'iNT
(Stream.count stream) >];
Some( Node(l, "PARSING_ERROR",
- List.map Ast.str
+ List.map Ctast.str
(get_substring_list string_list this_pos
(Stream.count stream))))
with End_of_file -> None
@@ -163,7 +164,7 @@ let parse_command_list reqid stream string_list =
begin
discard_to_dot stream;
Some(Node((0,0), "PARSING_ERROR2",
- List.map Ast.str
+ List.map Ctast.str
(get_substring_list string_list this_pos
(Stream.count stream))))
end in
@@ -190,25 +191,25 @@ let parse_string_action reqid phylum char_stream string_list =
P_c
(xlate_vernac
(execute_when_necessary
- (Gram.Entry.parse Pcoq.Vernac_.vernac_eoi (Gram.parsable char_stream))))
+ (Ctast.ast_to_ct (Gram.Entry.parse Pcoq.Vernac_.vernac_eoi (Gram.parsable char_stream)))))
| "TACTIC_COM" ->
P_t
- (xlate_tactic (Gram.Entry.parse Pcoq.Tactic.tactic_eoi
- (Gram.parsable char_stream)))
+ (xlate_tactic (Ctast.ast_to_ct(Gram.Entry.parse Pcoq.Tactic.tactic_eoi
+ (Gram.parsable char_stream))))
| "FORMULA" ->
P_f
(xlate_formula
- (Gram.Entry.parse Pcoq.Constr.constr_eoi (Gram.parsable char_stream)))
+ (Ctast.ast_to_ct (Gram.Entry.parse Pcoq.Constr.constr_eoi (Gram.parsable char_stream))))
| "ID" -> P_id (xlate_id
- (Gram.Entry.parse Pcoq.Prim.ident
- (Gram.parsable char_stream)))
+ (Ctast.ast_to_ct (Gram.Entry.parse Pcoq.Prim.ident
+ (Gram.parsable char_stream))))
| "STRING" ->
P_s
- (xlate_string (Gram.Entry.parse Pcoq.Prim.string
- (Gram.parsable char_stream)))
+ (xlate_string (Ctast.ast_to_ct (Gram.Entry.parse Pcoq.Prim.string
+ (Gram.parsable char_stream))))
| "INT" ->
- P_i (xlate_int (Gram.Entry.parse Pcoq.Prim.number
- (Gram.parsable char_stream)))
+ P_i (xlate_int (Ctast.ast_to_ct (Gram.Entry.parse Pcoq.Prim.number
+ (Gram.parsable char_stream))))
| _ -> error "parse_string_action : bad phylum" in
print_parse_results reqid msg
with
@@ -242,7 +243,7 @@ let parse_file_action reqid file_name =
match
try
let this_ast =
- Gram.Entry.parse Pcoq.main_entry (Gram.parsable stream) in
+ option_app Ctast.ast_to_ct (Gram.Entry.parse Pcoq.main_entry (Gram.parsable stream)) in
this_ast
with
| Stdpp.Exc_located(l,Stream.Error txt ) ->
@@ -294,8 +295,7 @@ let add_path dir coq_dirpath =
if coq_dirpath = [] then anomaly "add_path: empty path in library";
if exists_dir dir then
begin
- Library.add_load_path_entry
- { directory = dir; coq_dirpath = coq_dirpath };
+ Library.add_load_path_entry (dir,coq_dirpath);
Nametab.push_library_root (List.hd coq_dirpath)
end
else
@@ -303,8 +303,10 @@ let add_path dir coq_dirpath =
let add_rec_path dir coq_dirpath =
if coq_dirpath = [] then anomaly "add_path: empty path in library";
- let dirs = all_subdirs dir (Some coq_dirpath) in
+ let dirs = all_subdirs dir in
if dirs <> [] then
+ let convert = List.map Names.id_of_string in
+ let dirs = List.map (fun (lp,cp) -> (lp,coq_dirpath@(convert cp))) dirs in
begin
List.iter Library.add_load_path_entry dirs;
Nametab.push_library_root (List.hd coq_dirpath)
@@ -316,7 +318,7 @@ let add_path_action reqid string_arg =
let directory_name = glob string_arg in
let alias = Filename.basename directory_name in
begin
- add_path directory_name [alias]
+ add_path directory_name [Names.id_of_string alias]
end;;
let print_version_action () =
@@ -325,9 +327,12 @@ let print_version_action () =
let load_syntax_action reqid module_name =
mSG [< 'sTR "loading "; 'sTR module_name; 'sTR "... " >];
- try (load_module module_name None;
+ try
+ (let qid = Nametab.make_qualid [] (Names.id_of_string module_name) in
+ read_module qid;
mSG [< 'sTR "opening... ">];
- import_module module_name;
+ let fullname = Nametab.locate_loaded_library qid in
+ import_module fullname;
mSGNL [< 'sTR "done"; 'fNL >];
())
with
@@ -367,7 +372,7 @@ Libobject.relax true;
add_rec_path (Filename.concat coqdir "theories") [Nametab.coq_root];
add_path (Filename.concat coqdir "tactics") [Nametab.coq_root];
add_rec_path (Filename.concat coqdir "contrib") [Nametab.coq_root];
- List.iter (fun {directory=a} -> mSGNL [< 'sTR a >]) (get_load_path())
+ List.iter (fun a -> mSGNL [< 'sTR a >]) (get_load_path())
end;
(try
(match create_entry (get_univ "nat") "number" ETast with
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index a5f44847b9..409f5eb368 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -9,7 +9,7 @@ open Tacticals;;
open Hipattern;;
open Pattern;;
open Reduction;;
-open Coqast;;
+open Ctast;;
open Rawterm;;
open Environ;;
@@ -38,8 +38,8 @@ type pbp_rule = (identifier list *
(identifier list ->
string list ->
bool ->
- string option -> (types, constr) kind_of_term -> int list -> Coqast.t)) ->
- Coqast.t option;;
+ string option -> (types, constr) kind_of_term -> int list -> Ctast.t)) ->
+ Ctast.t option;;
let zz = (0,0);;
@@ -176,7 +176,7 @@ let (imply_elim2: pbp_rule) = function
| _ -> None;;
let reference dir s =
- let dir = "Coq"::"Init"::[dir] in
+ let dir = List.map id_of_string ("Coq"::"Init"::[dir]) in
let id = id_of_string s in
try
Nametab.locate_in_absolute_module dir id
diff --git a/contrib/interface/pbp.mli b/contrib/interface/pbp.mli
index 6499540198..57794ec229 100644
--- a/contrib/interface/pbp.mli
+++ b/contrib/interface/pbp.mli
@@ -1,4 +1,4 @@
-val pbp_tac : (Coqast.t -> 'a) ->
+val pbp_tac : (Ctast.t -> 'a) ->
Proof_type.tactic_arg list ->
Proof_type.goal Tacmach.sigma ->
Proof_type.goal list Proof_type.sigma * Proof_type.validation;;
diff --git a/contrib/interface/translate.ml b/contrib/interface/translate.ml
index d40fee26a6..75cd7db387 100644
--- a/contrib/interface/translate.ml
+++ b/contrib/interface/translate.ml
@@ -16,7 +16,7 @@ open Evd;;
open Evarutil;;
open Xlate;;
-open Coqast;;
+open Ctast;;
open Vtp;;
open Ascent;;
open Environ;;
@@ -111,7 +111,7 @@ let rec discard_coercions =
let translate_constr assumptions c =
let com = ast_of_constr true assumptions c in
(* dead code: let rcom = relativize_cci (discard_coercions com) in *)
- xlate_formula com (* dead code: rcom *);;
+ xlate_formula (Ctast.ast_to_ct com) (* dead code: rcom *);;
(*translates a named_context into a centaur-tree --> PREMISES_LIST *)
(* this code is inspired from printer.ml (function pr_named_context_of) *)
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 63ef38e4f5..ccaa08f506 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -6,14 +6,14 @@ open Char;;
open Util;;
open Ast;;
open Names;;
+open Ctast;;
open Ascent;;
-open Coqast;;
let in_coq_ref = ref false;;
let xlate_mut_stuff = ref ((fun _ ->
Nvar((0,0), "function xlate_mut_stuff should not be used here")):
- Coqast.t -> Coqast.t);;
+ Ctast.t -> Ctast.t);;
let set_xlate_mut_stuff v = xlate_mut_stuff := v;;
@@ -383,10 +383,10 @@ let xlate_op the_node opn a b =
(match a, b with
| ((Path (_, sl, kind)) :: []), [] ->
CT_coerce_ID_to_FORMULA(CT_ident
- (Names.string_of_id (Names.basename (Ast.section_path sl kind))))
+ (Names.string_of_id (Names.basename (section_path sl kind))))
| ((Path (_, sl, kind)) :: []), tl ->
CT_coerce_ID_to_FORMULA(CT_ident
- (Names.string_of_id(Names.basename (Ast.section_path sl kind))))
+ (Names.string_of_id(Names.basename (section_path sl kind))))
| _, _ -> xlate_error "xlate_op : CONST")
| (** string_of_path needs to be investigated.
*)
@@ -402,7 +402,7 @@ let xlate_op the_node opn a b =
CT_coerce_ID_to_FORMULA(
CT_ident(Names.string_of_id
(Names.basename
- (Ast.section_path sl kind))))
+ (section_path sl kind))))
| _, _ -> xlate_error "xlate_op : MUTIND")
| "MUTCASE"
| "CASE" ->
@@ -425,7 +425,7 @@ let xlate_op the_node opn a b =
| Some(Rform x) -> x
| _ -> assert false
else
- let name = Names.string_of_path (Ast.section_path sl kind) in
+ let name = Names.string_of_path (section_path sl kind) in
(* This is rather a patch to cope with the fact that identifier
names have disappeared from the vo files for grammar rules *)
let type_desc = (try Some (Hashtbl.find type_table name) with
@@ -1372,7 +1372,7 @@ and xlate_tac =
CT_user_tac (id, CT_targ_list (List.map coerce_iTARG_to_TARG l))
| s, l ->
CT_user_tac (CT_ident s, CT_targ_list (List.map coerce_iTARG_to_TARG l))
-and (xlate_context_rule: Coqast.t -> ct_CONTEXT_RULE) =
+and (xlate_context_rule: Ctast.t -> ct_CONTEXT_RULE) =
function
| Node(_, "MATCHCONTEXTRULE", parts) ->
let rec xlate_ctxt_rule_aux = function
diff --git a/contrib/interface/xlate.mli b/contrib/interface/xlate.mli
index 5613dd0952..b93635e473 100644
--- a/contrib/interface/xlate.mli
+++ b/contrib/interface/xlate.mli
@@ -1,14 +1,14 @@
open Ascent;;
-val xlate_vernac : Coqast.t -> ct_COMMAND;;
-val xlate_tactic : Coqast.t -> ct_TACTIC_COM;;
-val xlate_formula : Coqast.t -> ct_FORMULA;;
-val xlate_int : Coqast.t -> ct_INT;;
-val xlate_string : Coqast.t -> ct_STRING;;
-val xlate_id : Coqast.t -> ct_ID;;
-val xlate_vernac_list : Coqast.t -> ct_COMMAND_LIST;;
+val xlate_vernac : Ctast.t -> ct_COMMAND;;
+val xlate_tactic : Ctast.t -> ct_TACTIC_COM;;
+val xlate_formula : Ctast.t -> ct_FORMULA;;
+val xlate_int : Ctast.t -> ct_INT;;
+val xlate_string : Ctast.t -> ct_STRING;;
+val xlate_id : Ctast.t -> ct_ID;;
+val xlate_vernac_list : Ctast.t -> ct_COMMAND_LIST;;
val g_nat_syntax_flag : bool ref;;
val set_flags : (unit -> unit) ref;;
-val set_xlate_mut_stuff : (Coqast.t -> Coqast.t) -> unit;;
+val set_xlate_mut_stuff : (Ctast.t -> Ctast.t) -> unit;;
val declare_in_coq : (unit -> unit);;
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 00:42:27 +0000