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/funind/glob_term_to_relation.ml | |
| 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/funind/glob_term_to_relation.ml')
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 6ed61043f9..767a9ec39b 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -332,7 +332,7 @@ let add_pat_variables sigma pat typ env : Environ.env = let constructors = Inductiveops.get_constructors env indf in let constructor : Inductiveops.constructor_summary = List.find - (fun cs -> eq_constructor c (fst cs.Inductiveops.cs_cstr)) + (fun cs -> Construct.CanOrd.equal c (fst cs.Inductiveops.cs_cstr)) (Array.to_list constructors) in let cs_args_types : types list = @@ -402,7 +402,8 @@ let rec pattern_to_term_and_type env typ = let constructors = Inductiveops.get_constructors env indf in let constructor = List.find - (fun cs -> eq_constructor (fst cs.Inductiveops.cs_cstr) constr) + (fun cs -> + Construct.CanOrd.equal (fst cs.Inductiveops.cs_cstr) constr) (Array.to_list constructors) in let cs_args_types : types list = |