diff options
Diffstat (limited to 'plugins/extraction')
| -rw-r--r-- | plugins/extraction/extraction.ml | 2 | ||||
| -rw-r--r-- | plugins/extraction/mlutil.ml | 2 | ||||
| -rw-r--r-- | plugins/extraction/table.ml | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 2dca1d5e49..6869f9c47e 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -741,7 +741,7 @@ and extract_cst_app env sg mle mlt kn args = (* Can we instantiate types variables for this constant ? *) (* In Ocaml, inside the definition of this constant, the answer is no. *) let instantiated = - if lang () == Ocaml && List.mem_f Constant.equal kn !current_fixpoints + if lang () == Ocaml && List.mem_f Constant.CanOrd.equal kn !current_fixpoints then var2var' (snd schema) else instantiation schema in diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index b1ce10985a..21ec80abbc 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -685,7 +685,7 @@ let is_regular_match br = | _ -> raise Impossible in let is_ref i tr = match get_r tr with - | GlobRef.ConstructRef (ind', j) -> eq_ind ind ind' && Int.equal j (i + 1) + | GlobRef.ConstructRef (ind', j) -> Ind.CanOrd.equal ind ind' && Int.equal j (i + 1) | _ -> false in Array.for_all_i is_ref 0 br diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index f8449bcda1..e56d66ca2d 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -32,7 +32,7 @@ module Refset' = GlobRef.Set_env let occur_kn_in_ref kn = let open GlobRef in function | IndRef (kn',_) - | ConstructRef ((kn',_),_) -> MutInd.equal kn kn' + | ConstructRef ((kn',_),_) -> MutInd.CanOrd.equal kn kn' | ConstRef _ | VarRef _ -> false let repr_of_r = let open GlobRef in function |