diff options
| author | herbelin | 2000-04-30 00:51:02 +0000 |
|---|---|---|
| committer | herbelin | 2000-04-30 00:51:02 +0000 |
| commit | 35ae98e0426b6ea0abb1fee30856b38fecb4d35a (patch) | |
| tree | 86bfeba90676aafb35d7978b5852a7647a8caa1d | |
| parent | 00b32058d81c38d94b5333765291004034efa3f7 (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.ml | 4 | ||||
| -rwxr-xr-x | contrib/omega/omega.ml | 6 |
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 |
