From a42795cc1c2a8ed3efa9960af920ff7b16d928f0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 1 Sep 2016 17:52:44 +0200 Subject: Introducing a new EConstr.t type to perform the nf_evar operation on demand. --- dev/db | 1 + dev/top_printers.ml | 1 + 2 files changed, 2 insertions(+) (limited to 'dev') diff --git a/dev/db b/dev/db index d3503ef439..432baf8a62 100644 --- a/dev/db +++ b/dev/db @@ -28,6 +28,7 @@ install_printer Top_printers.pppattern install_printer Top_printers.ppglob_constr install_printer Top_printers.ppconstr +install_printer Top_printers.ppeconstr install_printer Top_printers.ppuni install_printer Top_printers.ppuniverses install_printer Top_printers.ppconstraints diff --git a/dev/top_printers.ml b/dev/top_printers.ml index b552d99949..b7736f4987 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -71,6 +71,7 @@ let ppwf_paths x = pp (Rtree.pp_tree pprecarg x) let rawdebug = ref false let ppevar evk = pp (str (Evd.string_of_existential evk)) let ppconstr x = pp (Termops.print_constr x) +let ppeconstr x = pp (Termops.print_constr (EConstr.Unsafe.to_constr x)) let ppconstr_expr x = pp (Ppconstr.pr_constr_expr x) let ppconstrdb x = pp(Flags.with_option rawdebug Termops.print_constr x) let ppterm = ppconstr -- cgit v1.2.3 From e6a8ab0f428c26fff2bd7e636126974f167101bf Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Nov 2016 01:35:54 +0100 Subject: Tactic_matching API using EConstr. --- dev/top_printers.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'dev') diff --git a/dev/top_printers.ml b/dev/top_printers.ml index b7736f4987..8290ca945f 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -109,7 +109,7 @@ let ppididmap = ppidmap (fun _ -> pr_id) let prconstrunderbindersidmap = pridmap (fun _ (l,c) -> hov 1 (str"[" ++ prlist_with_sep spc Id.print l ++ str"]") - ++ str "," ++ spc () ++ Termops.print_constr c) + ++ str "," ++ spc () ++ Termops.print_constr (EConstr.Unsafe.to_constr c)) let ppconstrunderbindersidmap l = pp (prconstrunderbindersidmap l) -- cgit v1.2.3 From 05afd04095e35d77ca135bd2c1cb8d303ea2d6a8 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 24 Nov 2016 18:18:17 +0100 Subject: Ltac now uses evar-based constrs. --- dev/top_printers.ml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'dev') diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 8290ca945f..04aacdc098 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -70,10 +70,10 @@ let ppwf_paths x = pp (Rtree.pp_tree pprecarg x) (* term printers *) let rawdebug = ref false let ppevar evk = pp (str (Evd.string_of_existential evk)) -let ppconstr x = pp (Termops.print_constr x) -let ppeconstr x = pp (Termops.print_constr (EConstr.Unsafe.to_constr x)) +let ppconstr x = pp (Termops.print_constr (EConstr.of_constr x)) +let ppeconstr x = pp (Termops.print_constr x) let ppconstr_expr x = pp (Ppconstr.pr_constr_expr x) -let ppconstrdb x = pp(Flags.with_option rawdebug Termops.print_constr x) +let ppconstrdb x = pp(Flags.with_option rawdebug Termops.print_constr (EConstr.of_constr x)) let ppterm = ppconstr let ppsconstr x = ppconstr (Mod_subst.force_constr x) let ppconstr_univ x = Constrextern.with_universes ppconstr x @@ -98,9 +98,9 @@ let ppidmap pr l = pp (pridmap pr l) let ppevarsubst = ppidmap (fun id0 -> prset (fun (c,copt,id) -> hov 0 - (Termops.print_constr c ++ + (Termops.print_constr (EConstr.of_constr c) ++ (match copt with None -> mt () | Some c -> spc () ++ str "") ++ + Termops.print_constr (EConstr.of_constr c) ++ str">") ++ (if id = id0 then mt () else spc () ++ str "")))) @@ -109,7 +109,7 @@ let ppididmap = ppidmap (fun _ -> pr_id) let prconstrunderbindersidmap = pridmap (fun _ (l,c) -> hov 1 (str"[" ++ prlist_with_sep spc Id.print l ++ str"]") - ++ str "," ++ spc () ++ Termops.print_constr (EConstr.Unsafe.to_constr c)) + ++ str "," ++ spc () ++ Termops.print_constr c) let ppconstrunderbindersidmap l = pp (prconstrunderbindersidmap l) @@ -159,7 +159,7 @@ let prdelta s = pp (Mod_subst.debug_pr_delta s) let pp_idpred s = pp (pr_idpred s) let pp_cpred s = pp (pr_cpred s) let pp_transparent_state s = pp (pr_transparent_state s) -let pp_stack_t n = pp (Reductionops.Stack.pr Termops.print_constr n) +let pp_stack_t n = pp (Reductionops.Stack.pr (EConstr.of_constr %> Termops.print_constr) n) let pp_cst_stack_t n = pp (Reductionops.Cst_stack.pr n) let pp_state_t n = pp (Reductionops.pr_state n) -- cgit v1.2.3 From 27fbf069ccd846383bcfb35ba1ea5bd1d95090a0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 29 Nov 2016 23:48:28 +0100 Subject: Moving printing code from Evd to Termops. --- dev/top_printers.ml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'dev') diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 04aacdc098..33fc52e205 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -165,9 +165,9 @@ let pp_state_t n = pp (Reductionops.pr_state n) (* proof printers *) let pr_evar ev = Pp.int (Evar.repr ev) -let ppmetas metas = pp(pr_metaset metas) -let ppevm evd = pp(pr_evar_map ~with_univs:!Flags.univ_print (Some 2) evd) -let ppevmall evd = pp(pr_evar_map ~with_univs:!Flags.univ_print None evd) +let ppmetas metas = pp(Termops.pr_metaset metas) +let ppevm evd = pp(Termops.pr_evar_map ~with_univs:!Flags.univ_print (Some 2) evd) +let ppevmall evd = pp(Termops.pr_evar_map ~with_univs:!Flags.univ_print None evd) let pr_existentialset evars = prlist_with_sep spc pr_evar (Evar.Set.elements evars) let ppexistentialset evars = @@ -178,14 +178,14 @@ let ppexistentialfilter filter = match Evd.Filter.repr filter with let ppclenv clenv = pp(pr_clenv clenv) let ppgoalgoal gl = pp(Goal.pr_goal gl) let ppgoal g = pp(Printer.pr_goal g) -let ppgoalsigma g = pp(Printer.pr_goal g ++ pr_evar_map None (Refiner.project g)) +let ppgoalsigma g = pp(Printer.pr_goal g ++ Termops.pr_evar_map None (Refiner.project g)) let pphintdb db = pp(Hints.pr_hint_db db) let ppproofview p = let gls,sigma = Proofview.proofview p in - pp(pr_enum Goal.pr_goal gls ++ fnl () ++ pr_evar_map (Some 1) sigma) + pp(pr_enum Goal.pr_goal gls ++ fnl () ++ Termops.pr_evar_map (Some 1) sigma) let ppopenconstr (x : Evd.open_constr) = - let (evd,c) = x in pp (pr_evar_map (Some 2) evd ++ pr_constr c) + let (evd,c) = x in pp (Termops.pr_evar_map (Some 2) evd ++ pr_constr c) (* spiwack: deactivated until a replacement is found let pppftreestate p = pp(print_pftreestate p) *) @@ -215,7 +215,7 @@ let ppuniverse_context_set l = pp (pr_universe_context_set prlev l) let ppuniverse_subst l = pp (Univ.pr_universe_subst l) let ppuniverse_opt_subst l = pp (Universes.pr_universe_opt_subst l) let ppuniverse_level_subst l = pp (Univ.pr_universe_level_subst l) -let ppevar_universe_context l = pp (Evd.pr_evar_universe_context l) +let ppevar_universe_context l = pp (Termops.pr_evar_universe_context l) let ppconstraints c = pp (pr_constraints Level.pr c) let ppuniverseconstraints c = pp (Universes.Constraints.pr c) let ppuniverse_context_future c = -- cgit v1.2.3 From 98e51078fa624ce780b16d8e372ef33ac97ffaee Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Sat, 25 Mar 2017 00:00:18 +0100 Subject: Mathcomp overlay. --- dev/ci/ci-user-overlay.sh | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'dev') diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh index 0285747432..ab2d2e382c 100644 --- a/dev/ci/ci-user-overlay.sh +++ b/dev/ci/ci-user-overlay.sh @@ -20,3 +20,12 @@ # the name of the branch from which the PR originated. "" if the # current job is a push build. +echo $TRAVIS_PULL_REQUEST_BRANCH +echo $TRAVIS_PULL_REQUEST +echo $TRAVIS_BRANCH +echo $TRAVIS_COMMIT + +if [ $TRAVIS_PULL_REQUEST == "379" ] || [ $TRAVIS_BRANCH == "pr379" ]; then + mathcomp_CI_BRANCH=econstr + mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git +fi -- cgit v1.2.3