diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/checker_printers.ml | 4 | ||||
| -rw-r--r-- | dev/checker_printers.mli | 4 | ||||
| -rw-r--r-- | dev/ocamldebug-coq.run | 58 |
3 files changed, 21 insertions, 45 deletions
diff --git a/dev/checker_printers.ml b/dev/checker_printers.ml index 40ae1a7b05..4f89bbd34e 100644 --- a/dev/checker_printers.ml +++ b/dev/checker_printers.ml @@ -59,15 +59,11 @@ let pP s = pp (hov 0 s) let ppuni u = pp(Universe.pr u) let ppuni_level u = pp (Level.pr u) -let ppuniverse_set l = pp (LSet.pr l) -let ppuniverse_instance l = pp (Instance.pr l) -let ppauniverse_context l = pp (AUContext.pr Level.pr l) let ppuniverse_context l = pp (pr_universe_context Level.pr l) let ppconstraints c = pp (pr_constraints Level.pr c) let ppuniverse_context_future c = let ctx = Future.force c in ppuniverse_context ctx -let ppuniverses u = pp (Univ.pr_universes u) let pploc x = let (l,r) = Loc.unloc x in print_string"(";print_int l;print_string",";print_int r;print_string")" diff --git a/dev/checker_printers.mli b/dev/checker_printers.mli index 2f9500c5c3..8be9b87257 100644 --- a/dev/checker_printers.mli +++ b/dev/checker_printers.mli @@ -43,12 +43,8 @@ val ppididmap : Names.Id.t Names.Id.Map.t -> unit (* Universes *) val ppuni : Univ.Universe.t -> unit val ppuni_level : Univ.Level.t -> unit (* raw *) -val ppuniverse_set : Univ.LSet.t -> unit -val ppuniverse_instance : Univ.Instance.t -> unit -val ppauniverse_context : Univ.AUContext.t -> unit val ppuniverse_context : Univ.UContext.t -> unit val ppconstraints : Univ.Constraint.t -> unit val ppuniverse_context_future : Univ.UContext.t Future.computation -> unit -val ppuniverses : Univ.universes -> unit val pploc : Loc.t -> unit diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run index 85bb04efe0..d330f517be 100644 --- a/dev/ocamldebug-coq.run +++ b/dev/ocamldebug-coq.run @@ -14,40 +14,24 @@ export CAML_LD_LIBRARY_PATH=$COQTOP/kernel/byterun:$CAML_LD_LIBRARY_PATH -GUESS_CHECKER= -for arg in "$@"; do - if [ "${arg##*/}" = coqchk.byte ]; then - GUESS_CHECKER=1 - fi -done - -if [ -z "$GUESS_CHECKER" ]; then - exec $OCAMLDEBUG \ - -I $CAMLP5LIB -I +threads \ - -I $COQTOP \ - -I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar -I $COQTOP/clib \ - -I $COQTOP/lib -I $COQTOP/kernel -I $COQTOP/kernel/byterun \ - -I $COQTOP/library -I $COQTOP/engine \ - -I $COQTOP/pretyping -I $COQTOP/parsing -I $COQTOP/vernac \ - -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics -I $COQTOP/stm \ - -I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config -I $COQTOP/ltac \ - -I $COQTOP/plugins/cc -I $COQTOP/plugins/dp \ - -I $COQTOP/plugins/extraction -I $COQTOP/plugins/field \ - -I $COQTOP/plugins/firstorder \ - -I $COQTOP/plugins/funind -I $COQTOP/plugins/groebner \ - -I $COQTOP/plugins/interface -I $COQTOP/plugins/micromega \ - -I $COQTOP/plugins/omega -I $COQTOP/plugins/quote \ - -I $COQTOP/plugins/ring \ - -I $COQTOP/plugins/rtauto -I $COQTOP/plugins/setoid_ring \ - -I $COQTOP/plugins/subtac -I $COQTOP/plugins/syntax \ - -I $COQTOP/plugins/xml -I $COQTOP/plugins/ltac \ - -I $COQTOP/ide \ - "$@" -else - exec $OCAMLDEBUG \ - -I $CAMLP5LIB -I +threads \ - -I $COQTOP \ - -I $COQTOP/config -I $COQTOP/clib \ - -I $COQTOP/lib -I $COQTOP/checker \ - "$@" -fi +exec $OCAMLDEBUG \ + -I $CAMLP5LIB -I +threads \ + -I $COQTOP \ + -I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar -I $COQTOP/clib \ + -I $COQTOP/lib -I $COQTOP/kernel -I $COQTOP/kernel/byterun \ + -I $COQTOP/library -I $COQTOP/engine \ + -I $COQTOP/pretyping -I $COQTOP/parsing -I $COQTOP/vernac \ + -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics -I $COQTOP/stm \ + -I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config -I $COQTOP/ltac \ + -I $COQTOP/plugins/cc -I $COQTOP/plugins/dp \ + -I $COQTOP/plugins/extraction -I $COQTOP/plugins/field \ + -I $COQTOP/plugins/firstorder \ + -I $COQTOP/plugins/funind -I $COQTOP/plugins/groebner \ + -I $COQTOP/plugins/interface -I $COQTOP/plugins/micromega \ + -I $COQTOP/plugins/omega -I $COQTOP/plugins/quote \ + -I $COQTOP/plugins/ring \ + -I $COQTOP/plugins/rtauto -I $COQTOP/plugins/setoid_ring \ + -I $COQTOP/plugins/subtac -I $COQTOP/plugins/syntax \ + -I $COQTOP/plugins/xml -I $COQTOP/plugins/ltac \ + -I $COQTOP/ide \ + "$@" |