diff options
| author | Pierre-Marie Pédrot | 2019-12-10 09:44:08 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-12-10 10:53:54 +0100 |
| commit | 5ccf803a86bc46d67038f4d33d26d5c9e899027f (patch) | |
| tree | 45fc5c34c1054ad7c5cf7989642911b784217223 /plugins | |
| parent | 50221b84f6af681f69e8f9847a851329a4662509 (diff) | |
Side-effect free wrapper around already declared schemes.
Some calls are actually guarded by a check that the scheme is already in
the cache. There is no reason to generate dummy side-effects in that case.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/rewrite.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 2998e1c767..ca5c8b30c2 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -924,10 +924,10 @@ let reset_env env = let env' = Global.env_of_context (Environ.named_context_val env) in Environ.push_rel_context (Environ.rel_context env) env' -let fold_match ?(force=false) env sigma c = +let fold_match env sigma c = let (ci, p, c, brs) = destCase sigma c in let cty = Retyping.get_type_of env sigma c in - let dep, pred, exists, (sk,eff) = + let dep, pred, exists, sk = let env', ctx, body = let ctx, pred = decompose_lam_assum sigma p in let env' = push_rel_context ctx env in @@ -954,8 +954,8 @@ let fold_match ?(force=false) env sigma c = else case_scheme_kind_from_type) in let exists = Ind_tables.check_scheme sk ci.ci_ind in - if exists || force then - dep, pred, exists, Ind_tables.find_scheme sk ci.ci_ind + if exists then + dep, pred, exists, Ind_tables.lookup_scheme sk ci.ci_ind else raise Not_found in let app = @@ -964,7 +964,7 @@ let fold_match ?(force=false) env sigma c = let meths = List.map (fun br -> br) (Array.to_list brs) in applist (mkConst sk, pars @ [pred] @ meths @ args @ [c]) in - sk, (if exists then env else reset_env env), app, eff + sk, (if exists then env else reset_env env), app let unfold_match env sigma sk app = match EConstr.kind sigma app with @@ -1222,7 +1222,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = else match try Some (fold_match env (goalevars evars) t) with Not_found -> None with | None -> state, c' - | Some (cst, _, t', eff (*FIXME*)) -> + | Some (cst, _, t') -> let state, res = aux { state ; env ; unfresh ; term1 = t' ; ty1 = ty ; cstr = (prop,cstr) ; evars } in |