diff options
| author | coqbot-app[bot] | 2020-10-27 12:55:13 +0000 |
|---|---|---|
| committer | GitHub | 2020-10-27 12:55:13 +0000 |
| commit | 5f5cddae48c08872107f30938dcc2f3c8d91f33a (patch) | |
| tree | 2f1bb58c33fee5b4bb0913296ef4341a8832feb4 /plugins/extraction | |
| parent | b87fd6cfe5fe872a38d98c294aea84cde8c6c160 (diff) | |
| parent | 375fc707b402b855770ec32c57ad1362f2a89e5c (diff) | |
Merge PR #13075: Introducing the foundations for a name-alias-agnostic API
Reviewed-by: SkySkimmer
Ack-by: gares
Ack-by: ejgallego
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 |