diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-12 16:50:17 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-12 16:59:53 +0200 |
| commit | 5dc8187aa8e6b481338035a022fec4025a25eb33 (patch) | |
| tree | 153dbb1b9dd62a27bc53cb5d1438b457afd04b9d /dev/base_include | |
| parent | 2219309681e03b32d0490690374e7f9f6c92b2f4 (diff) | |
Fix base_include due to change in argument order of env and evar_map
Diffstat (limited to 'dev/base_include')
| -rw-r--r-- | dev/base_include | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/dev/base_include b/dev/base_include index a5ccf24aa..2699551a5 100644 --- a/dev/base_include +++ b/dev/base_include @@ -188,7 +188,7 @@ let e s = Constrintern.intern_constr (Global.env()) (parse_constr s);; implicit syntax *) let constr_of_string s = - Constrintern.interp_constr Evd.empty (Global.env()) (parse_constr s);; + Constrintern.interp_constr (Global.env()) Evd.empty (parse_constr s);; (* get the body of a constant *) @@ -207,7 +207,7 @@ let get_nth_goal n = nth_goal_of_pftreestate n (Pfedit.get_pftreestate ());; let current_goal () = get_nth_goal 1;; *) let pf_e gl s = - Constrintern.interp_constr (project gl) (pf_env gl) (parse_constr s);; + Constrintern.interp_constr (pf_env gl) (project gl) (parse_constr s);; (* Set usual printing since the global env is available from the tracer *) let _ = Constrextern.in_debugger := false |