diff options
| author | Lasse Blaauwbroek | 2020-12-22 06:15:28 +0100 |
|---|---|---|
| committer | Lasse Blaauwbroek | 2020-12-27 18:26:01 +0100 |
| commit | d1af000c4b9b1d1ff9b2f9fbf2dcb570ae7c974c (patch) | |
| tree | 6ee84b6104fdfacab5a63661b8577a079cc72a3e /plugins/ssr/ssrequality.ml | |
| parent | a84ff9806f0ee77e081954453ee6afb67921eb50 (diff) | |
Make ssrtermkind algebraic instead of a char
Diffstat (limited to 'plugins/ssr/ssrequality.ml')
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index fdfba48024..aeb6b3cf85 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -232,7 +232,7 @@ let rec get_evalref env sigma c = match EConstr.kind sigma c with (* Strip a pattern generated by a prenex implicit to its constant. *) let strip_unfold_term _ ((sigma, t) as p) kt = match EConstr.kind sigma t with - | App (f, a) when kt = xNoFlag && Array.for_all (EConstr.isEvar sigma) a && EConstr.isConst sigma f -> + | App (f, a) when kt = NoFlag && Array.for_all (EConstr.isEvar sigma) a && EConstr.isConst sigma f -> (sigma, f), true | Const _ | Var _ -> p, true | Proj _ -> p, true @@ -736,7 +736,7 @@ let unlocktac ist args = Ssrcommon.tacMK_SSR_CONST "locked" >>= fun locked -> Ssrcommon.tacMK_SSR_CONST "master_key" >>= fun key -> let ktacs = [ - (Proofview.tclEVARMAP >>= fun sigma -> unfoldtac None None (sigma, locked) xInParens); + (Proofview.tclEVARMAP >>= fun sigma -> unfoldtac None None (sigma, locked) InParens); Ssrelim.casetac key (fun ?seed:_ k -> k) ] in Tacticals.New.tclTHENLIST (List.map utac args @ ktacs) |