aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-04 16:50:36 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-04 16:50:36 +0100
commitb3a8761790c0905aad8e5d3102fab606fe5e7fd6 (patch)
treece5fbe8cb717bad677ad755e7875413d3e5d0e84 /dev
parent9cd987a07d3792dc200e15c5e792a25a1a99c9c6 (diff)
parent886a9c2fb25e32bd87b3fce38023b3e701134d23 (diff)
Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.
Diffstat (limited to 'dev')
-rw-r--r--dev/base_include5
-rw-r--r--dev/ci/user-overlays/06511-ejgallego-econstr+more_fix.sh7
-rw-r--r--dev/top_printers.ml8
3 files changed, 17 insertions, 3 deletions
diff --git a/dev/base_include b/dev/base_include
index 762662c20..3320a2a94 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -196,7 +196,10 @@ let parse_tac = Pcoq.parse_string Ltac_plugin.Pltac.tactic;;
(* build a term of type glob_constr without type-checking or resolution of
implicit syntax *)
-let e s = Constrintern.intern_constr (Global.env()) (parse_constr s);;
+let e s =
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ Constrintern.intern_constr env sigma (parse_constr s);;
(* build a term of type constr with type-checking and resolution of
implicit syntax *)
diff --git a/dev/ci/user-overlays/06511-ejgallego-econstr+more_fix.sh b/dev/ci/user-overlays/06511-ejgallego-econstr+more_fix.sh
new file mode 100644
index 000000000..4b681909d
--- /dev/null
+++ b/dev/ci/user-overlays/06511-ejgallego-econstr+more_fix.sh
@@ -0,0 +1,7 @@
+ if [ "$CI_PULL_REQUEST" = "6511" ] || [ "$CI_BRANCH" = "econstr+more_fix" ]; then
+ ltac2_CI_BRANCH=econstr+more_fix
+ ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
+
+ Equations_CI_BRANCH=econstr+more_fix
+ Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+fi
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index f99e2593d..2c983fd8d 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -313,6 +313,8 @@ let constr_display csr =
in
pp (str (term_display csr) ++fnl ())
+let econstr_display c = constr_display EConstr.Unsafe.(to_constr c) ;;
+
open Format;;
let print_pure_constr csr =
@@ -452,6 +454,8 @@ let print_pure_constr csr =
print_string (Printexc.to_string e);print_flush ();
raise e
+let print_pure_econstr c = print_pure_constr EConstr.Unsafe.(to_constr c) ;;
+
let pploc x = let (l,r) = Loc.unloc x in
print_string"(";print_int l;print_string",";print_int r;print_string")"
@@ -505,7 +509,7 @@ let _ =
(function
[c] when genarg_tag c = unquote (topwit wit_constr) && true ->
let c = out_gen (rawwit wit_constr) c in
- (fun ~atts ~st -> in_current_context constr_display c; st)
+ (fun ~atts ~st -> in_current_context econstr_display c; st)
| _ -> failwith "Vernac extension: cannot occur")
with
e -> pp (CErrors.print e)
@@ -521,7 +525,7 @@ let _ =
(function
[c] when genarg_tag c = unquote (topwit wit_constr) && true ->
let c = out_gen (rawwit wit_constr) c in
- (fun ~atts ~st -> in_current_context print_pure_constr c; st)
+ (fun ~atts ~st -> in_current_context print_pure_econstr c; st)
| _ -> failwith "Vernac extension: cannot occur")
with
e -> pp (CErrors.print e)