diff options
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 4 | ||||
| -rw-r--r-- | plugins/ssr/ssripats.ml | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrparser.ml4 | 3 |
3 files changed, 5 insertions, 4 deletions
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index d389f70859..490ded9d4d 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -226,8 +226,8 @@ let isAppInd gl c = let interp_refine ist gl rc = let constrvars = Tacinterp.extract_ltac_constr_values ist (pf_env gl) in - let vars = { Pretyping.empty_lvar with - Pretyping.ltac_constrs = constrvars; ltac_genargs = ist.Tacinterp.lfun + let vars = { Glob_ops.empty_lvar with + Glob_term.ltac_constrs = constrvars; ltac_genargs = ist.Tacinterp.lfun } in let kind = Pretyping.OfType (pf_concl gl) in let flags = { diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index 4a9dddd2ba..7ae9e38248 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -95,7 +95,7 @@ let ssrmkabs id gl = end in Proofview.V82.of_tactic (Proofview.tclTHEN - (Tactics.New.refine step) + (Tactics.New.refine ~typecheck:false step) (Proofview.tclFOCUS 1 3 Proofview.shelve)) gl let ssrmkabstac ids = diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 3ea8c24314..09917339a7 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -346,7 +346,8 @@ let interp_index ist gl idx = | Some c -> let rc = Detyping.detype false [] (pf_env gl) (project gl) c in begin match Notation.uninterp_prim_token rc with - | _, Constrexpr.Numeral bigi -> int_of_string (Bigint.to_string bigi) + | _, Constrexpr.Numeral (s,b) -> + let n = int_of_string s in if b then n else -n | _ -> raise Not_found end | None -> raise Not_found |