diff options
| -rw-r--r-- | contrib/funind/rawterm_to_relation.ml | 2 | ||||
| -rw-r--r-- | contrib/funind/rawtermops.ml | 7 | ||||
| -rw-r--r-- | contrib/funind/rawtermops.mli | 4 |
3 files changed, 10 insertions, 3 deletions
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml index 6b3590dd6e..e7914d7d65 100644 --- a/contrib/funind/rawterm_to_relation.ml +++ b/contrib/funind/rawterm_to_relation.ml @@ -122,7 +122,7 @@ let rec change_vars_in_binder mapping = function | (bt,t)::l -> let new_mapping = List.fold_right Idmap.remove (ids_of_binder bt) mapping in (bt,change_vars mapping t):: - (if Idmap.is_empty new_mapping + (if idmap_is_empty new_mapping then l else change_vars_in_binder new_mapping l ) diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml index f5eda3a7bf..2684a8f114 100644 --- a/contrib/funind/rawtermops.ml +++ b/contrib/funind/rawtermops.ml @@ -2,6 +2,9 @@ open Pp open Rawterm open Util open Names +(* Ocaml 3.06 Map.S does not handle is_empty *) +let idmap_is_empty m = m = Idmap.empty + (* Some basic functions to rebuild rawconstr In each of them the location is Util.dummy_loc @@ -129,7 +132,7 @@ let change_vars = | RDynamic _ -> error "Not handled RDynamic" and change_vars_br mapping ((loc,idl,patl,res) as br) = let new_mapping = List.fold_right Idmap.remove idl mapping in - if Idmap.is_empty new_mapping + if idmap_is_empty new_mapping then br else (loc,idl,patl,change_vars new_mapping res) in @@ -278,7 +281,7 @@ let rec alpha_rt excluded rt = in let new_nal = List.rev rev_new_nal in let new_rto,new_t,new_b = - if Idmap.is_empty mapping + if idmap_is_empty mapping then rto,t,b else let replace = change_vars mapping in (option_app replace rto,replace t,replace b) diff --git a/contrib/funind/rawtermops.mli b/contrib/funind/rawtermops.mli index f4bf64613c..ecb59a87f5 100644 --- a/contrib/funind/rawtermops.mli +++ b/contrib/funind/rawtermops.mli @@ -1,5 +1,9 @@ open Rawterm +(* Ocaml 3.06 Map.S does not handle is_empty *) +val idmap_is_empty : 'a Names.Idmap.t -> bool + + (* [get_pattern_id pat] returns a list of all the variable appearing in [pat] *) val get_pattern_id : cases_pattern -> Names.identifier list |