(* *)
(***************************************************************************)
-let use_stylesheets = ref false;;(* false performs the transformations in OCaml*)
-
(* List utility functions *)
exception Skip;;
method load_sequent metasenv sequent =
(**** SIAM QUI ****)
let sequent_mml,(ids_to_terms,ids_to_father_ids,ids_to_hypotheses) =
- if !use_stylesheets then
- ApplyStylesheets.mml_of_cic_sequent metasenv sequent
- else
- ApplyTransformation.mml_of_cic_sequent metasenv sequent
+ ChosenTransformer.mml_of_cic_sequent metasenv sequent
in
self#load_doc ~dom:sequent_mml ;
(*
= Cic2acic.acic_object_of_cic_object currentproof
in
let mml =
- if !use_stylesheets then
- ApplyStylesheets.mml_of_cic_object
- ~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types
- else
- ApplyTransformation.mml_of_cic_object
- ~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types in
+ ChosenTransformer.mml_of_cic_object
+ ~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types
+ in
current_infos <-
Some
(ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses);