aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorherbelin2000-04-30 00:51:02 +0000
committerherbelin2000-04-30 00:51:02 +0000
commit35ae98e0426b6ea0abb1fee30856b38fecb4d35a (patch)
tree86bfeba90676aafb35d7978b5852a7647a8caa1d
parent00b32058d81c38d94b5333765291004034efa3f7 (diff)
MODIFS pour compatibilité aussi 2.99
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@391 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--contrib/omega/coq_omega.ml4
-rwxr-xr-xcontrib/omega/omega.ml6
2 files changed, 5 insertions, 5 deletions
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index 9fb2f918b1..f57a17f30e 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -424,7 +424,7 @@ type constr_path =
| P_ARITY
| P_ARG
-let context operation path (t:constr) =
+let context operation path (t : constr) =
let rec loop i p0 p1 =
match (p0,p1) with
| (p, (DOP2(Cast,c,t))) -> DOP2(Cast,loop i p c,t)
@@ -460,7 +460,7 @@ let context operation path (t:constr) =
in
loop 1 path t
-let occurence path (t:constr) =
+let occurence path (t : constr) =
let rec loop p0 p1 = match (p0,p1) with
| (p, (DOP2(Cast,c,t))) -> loop p c
| ([], t) -> t
diff --git a/contrib/omega/omega.ml b/contrib/omega/omega.ml
index c06a4cb8cc..86f1a2e334 100755
--- a/contrib/omega/omega.ml
+++ b/contrib/omega/omega.ml
@@ -87,7 +87,7 @@ exception NO_CONTRADICTION
let intern_id,unintern_id =
let cpt = ref 0 in
let table = create 7 and co_table = create 7 in
- (fun (name:string) ->
+ (fun (name : string) ->
try find table name with Not_found ->
let idx = !cpt in
add table name idx; add co_table idx name; incr cpt; idx),
@@ -197,13 +197,13 @@ let rec display_action = function
let add_event, history, clear_history =
let accu = ref [] in
- (fun (v:action) -> if !debug then display_action [v]; push v accu),
+ (fun (v : action) -> if !debug then display_action [v]; push v accu),
(fun () -> !accu),
(fun () -> accu := [])
let nf_linear = Sort.list (fun x y -> x.v > y.v)
-let nf ((b:bool),(e,(x:int))) = (b,(nf_linear e,x))
+let nf ((b : bool),(e,(x : int))) = (b,(nf_linear e,x))
let map_eq_linear f =
let rec loop = function