diff options
| author | Maxime Dénès | 2019-03-01 15:27:05 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-03-20 09:33:15 +0100 |
| commit | 27d453641446b3d35aa2211b94f949b57a88ebb2 (patch) | |
| tree | af47b4cb0e3fbb7fde26b6cab3a9b78b99699e94 /plugins/micromega | |
| parent | e5a2f0452cf9523bc86e71ae6d2ac30883a28be6 (diff) | |
Stop accessing proof env via Pfedit in printers
This should make https://github.com/coq/coq/pull/9129 easier.
Diffstat (limited to 'plugins/micromega')
| -rw-r--r-- | plugins/micromega/coq_micromega.ml | 21 |
1 files changed, 9 insertions, 12 deletions
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index ac34faa7da..7db47e13a5 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -877,11 +877,9 @@ struct * This is the big generic function for expression parsers. *) - let parse_expr sigma parse_constant parse_exp ops_spec env term = + let parse_expr cenv sigma parse_constant parse_exp ops_spec env term = if debug - then ( - let _, env = Pfedit.get_current_context () in - Feedback.msg_debug (Pp.str "parse_expr: " ++ Printer.pr_leconstr_env env sigma term)); + then Feedback.msg_debug (Pp.str "parse_expr: " ++ Printer.pr_leconstr_env cenv sigma term); (* let constant_or_variable env term = @@ -1000,8 +998,7 @@ struct | _ -> raise ParseError - let rconstant sigma term = - let _, env = Pfedit.get_current_context () in + let rconstant env sigma term = if debug then Feedback.msg_debug (Pp.str "rconstant: " ++ Printer.pr_leconstr_env env sigma term ++ fnl ()); let res = rconstant sigma term in @@ -1010,7 +1007,7 @@ struct res - let parse_zexpr sigma = parse_expr sigma + let parse_zexpr env sigma = parse_expr env sigma (zconstant sigma) (fun expr x -> let exp = (parse_z sigma x) in @@ -1019,7 +1016,7 @@ struct | _ -> Mc.PEpow(expr, Mc.Z.to_N exp)) zop_spec - let parse_qexpr sigma = parse_expr sigma + let parse_qexpr env sigma = parse_expr env sigma (qconstant sigma) (fun expr x -> let exp = parse_z sigma x in @@ -1034,8 +1031,8 @@ struct Mc.PEpow(expr,exp)) qop_spec - let parse_rexpr sigma = parse_expr sigma - (rconstant sigma) + let parse_rexpr env sigma = parse_expr env sigma + (rconstant env sigma) (fun expr x -> let exp = Mc.N.of_nat (parse_nat sigma x) in Mc.PEpow(expr,exp)) @@ -1048,8 +1045,8 @@ struct match EConstr.kind sigma cstr with | App(op,args) -> let (op,lhs,rhs) = parse_op gl (op,args) in - let (e1,env) = parse_expr sigma env lhs in - let (e2,env) = parse_expr sigma env rhs in + let (e1,env) = parse_expr gl.env sigma env lhs in + let (e2,env) = parse_expr gl.env sigma env rhs in ({Mc.flhs = e1; Mc.fop = op;Mc.frhs = e2},env) | _ -> failwith "error : parse_arith(2)" |