diff options
| author | Pierre-Marie Pédrot | 2020-04-28 16:21:33 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-04-28 16:31:43 +0200 |
| commit | 3ff3c18031317dcd08bf081e55212617b8820647 (patch) | |
| tree | 420126181a1158afda19a649e388e306f41d723c /plugins | |
| parent | 2c04f5df480492169e533c376cc50caff863ba5a (diff) | |
Return an option in lookup_scheme.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/rewrite.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index f002bbc57a..3834b21a14 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -952,10 +952,11 @@ let fold_match env sigma c = then case_dep_scheme_kind_from_type else case_scheme_kind_from_type) in - let exists = Ind_tables.check_scheme sk ci.ci_ind in - if exists then - dep, pred, exists, Ind_tables.lookup_scheme sk ci.ci_ind - else raise Not_found + match Ind_tables.lookup_scheme sk ci.ci_ind with + | Some cst -> + dep, pred, true, cst + | None -> + raise Not_found in let app = let ind, args = Inductiveops.find_mrectype env sigma cty in |