aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernacentries.ml
Commit message (Collapse)AuthorAge
* Better error message for non-existent required libraries with a From prefix.Gravatar Pierre-Marie Pédrot2015-05-13
|
* STM: process_error_hook set in Vernac where fname is known (fix #4229)Gravatar Enrico Tassi2015-05-12
| | | | | | | In compiler mode, only vernac.ml knows the current file name. Stm.process_error_hook moved from Vernacentries to Vernac to be bale to properly enrich the exception with the current file name (if any).
* Add a [Redirect] vernacular commandGravatar Clément Pit--Claudel2015-05-04
| | | | | | | The command [Redirect "filename" (...)] redirects all the output of [(...)] to file "filename.out". This is useful for storing the results of an [Eval compute], for redirecting the results of a large search, for automatically generating traces of interesting developments, and so on.
* Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
| | | | | | Since error messages are ultimately passed to Format, which has its own buffers for concatenating strings, using concatenation for preparing error messages just doubles the workload and increases memory pressure.
* Make "Add LoadPath" behave accordingly to its documentation.Gravatar Guillaume Melquiond2015-04-02
| | | | | "Add LoadPath" is documented as acting as -Q, not as -I-as. Note that "Add Rec LoadPath" should be used when compatibility with 8.4 matters.
* Display the proper error message when Require fails to find a library.Gravatar Guillaume Melquiond2015-04-02
|
* From X Require Y looks for X with absolute path, disregarding -R.Gravatar Pierre-Marie Pédrot2015-04-01
|
* Putting the From parameter of the Require command into the AST.Gravatar Pierre-Marie Pédrot2015-03-27
|
* Load: don't give anomaly on aborted proofs (Close: #3882)Gravatar Enrico Tassi2015-03-23
|
* Do not prepend a "Error:" header when the error is expected by the user.Gravatar Guillaume Melquiond2015-03-05
| | | | | This commit also removes the extraneous "=>" token from Fail messages and prevents them from losing all the formatting information.
* Fixing OCaml 3.12 compilation.Gravatar Pierre-Marie Pédrot2015-02-27
|
* Fixing bug #3249.Gravatar Pierre-Marie Pédrot2015-02-27
| | | | | | | Instead of substituting carelessly the recursive names in Ltac interpretation, we declare them in the environment beforehand, so that they get globalized as themselves. We restore the environment afterwards by transactifying the globalization procedure.
* Univs: Fix Check calling the kernel to retype in the wrong environment.Gravatar Matthieu Sozeau2015-02-24
| | | | Fixes bug #4089.
* Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorGravatar Enrico Tassi2015-02-14
| | | | Of course such proofs cannot be processed asynchronously
* Optimized Import/Export the same way as Require Import/Export wasGravatar Hugo Herbelin2015-02-04
| | | | | | optimized. Now "Import Arith ZArith" imports only once the libraries reexported by both Arith and ZArith. (No side effect can be inserted here, so that this looks compatible).
* Prevent spurious warnings about Arguments.Gravatar Guillaume Melquiond2015-01-29
| | | | | | | | | | | | | The Arguments command tends to emit the following warning even when properly used: This command is just asserting the number and names of arguments of cons. If this is what you want add ': assert' to silence the warning. If you want to clear implicit arguments add ': clear implicits'. If you want to clear notation scopes add ': clear scopes' In fact, even ': assert' does not silence it, contrarily to what the message suggests.
* Isolate a function for printing evar sets.Gravatar Hugo Herbelin2015-01-24
|
* Univs: proper printing of global and local universe names (onlyGravatar Matthieu Sozeau2015-01-17
| | | | printing functions touched in the kernel).
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* In Show Universes, print universes before normalization.Gravatar Matthieu Sozeau2015-01-05
|
* Proof using: do not clear letins (unless they use a cleared var)Gravatar Enrico Tassi2014-12-29
|
* Proof using: call "clear" to remove from sight the vars not selectedGravatar Enrico Tassi2014-12-28
| | | | | | | As discussed on coqdev, clear is not perfect, Hints for trivial using cleared section vars are still used. But it is better than nothing I guess.
* remove debug prints (leftover)Gravatar Enrico Tassi2014-12-28
|
* Better doc and a few fixes for Proof using.Gravatar Enrico Tassi2014-12-19
|
* Proof using: New vernacular to name sets of section variablesGravatar Enrico Tassi2014-12-18
|
* Arguments: warn only if no option is given (Close 3860)Gravatar Enrico Tassi2014-12-17
|
* Fixing CAMLP4 compilation.Gravatar Pierre-Marie Pédrot2014-12-16
|
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
| | | | | | | | | | | | | | | | | | | | Instead of modifying exceptions to wear additional information, we instead use a dedicated type now. All exception-using functions were modified to support this new type, in particular Future's fix_exn-s and the tactic monad. To solve the problem of enriching exceptions at raise time and recover this data in the try-with handler, we use a global datastructure recording the given piece of data imperatively that we retrieve in the try-with handler. We ensure that such instrumented try-with destroy the data so that there may not be confusion with another exception. To further harden the correction of this structure, we also check for pointer equality with the last raised exception. The global data structure is not thread-safe for now, which is incorrect as the STM uses threads and enriched exceptions. Yet, we splitted the patch in two parts, so that we do not introduce dependencies to the Thread library immediatly. This will allow to revert only the second patch if ever we switch to OCaml-coded lightweight threads.
* Error messages of Searchxxx are coherent with goal selector.Gravatar Pierre Courtieu2014-12-16
| | | | | | If a goal is given and wrong, exception is raised. If no goal is given, then goal 1 is tried but no failure if goal 1 does not exist, just fall back to gloab env.
* About now accepts hypothesis names and goal selector.Gravatar Pierre Courtieu2014-12-15
|
* Util.un_op -> Option.defaultGravatar Pierre Boutillier2014-12-14
|
* Searchxxx now interpret patterns in goal environment if any.Gravatar Pierre Courtieu2014-12-12
| | | | | | | | | | | This makes such things work: x:nat h: x = 3 ================ True Search x.
* Searchxxx now search also the hypothesis and support goal selector.Gravatar Pierre Courtieu2014-12-12
| | | | Documentation also updated.
* Reactivating option "Set Printing Existential Instances" for asking printing ↵Gravatar Hugo Herbelin2014-12-04
| | | | full instances.
* Now that evars can be parsed, protect strongly Check from calling kernel ↵Gravatar Hugo Herbelin2014-11-03
| | | | with evars.
* Show: do print the goalsGravatar Enrico Tassi2014-11-03
|
* Add an [Info Level] option to print info traces automatically.Gravatar Arnaud Spiwack2014-11-01
| | | | [Set Info Level n] prints all info traces at level [n]. [Unset Info Level] stops the automatic printing of info traces. The unfolding level [n] can be overloaded by local [Info m tac] calls.
* Add [Info] command.Gravatar Arnaud Spiwack2014-11-01
| | | | Called with [Info n tac], runs [tac] and prints its info trace unfolding [n] level of tactic names ([0] for no unfolding at all).
* Show_script called only if in coqtop modeGravatar Enrico Tassi2014-10-31
|
* Fixes for PG (Close 3763, 3770)Gravatar Enrico Tassi2014-10-27
| | | | | | | - Show does not print the goal twice - Undo is considered as part of the document when PG mode (bug introduced when Undo was said not to be part of the document in coqtop mode).
* Change reduction_of_red_expr to return an e_reduction_function returningGravatar Matthieu Sozeau2014-10-24
| | | | | | an updated evar_map, as pattern is working up to universe equalities that must be kept. Straightforward adaptation of the code depending on this.
* Goal printing made uniform: always done in STM (close 3585)Gravatar Enrico Tassi2014-10-22
| | | | | | | | | | Goal printing was partially broken. Some commands in vernacentries were printing, but not all of them. Moreover an unlucky combination of `Flags.verbosely (fun () -> interp "Set Silent")` was making the silent flag not settable anymore. Now STM always print the open goals after a command when run in interactive mode via coqtop or emacs. More modern GUI do ask for the goals.
* Continuing experimental printing of the signature of open evars inGravatar Hugo Herbelin2014-10-21
| | | | | | Check (see cfff8f8a327) [printing only visible evars, not the ones corresponding to unrelated open goals + fixing bug on wrong sigma and on evar_info normalization].
* Experimental printing of the signature of open evars in Check.Gravatar Hugo Herbelin2014-10-17
|
* Fix typo, thanks Mike Shulman for spotting itGravatar Enrico Tassi2014-10-13
|
* Emit a warning for void Arguments statement (Close 3713)Gravatar Enrico Tassi2014-10-13
|
* Splitting out of auto.ml a file hints.ml dedicated to hints so as toGravatar Hugo Herbelin2014-10-07
| | | | | | being able to export hints without tactics, vm, etc. to come with. Some functions moved to the new proof engine.
* Notation: option to attach extra pretty printing rules to notationsGravatar Enrico Tassi2014-09-29
| | | | | | | | | | | so that one can retrieve them and pass them to third party tools (i.e. print the AST with the notations attached to the nodes concerned). Available syntax: - all in one: Notation "a /\ b" := ... (format "...", format "latex" "#1 \wedge #2"). - a posteriori: Format Notation "a /\ b" "latex" "#1 \wedge #2".
* Revert specific syntax for primitive projections, avoiding uglyGravatar Matthieu Sozeau2014-09-17
| | | | | | | | contortions in internalization/externalization. It uses a fully typed version of detyping, requiring the environment, to move from primitive projection applications to regular applications of the eta-expanded version. The kernel is unchanged, and only constrMatching needs compatibility code now.
* Rework typeclass resolution and control of backtracking.Gravatar Matthieu Sozeau2014-09-15
| | | | | | | Add a global option to check for multiple solutions and fail in that case. Add another flag to declare classes as having unique instances (not checked but assumed correct, avoiding some backtracking).
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 12:19:54 +0000