aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernacentries.ml
Commit message (Collapse)AuthorAge
* 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).
* Uniformisation of the order of arguments env and sigma.Gravatar Hugo Herbelin2014-09-12
|
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
| | | | | instances still to do). Using heuristics to name after the quantifier name it comes. Also added a "sigma" to almost all printing functions.
* Commands like [Inductive > X := … | … | …] raise an error message ↵Gravatar Arnaud Spiwack2014-09-04
| | | | instead of silently ignoring the ">" syntax.
* Remove [Infer] option of records.Gravatar Arnaud Spiwack2014-09-04
| | | Dead code formerly used by the now defunct [autoinstances].
* Type definitions [Variant] and [Record] really don't accept the wrong kind ↵Gravatar Arnaud Spiwack2014-09-04
| | | | | | | of definition. - [Variant] will accept variant definitions but no record definition - [Record] will accept record definitions but no variant definition
* Print [Variant] types with the keyword [Variant].Gravatar Arnaud Spiwack2014-09-04
| | | | Involves changing the [mind_finite] field in the kernel from a bool to the trivalued type [Decl_kinds.recursivity_kind]. This is why so many files are (unfortunately) affected. It would not be very surprising if some bug was introduced.
* Moving code of tactic interpretation from Tacenv to Vernacentries.Gravatar Pierre-Marie Pédrot2014-08-31
| | | | | This allows to directly register globtactics in the Tacenv API, without having to resort to any internalization function.
* Fixing the essence of naming bug #3204: use same strategy for namingGravatar Hugo Herbelin2014-08-25
| | | | | | | | | | cases pattern variables than for naming forall/fun binders (but still avoiding constructor names). Note in passing: such as it is implemented, the general strategy is in O(n²) in the number of nested binders, because, when computing the name for each 'fun x => c" (or forall, or a pattern name), the names from the outside c and visibly occurring in c are computed.
* STM: new "par:" goal selector, like "all:" but in parallelGravatar Enrico Tassi2014-08-05
| | | | | par: distributes the goals among a number of workers given by -async-proofs-tac-j (defaults to 2).
* Unifying locate code, also making it more powerful: it is now able to findGravatar Pierre-Marie Pédrot2014-07-21
| | | | any prefix of the given qualid.
* Adding a new "Locate Term" command, distinct from the raw "Locate" command.Gravatar Pierre-Marie Pédrot2014-07-21
| | | | | | | | The new Term version has essentially the same behaviour as the old "Locate", while the new raw searches for all types of objects. Also code merging with the "Locate Ltac". Fixes bug #3380.
* More complete printing of Ltac location, akin to the term-dedicated Locate ↵Gravatar Pierre-Marie Pédrot2014-07-21
| | | | command.
* smartlocate: look for the head symbol for realGravatar Enrico Tassi2014-07-14
| | | | | | This bug was hacked around in ssreflect, but with the new idea that parsing and interpretation are done in distinct phases the work around could not be implemented anymore.
* Adding a "time" tactical for benchmarking purposes. In case the tacticGravatar Hugo Herbelin2014-07-13
| | | | backtracks, print time spent in each of successive calls.
* Revert "time tac" (committed by mistake).Gravatar Hugo Herbelin2014-07-07
| | | | This reverts commit abad0a15ac44cb5b53b87382bb4d587d9800a0f6.
* time tacGravatar Hugo Herbelin2014-07-07
|
* Add toplevel commands to declare global universes and constraints.Gravatar Matthieu Sozeau2014-07-01
|
* all coqide specific files moved into ide/Gravatar Enrico Tassi2014-06-25
| | | | | | | | | | | | | | | | | | | | lib/interface split into: - lib/feedback subscribe-based feedback bus (also used by coqidetop) - ide/interface definition of coqide protocol messages lib/pp structured info/err/warn messages lib/serialize split into: - lib/serialize generic xml serialization (list, pairs, int, loc, ...) used by coqide but potentially useful to other interfaces - ide/xmlprotocol serialization of protocol messages as in ide/interface the only drawback is that coqidetop needs -thread and I had to pass that option to all files in ide/
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 05:25:50 +0000