diff options
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 4 | ||||
| -rw-r--r-- | plugins/ssr/ssrelim.ml | 11 | ||||
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrparser.mlg | 8 | ||||
| -rw-r--r-- | plugins/ssr/ssrvernac.mlg | 2 |
5 files changed, 16 insertions, 11 deletions
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 1b7768852e..d859fe51ab 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -1047,7 +1047,7 @@ let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc = let uct = Evd.evar_universe_context (fst oc) in let n, oc = abs_evars_pirrel env sigma (fst oc, EConstr.to_constr ~abort_on_undefined_evars:false (fst oc) (snd oc)) in Proofview.Unsafe.tclEVARS (Evd.set_universe_context sigma uct) <*> - Proofview.tclOR (applyn ~with_evars ~first_goes_last ~with_shelve:true ?beta n (EConstr.of_constr oc)) + Proofview.tclORELSE (applyn ~with_evars ~first_goes_last ~with_shelve:true ?beta n (EConstr.of_constr oc)) (fun _ -> Proofview.tclZERO dependent_apply_error) end @@ -1352,7 +1352,7 @@ let unsafe_intro env decl b = Refine.refine ~typecheck:false begin fun sigma -> let ctx = Environ.named_context_val env in let nctx = EConstr.push_named_context_val decl ctx in - let inst = List.map (get_id %> EConstr.mkVar) (Environ.named_context env) in + let inst = EConstr.identity_subst_val (Environ.named_context_val env) in let ninst = EConstr.mkRel 1 :: inst in let nb = EConstr.Vars.subst1 (EConstr.mkVar (get_id decl)) b in let sigma, ev = Evarutil.new_pure_evar ~principal:true nctx sigma nb in diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 1e182b52fa..582c45cde1 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -478,11 +478,16 @@ let revtoptac n0 = Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let concl = Proofview.Goal.concl gl in + let env = Proofview.Goal.env gl in let n = nb_prod sigma concl - n0 in let dc, cl = EConstr.decompose_prod_n_assum sigma n concl in - let dc' = dc @ [Context.Rel.Declaration.LocalAssum(make_annot (Name rev_id) Sorts.Relevant, EConstr.it_mkProd_or_LetIn cl (List.rev dc))] in - let f = EConstr.it_mkLambda_or_LetIn (mkEtaApp (EConstr.mkRel (n + 1)) (-n) 1) dc' in - Logic.refiner ~check:true EConstr.Unsafe.(to_constr (EConstr.mkApp (f, [|Evarutil.mk_new_meta ()|]))) + let ty = EConstr.it_mkProd_or_LetIn cl (List.rev dc) in + let dc' = dc @ [Context.Rel.Declaration.LocalAssum(make_annot (Name rev_id) Sorts.Relevant, ty)] in + Refine.refine ~typecheck:true begin fun sigma -> + let f = EConstr.it_mkLambda_or_LetIn (mkEtaApp (EConstr.mkRel (n + 1)) (-n) 1) dc' in + let sigma, ev = Evarutil.new_evar env sigma ty in + sigma, (EConstr.mkApp (f, [|ev|])) + end end let nothing_to_inject = diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index da623703a2..38b26d06b9 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -465,7 +465,7 @@ let rwcltac ?under ?map_redex cl rdx dir sr = Tactics.apply_type ~typecheck:true cl'' [rdx; EConstr.it_mkLambda_or_LetIn r3 dc], Tacticals.New.tclTHENLIST (itacs @ rwtacs), sigma0 in let cvtac' = - Proofview.tclOR cvtac begin function + Proofview.tclORELSE cvtac begin function | (PRtype_error e, _) -> let error = Option.cata (fun (env, sigma, te) -> Pp.(fnl () ++ str "Type error was: " ++ Himsg.explain_pretype_error env sigma te)) diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 60af804c1b..98439e27a1 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -219,20 +219,20 @@ let test_ssrslashnum b1 b2 _ strm = match Util.stream_nth 0 strm with | Tok.KEYWORD "/" -> (match Util.stream_nth 1 strm with - | Tok.NUMERAL _ when b1 -> + | Tok.NUMBER _ when b1 -> (match Util.stream_nth 2 strm with | Tok.KEYWORD "=" | Tok.KEYWORD "/=" when not b2 -> () | Tok.KEYWORD "/" -> if not b2 then () else begin match Util.stream_nth 3 strm with - | Tok.NUMERAL _ -> () + | Tok.NUMBER _ -> () | _ -> raise Stream.Failure end | _ -> raise Stream.Failure) | Tok.KEYWORD "/" when not b1 -> (match Util.stream_nth 2 strm with | Tok.KEYWORD "=" when not b2 -> () - | Tok.NUMERAL _ when b2 -> + | Tok.NUMBER _ when b2 -> (match Util.stream_nth 3 strm with | Tok.KEYWORD "=" -> () | _ -> raise Stream.Failure) @@ -243,7 +243,7 @@ let test_ssrslashnum b1 b2 _ strm = | Tok.KEYWORD "//" when not b1 -> (match Util.stream_nth 1 strm with | Tok.KEYWORD "=" when not b2 -> () - | Tok.NUMERAL _ when b2 -> + | Tok.NUMBER _ when b2 -> (match Util.stream_nth 2 strm with | Tok.KEYWORD "=" -> () | _ -> raise Stream.Failure) diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index 24772a8514..4a907b2795 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -159,7 +159,7 @@ let declare_one_prenex_implicit locality f = | [] -> errorstrm (str "Expected some implicits for " ++ pr_qualid f) | impls -> - Impargs.set_implicits locality fref [impls] + Impargs.set_implicits locality fref [List.map (fun imp -> (Anonymous,imp)) impls] } |