aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Collapse)AuthorAge
* Add syntax for naming new goals in refine: writing ?[id] instead of _Gravatar Hugo Herbelin2014-09-30
| | | | | | | | will name the goal id; writing ?[?id] will use the first fresh name available based with prefix id. Tactics intro, rename, change, ... from logic.ml now preserve goal name; cut preserves goal name on its main premise.
* 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".
* do not explode if a plugin is not up to date on -help (Close: 3673)Gravatar Enrico Tassi2014-09-29
|
* Merging some functions from evarutil.ml/evd.ml.Gravatar Hugo Herbelin2014-09-29
| | | | | | | | | | | | | - Removed collect_evars which does not consider instance (use evars_of_term instead). - Also removed evars_of_evar_info which did not filter context (use evars_of_filterered_evar_info instead). This is consistent with printing goal contexts in the filtered way. Anyway, as of today, afaics goals filters are trivial because (if I interpret evarutil.ml correctly), evars with non-trivial filter necessarily occur in a conv pb. Conversely, conv pbs being solved when tactics are called, there should not be an evar used as a goal with a non-trivial filter.
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
| | | | | | | | so as to reproduce correctly the reduction behavior of existing projections, i.e. delta + iota. Make [projection] an abstract datatype in Names.ml, most of the patch is about using that abstraction. Fix unification.ml which tried canonical projections too early in presence of primitive projections.
* Fixing bug #3646.Gravatar Pierre-Marie Pédrot2014-09-19
|
* mltop: when a plugin is loaded store its full path in the summaryGravatar Enrico Tassi2014-09-18
| | | | | | | | | | | This fixes the following bug related to stm: if one passes -I to coqide, then such flag is passes to the workers; but if one uses "Add ML LoadPath" to extend the paths in which coq looks for plugins, this extra path was no passed to the slaves (via the command line) nor store in the system state and hence sent to the slaves. With this patch, when a cmxs is loaded, its full path is stored in the summary and hence sent to the workers as one may expect.
* Be more conservative and keep the use of eq_constr in pretyping/ functions.Gravatar Matthieu Sozeau2014-09-17
|
* Fix bug #3593, making constr_eq and progress work up toGravatar Matthieu Sozeau2014-09-17
| | | | equality of universes, along with a few other functions in evd.
* 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.
* Undo prints only if coqtop || emacsGravatar Enrico Tassi2014-09-16
|
* better error messageGravatar Enrico Tassi2014-09-16
|
* 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).
* Providing a -type-in-type option for collapsing the universe hierarchy.Gravatar Hugo Herbelin2014-09-13
|
* 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.
* Add a flag for restricting resolution of typeclasses toGravatar Matthieu Sozeau2014-09-11
| | | | | | | matching (i.e. no instanciation of the goal evars). Classes defined when [Set Typeclasses Strict Resolution] is on use the restricted resolution for all their instances (except for Hint Extern's).
* Fix categorization of recursive inductives.Gravatar Matthieu Sozeau2014-09-10
|
* Fixing localisation of tactic errors (my mistake in himsg.ml essentially).Gravatar Hugo Herbelin2014-09-10
|
* VernacExtend does not dispatch on type anymore.Gravatar Pierre-Marie Pédrot2014-09-10
|
* Load Prelude.vi if not Prelude.vo is found (Close: 3595)Gravatar Enrico Tassi2014-09-09
|
* Undo: if the ui is coqtop (command line) then Undo is not part of the doc.Gravatar Enrico Tassi2014-09-09
|
* toploop plugins taken into account when printing --help (close: 3535)Gravatar Enrico Tassi2014-09-09
| | | | | | | | | | | | | E.g. Coq options are: -I dir look for ML files in dir -include dir (idem) [...] -h, --help print this list of options With the flag '-toploop coqidetop' these extra option are also available: --help-XML-protocol print the documentation of the XML protocol used by CoqIDE
* Removing dead code relative to the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
|
* Parsing of Type@{max(i,j)}.Gravatar Matthieu Sozeau2014-09-08
|
* Fixing bug #3492.Gravatar Pierre-Marie Pédrot2014-09-07
|
* Renaming goal-entering functions.Gravatar Pierre-Marie Pédrot2014-09-06
| | | | | | | | | | | 1. Proofview.Goal.enter into Proofview.Goal.nf_enter. 2. Proofview.Goal.raw_enter into Proofview.Goal.enter. 3. Proofview.Goal.goals -> Proofview.Goals.nf_goals 4. Proofview.Goal.raw_goals -> Proofview.Goals.goals 5. Ftactic.goals -> Ftactic.nf_goals 6. Ftactic.raw_goals -> Ftactic.goals This is more uniform with the other functions of Coq.
* More explicit printing in Himsg.Gravatar Pierre-Marie Pédrot2014-09-04
|
* 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 with [Variant] don't generate inductive schemes by default.Gravatar Arnaud Spiwack2014-09-04
| | | | | | - The option [Record Elimination Schemes] is replaced by [Nonrecursive Elimination Schemes] ([Record Elimination Schemes] is kept as a deprecated option for compatibility) - [Variant] don't generate inductive scheme unless [Nonrecursive Elimination Schemes] is turned on. - Inductive records generate induction schemes even when [Nonrecursive Elimination Schemes] is off.
* 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
* Types declared as Variants really do not accept recursive definitions.Gravatar Arnaud Spiwack2014-09-04
|
* 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.
* Print error messages with more hidden information based on α-equivalence .Gravatar Arnaud Spiwack2014-09-03
| | | | | The comparison on terms which triggers new printing flags in case two terms which are different would be printed identically now contains α-equivalence. The implementation using a canonization function on [constr] instead of trying to deal with [constr_expr] was suggested by Hugo.
* Additional entry tactic_arg in Print Grammar tactic.Gravatar Pierre-Marie Pédrot2014-09-03
|
* coqworkmgrGravatar Enrico Tassi2014-09-02
|
* Getting rid of atomic tactics in Tacenv.Gravatar Pierre-Marie Pédrot2014-08-31
| | | | | | ML tactics that may be used as simple identifiers are now declared as a true Ltac entry pertaining to the module that contains the Declare ML Module statement.
* 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.
* Simplify even further the declaration of primitive projections,Gravatar Matthieu Sozeau2014-08-30
| | | | | | | | | | | now done entirely using declare_mind, which declares the associated constants for primitive records. This avoids a hack related to elimination schemes and ensures that the forward references to constants in the mutual inductive entry are properly declared just after the inductive. This also clarifies (and simplifies) the code of term_typing for constants which does not have to deal with building or checking projections anymore. Also fix printing of universes showing the de Bruijn encoding in a few places.
* Fixing commit 50237af2.Gravatar Pierre-Marie Pédrot2014-08-29
| | | | | Indeed, generalized binders are unnamed, because their name is generated on the fly.
* Fix bug when defining primitive projections mixing defined and abstracts fields.Gravatar Matthieu Sozeau2014-08-29
|
* Fixing bug #3528.Gravatar Pierre-Marie Pédrot2014-08-28
|
* Change the way primitive projections are declared to the kernel.Gravatar Matthieu Sozeau2014-08-28
| | | | | | | | | | | Now kernel/indtypes builds the corresponding terms (has to be trusted) while translate_constant just binds a constant name to the already entered projection body, avoiding the dubious "check" of user given terms. "case" Pattern-matching on primitive records is now disallowed, and the default scheme is implemented using projections and eta (all elimination tactics now use projections as well). Elaborate "let (x, y) := p in t" using let bindings for the projections of p too.
* Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possibleGravatar Matthieu Sozeau2014-08-25
| | | | | to match on a primitive projection application c.(p) using "?f _", binding f to (fun x => x.(p)) with the correct typing.
* 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.
* Prerequisite to fix stm test-suite when not in -localGravatar Pierre Boutillier2014-08-25
|
* Fixing bug #3533.Gravatar Pierre-Marie Pédrot2014-08-23
| | | | | Now error printing tries to set universe printing when two terms are not desambiguated.
* Move UnsatisfiableConstraints to a pretype error.Gravatar Matthieu Sozeau2014-08-22
|
* Reorganisation of intropattern codeGravatar Hugo Herbelin2014-08-18
| | | | | | | | | | | | | | | | - emphasizing the different kinds of patterns - factorizing code of the non-naming intro-patterns Still some questions: - Should -> and <- apply to hypotheses or not (currently they apply to hypotheses either when used in assert-style tactics or apply in, or when the term to rewrite is a variable, in which case "subst" is applied)? - Should "subst" be used when the -> or <- rewrites an equation x=t posed by "assert" (i.e. rewrite everywhere and clearing x and hyp)? - Should -> and <- be applicable in non assert-style if the lemma has quantifications?
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 06:43:01 +0000