aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
Commit message (Collapse)AuthorAge
* Split [Proofview] into a file where the basic operations on the state are ↵Gravatar Arnaud Spiwack2014-10-22
| | | | | | defined and the file providing the primitives. The datatypes are defined in [Proofview_monad], previous [Proofview_monad] is now called [Logic_monad] since it is more generic since the refactoring.
* Fix ill-typed debugging functionGravatar Matthieu Sozeau2014-10-15
|
* Adding printers for ppproofview.Gravatar Hugo Herbelin2014-10-13
|
* Add debug printers for projections, fix printing of evar constraintsGravatar Matthieu Sozeau2014-10-10
| | | | and unsatisfiable constraints which were not done in the right environment.
* Adding printer for named_context_val and Goal.goal in debugger.Gravatar Hugo Herbelin2014-10-09
|
* Adding a printer for hints.Gravatar Hugo Herbelin2014-10-07
|
* Fixing interpretation of constr under binders which was broken afterGravatar Hugo Herbelin2014-10-02
| | | | | it became possible to have binding names themselves bound to ltac variables (2fcc458af16b).
* Fixing nice printing of error reporting with ml tactics bound to ltac names.Gravatar Hugo Herbelin2014-10-01
|
* Fixing use of arguments renaming in apply which was broken afterGravatar Hugo Herbelin2014-10-01
| | | | | reorganization of apply in d5fece25d8964d5d9fcd55b66164286aeef5fb9f: using renaming also in retyping.
* Index keys instead of simply global references.Gravatar Matthieu Sozeau2014-09-27
|
* 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.
* win32: embed NSIS for plugin writersGravatar Enrico Tassi2014-09-19
|
* Fix debug printing with primitive projections.Gravatar Matthieu Sozeau2014-09-18
| | | | | | | Add a flag to indicate if we're in the toplevel or debuggger to not try to retype terms in the wrong environment (and making find_rectype, get_type_of untraceable). This fixes bug #3638 along with the previous commit.
* win32: remove outdated splash screenGravatar Enrico Tassi2014-09-17
| | | | | The official Coq logo does not work as a splash screen. Simplest fix: no splash screen.
* win32: use subsystem windows on windows (and not console)Gravatar Enrico Tassi2014-09-17
| | | | This makes the hammer tools/mkwinapp.ml kind of obsolete
* Fix base_include due to change in argument order of env and evar_mapGravatar Matthieu Sozeau2014-09-12
|
* 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.
* VernacExtend does not dispatch on type anymore.Gravatar Pierre-Marie Pédrot2014-09-10
|
* Merge remote-tracking branch 'jason/win32-improvements' into trunkGravatar Enrico Tassi2014-09-09
|\
| * Bump CoqSDK revision numberGravatar Jason Gross2014-09-09
| |
| * Add a VERBOSE flag to make-sdk-win32Gravatar Jason Gross2014-09-09
| | | | | | | | For debugging purposes.
| * Minor code style cleanup in make-sdk-win32Gravatar Jason Gross2014-09-09
| |
| * Support 64-bit cygwinGravatar Jason Gross2014-09-09
| |
| * Support machines that have a full or nonexistant C driveGravatar Jason Gross2014-09-09
| |
| * Support environments where `find` is Windows' findGravatar Jason Gross2014-09-09
| |
* | Installer for win improvedGravatar Enrico Tassi2014-09-09
|/ | | | | | | | | - checks for paths containing whitespaces - Coqide has syntax highlighting - does not include the ocaml compiler, since it would not work anyway for the purpose of native compile. For that we really need the whole toolchain, including the C linker/assembler. Hence we should just recommend to install the SDK
* Installer for win32Gravatar Enrico Tassi2014-09-09
| | | | | | | | | | | | Not 100% functional, but coqide works. The native compiler is embedded but: - some path mangling problem prevents it from working even when run via cygwin (like in the build process) - CAMLLIB must be exported to ${COQ}\ocaml\lib to have it run (coq should do it). fix
* Debug RAKAMGravatar Pierre Boutillier2014-08-26
|
* A reorganization of the "assert" tactics (hopefully uniform namingGravatar Hugo Herbelin2014-08-18
| | | | | scheme, redundancies, possibility of chaining a tactic knowing the name of introduced hypothesis, new proof engine).
* 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?
* Fixing include of debugger.Gravatar Pierre-Marie Pédrot2014-08-18
|
* STM: encapsulate Pp.message in Feedback.feedbackGravatar Carst Tankink2014-08-04
|
* A tentative uniform naming policy in module Inductiveops.Gravatar Hugo Herbelin2014-08-01
| | | | | | | | | | | | - realargs: refers either to the indices of an inductive, or to the proper args of a constructor - params: refers to parameters (which are common to inductive and constructors) - allargs = params + realargs - realdecls: refers to the defining context of indices or proper args of a constructor (it includes letins) - paramdecls: refers to the defining context of params (it includes letins) - alldecls = paramdecls + realdecls
* Moved code for finding subterms (pattern, induction, set, generalize, ...)Gravatar Hugo Herbelin2014-06-28
| | | | | | | into a specific new cleaned file find_subterm.ml. This makes things clearer but also solves some dependencies problem between Evd, Termops and Pretype_errors.
* Made the subterm finding function make_abstraction independent of theGravatar Hugo Herbelin2014-06-28
| | | | proof engine. Moved it to unification.ml.
* More open in base_includeGravatar Hugo Herbelin2014-06-28
|
* 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/
* Dummy commit to test the new setup of coq-commits mailinglist (bis)Gravatar Pierre Letouzey2014-06-17
|
* Dummy commit to test the new setup of coq-commits mailinglistGravatar Pierre Letouzey2014-06-17
|
* Change Ltac constr matching semantics to consider universes when merging twoGravatar Matthieu Sozeau2014-06-15
| | | | | bindings of the same variable (fixing HoTT bug #52). Document the unification of universes in Ltac/tactics.
* - Fix bug #3368, due to wrong use of the Cst_stack for projections.Gravatar Matthieu Sozeau2014-06-11
| | | | | - Monomorphize Cst_stack to 'a = constr. - Add corresponding debug printer.
* Fix module order in printers.mllibGravatar Matthieu Sozeau2014-06-10
|
* Cleanup in Univ, moving code for UniverseConstraints outside the kernel in ↵Gravatar Matthieu Sozeau2014-06-10
| | | | | | | | Universes. Needed to exponse compare_head_gen(_leq) so that it could be reused in Universes. Remove unused functions from univ as well and refactor a little bit. Changed the syntax to Type@{} for explicit universe level specs, following the WG decision.
* Moving a Thread.yield in check_interrupt.Gravatar Pierre-Marie Pédrot2014-06-07
|
* Adding a new Control file centralizing the control options of Coq.Gravatar Pierre-Marie Pédrot2014-06-07
|
* A little bit of documentation about V5.10 and V6.3 and V7.Gravatar Hugo Herbelin2014-06-01
|
* - Fix in kernel conversion not folding the universe constraintsGravatar Matthieu Sozeau2014-05-26
| | | | | | | | | correctly when comparing stacks. - Disallow Type i <= Prop/Set constraints, that would otherwise allow constraints that make a universe lower than Prop. - Fix stm/lemmas that was pushing constraints to the global context, it is done depending on the constant/variable polymorphic status now. - Adapt generalized rewriting in Type code to these fixes.
* Isolating a function "make_abstraction", new name of "letin_abstract",Gravatar Hugo Herbelin2014-05-08
| | | | which compute an abstraction of the goal over a term or a pattern.
* Renaming new_induct -> induction; new_destruct -> destruct.Gravatar Hugo Herbelin2014-05-08
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 16:21:53 +0000