diff options
| author | Maxime Dénès | 2017-09-07 12:44:47 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-09-07 12:44:47 +0200 |
| commit | 084ef41c98d52078f85831c940d0a073a4ccdb7a (patch) | |
| tree | f1808d72e562f0dd674759f2f447f44cd5da9aad /plugins/ssr/ssrequality.ml | |
| parent | 276f08cb053eed175478c4c9359e61fb949742ba (diff) | |
| parent | 1db568d3dc88d538f975377bb4d8d3eecd87872c (diff) | |
Merge PR #914: Making the detyper lazy
Diffstat (limited to 'plugins/ssr/ssrequality.ml')
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index ab6a60f4ee..8b69c3435a 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -129,7 +129,7 @@ let newssrcongrtac arg ist gl = let eq, gl = pf_fresh_global (Coqlib.build_coq_eq ()) gl in pf_saturate gl (EConstr.of_constr eq) 3 in tclMATCH_GOAL (equality, gl') (fun gl' -> fs gl' (List.assoc 0 eq_args)) - (fun ty -> congrtac (arg, Detyping.detype false [] (pf_env gl) (project gl) ty) ist) + (fun ty -> congrtac (arg, Detyping.detype Detyping.Now false [] (pf_env gl) (project gl) ty) ist) (fun () -> let lhs, gl' = mk_evar gl EConstr.mkProp in let rhs, gl' = mk_evar gl' EConstr.mkProp in let arrow = EConstr.mkArrow lhs (EConstr.Vars.lift 1 rhs) in |