diff options
author | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-12-02 08:36:14 +0000 |
---|---|---|
committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-12-02 08:36:14 +0000 |
commit | 3cb4411089c18351d57685f9abe455d3f61f308f (patch) | |
tree | c23e0d757eee079722f4fcc92b37e69c4ff4ef81 /plugins/interface/translate.ml | |
parent | 3e253de6854b139a8a1be76af2388ffa9a3dcdb2 (diff) |
Remove interface plugin
It has moved to the contribs (Sophia-Antipolis/Interface).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12555 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/interface/translate.ml')
-rw-r--r-- | plugins/interface/translate.ml | 80 |
1 files changed, 0 insertions, 80 deletions
diff --git a/plugins/interface/translate.ml b/plugins/interface/translate.ml deleted file mode 100644 index 48f35ebab..000000000 --- a/plugins/interface/translate.ml +++ /dev/null @@ -1,80 +0,0 @@ -open Names;; -open Sign;; -open Util;; -open Term;; -open Pp;; -open Libobject;; -open Library;; -open Vernacinterp;; -open Tacmach;; -open Pfedit;; -open Parsing;; -open Evd;; -open Evarutil;; - -open Xlate;; -open Vtp;; -open Ascent;; -open Environ;; -open Proof_type;; - -(*translates a formula into a centaur-tree --> FORMULA *) -let translate_constr at_top env c = - xlate_formula (Constrextern.extern_constr at_top env c);; - -(*translates a named_context into a centaur-tree --> PREMISES_LIST *) -(* this code is inspired from printer.ml (function pr_named_context_of) *) -let translate_sign env = - let l = - Environ.fold_named_context - (fun env (id,v,c) l -> - (match v with - None -> - CT_premise(CT_ident(string_of_id id), translate_constr false env c) - | Some v1 -> - CT_eval_result - (CT_coerce_ID_to_FORMULA (CT_ident (string_of_id id)), - translate_constr false env v1, - translate_constr false env c))::l) - env ~init:[] - in - CT_premises_list l;; - -(* the function rev_and_compact performs two operations: - 1- it reverses the list of integers given as argument - 2- it replaces sequences of "1" by a negative number that is - the length of the sequence. *) -let rec rev_and_compact l = function - [] -> l - | 1::tl -> - (match l with - n::tl' -> - if n < 0 then - rev_and_compact ((n - 1)::tl') tl - else - rev_and_compact ((-1)::l) tl - | [] -> rev_and_compact [-1] tl) - | a::tl -> - if a < 0 then - (match l with - n::tl' -> - if n < 0 then - rev_and_compact ((n + a)::tl') tl - else - rev_and_compact (a::l) tl - | [] -> rev_and_compact (a::l) tl) - else - rev_and_compact (a::l) tl;; - -(*translates an int list into a centaur-tree --> SIGNED_INT_LIST *) -let translate_path l = - CT_signed_int_list - (List.map (function n -> CT_coerce_INT_to_SIGNED_INT (CT_int n)) - (rev_and_compact [] l));; - -(*translates a path and a goal into a centaur-tree --> RULE *) -let translate_goal (g:goal) = - CT_rule(translate_sign (evar_env g), translate_constr true (evar_env g) g.evar_concl);; - -let translate_goals (gl: goal list) = - CT_rule_list (List.map translate_goal gl);; |