diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-17 15:58:14 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-17 15:58:14 +0000 |
| commit | 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 (patch) | |
| tree | 961cc88c714aa91a0276ea9fbf8bc53b2b9d5c28 /plugins/interface/translate.ml | |
| parent | 6d3fbdf36c6a47b49c2a4b16f498972c93c07574 (diff) | |
Delete trailing whitespaces in all *.{v,ml*} files
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/interface/translate.ml')
| -rw-r--r-- | plugins/interface/translate.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/plugins/interface/translate.ml b/plugins/interface/translate.ml index 559860b2f..48f35ebab 100644 --- a/plugins/interface/translate.ml +++ b/plugins/interface/translate.ml @@ -25,9 +25,9 @@ let translate_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 = + let l = Environ.fold_named_context - (fun env (id,v,c) l -> + (fun env (id,v,c) l -> (match v with None -> CT_premise(CT_ident(string_of_id id), translate_constr false env c) @@ -36,19 +36,19 @@ let translate_sign env = (CT_coerce_ID_to_FORMULA (CT_ident (string_of_id id)), translate_constr false env v1, translate_constr false env c))::l) - env ~init:[] + 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 -> + | 1::tl -> (match l with - n::tl' -> + n::tl' -> if n < 0 then rev_and_compact ((n - 1)::tl') tl else |