diff options
| author | Emilio Jesus Gallego Arias | 2020-04-28 18:33:00 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-04-28 18:33:00 +0200 |
| commit | 16559843925f3489b61920ff398680f10f1f00cc (patch) | |
| tree | 2b2edeef6c6e5256e445e7945806ae066c7a3dda /plugins | |
| parent | 196b5e0d10db966529b3bd1d27014a9742c71d7c (diff) | |
| parent | 17a5e95cd38206d82a1ff83c1d155a9a26729495 (diff) | |
Merge PR #12164: Stop relying on side-effects for recursive scheme declaration
Reviewed-by: ejgallego
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 |