diff options
| author | Hugo Herbelin | 2019-05-11 00:21:22 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-05-11 00:21:22 +0200 |
| commit | 1fb2819d57d16196fd8dc7cb49e72b9e1d22758e (patch) | |
| tree | cef9145a06a6d9e79626ca05471ac9dd4aa89dc6 /plugins/ssr/ssrequality.ml | |
| parent | 2f2658c5a318fb8a8c00caf4d1aca9fbc2d060d0 (diff) | |
| parent | 1b4c0a1e52286d4957f6c79c8ff14868a6f3e838 (diff) | |
Merge PR #10052: Cleanup the hypothesis conversion function
Reviewed-by: herbelin
Diffstat (limited to 'plugins/ssr/ssrequality.ml')
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index ad20113320..e349031952 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -118,7 +118,7 @@ let newssrcongrtac arg ist gl = match try Some (pf_unify_HO gl_c (pf_concl gl) c) with exn when CErrors.noncritical exn -> None with | Some gl_c -> - tclTHEN (Proofview.V82.of_tactic (convert_concl (fs gl_c c))) + tclTHEN (Proofview.V82.of_tactic (convert_concl ~check:true (fs gl_c c))) (t_ok (proj gl_c)) gl | None -> t_fail () gl in let mk_evar gl ty = @@ -276,7 +276,7 @@ let unfoldintac occ rdx t (kt,_) gl = try beta env0 (EConstr.of_constr (eval_pattern env0 sigma0 concl0 rdx occ unfold)) with Option.IsNone -> errorstrm Pp.(str"Failed to unfold " ++ pr_econstr_pat env0 sigma t) in let _ = conclude () in - Proofview.V82.of_tactic (convert_concl concl) gl + Proofview.V82.of_tactic (convert_concl ~check:true concl) gl ;; let foldtac occ rdx ft gl = @@ -303,7 +303,7 @@ let foldtac occ rdx ft gl = let concl0 = EConstr.Unsafe.to_constr concl0 in let concl = eval_pattern env0 sigma0 concl0 rdx occ fold in let _ = conclude () in - Proofview.V82.of_tactic (convert_concl (EConstr.of_constr concl)) gl + Proofview.V82.of_tactic (convert_concl ~check:true (EConstr.of_constr concl)) gl ;; let converse_dir = function L2R -> R2L | R2L -> L2R @@ -406,7 +406,7 @@ let rwcltac ?under ?map_redex cl rdx dir sr gl = let cl' = EConstr.mkApp (EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdxt cl, [|rdx|]) in let sigma, _ = Typing.type_of env sigma cl' in let gl = pf_merge_uc_of sigma gl in - Proofview.V82.of_tactic (convert_concl cl'), rewritetac ?under dir r', gl + Proofview.V82.of_tactic (convert_concl ~check:true cl'), rewritetac ?under dir r', gl else let dc, r2 = EConstr.decompose_lam_n_assum (project gl) n r' in let r3, _, r3t = @@ -644,7 +644,7 @@ let unfoldtac occ ko t kt gl = let cl' = EConstr.Vars.subst1 (pf_unfoldn [OnlyOccurrences [1], get_evalref env (project gl) c] gl c) cl in let f = if ko = None then CClosure.betaiotazeta else CClosure.betaiota in Proofview.V82.of_tactic - (convert_concl (pf_reduce (Reductionops.clos_norm_flags f) gl cl')) gl + (convert_concl ~check:true (pf_reduce (Reductionops.clos_norm_flags f) gl cl')) gl let unlocktac ist args gl = let utac (occ, gt) gl = |