diff options
| author | coqbot-app[bot] | 2020-12-27 20:26:35 +0000 |
|---|---|---|
| committer | GitHub | 2020-12-27 20:26:35 +0000 |
| commit | 52154bfa574b30c10a9fbd78584cca44b885dc60 (patch) | |
| tree | e1fc2cbc6182543b8a8b22b7b12c17238da617f3 /plugins/ssr/ssrequality.ml | |
| parent | bcb2f4709412174718440d477b2321e5dc02a4c6 (diff) | |
| parent | 857f8403fcd216d28bf06d18c2774887ccf8bda5 (diff) | |
Merge PR #13659: Make ssr datastructures cpattern and rpattern public
Reviewed-by: gares
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) |