aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Feedback: LoadedFile + GoalsGravatar Enrico Tassi2014-07-11
| | | | | LoadedFile is generated when a .vo is loaded Goals is generated when -feedback-goals
* Export type_of_global_ref (useful for external users of glob files)Gravatar Enrico Tassi2014-07-11
|
* make the standard logging facility stm awareGravatar Enrico Tassi2014-07-11
|
* MSetRBT: unfortunate typo in compare_height (fix #3413)Gravatar Pierre Letouzey2014-07-10
|
* Better handling of the universe context in case of Admitted proof obligations.Gravatar Matthieu Sozeau2014-07-10
|
* Overlooked to remove a change in kernel/closure that made reducing underGravatar Matthieu Sozeau2014-07-10
| | | | a primitive projection impossible.
* option to always delegate futures to workersGravatar Enrico Tassi2014-07-10
|
* CoqIDE: on win32 the old interrputer code (SIGINT) is still neededGravatar Enrico Tassi2014-07-10
|
* more APIs in TQueue and CThreadGravatar Enrico Tassi2014-07-10
| | | | These are now sufficient to implement PIDE
* check_for_interrupt: better (but slower) in threading modeGravatar Enrico Tassi2014-07-10
| | | | | Experimenting with PIDE I discovered that yield is not sufficient to have a rescheduling, hence the delay.
* Reduce non-toplevel letins in splay_prod_assum (bug found in Ergo).Gravatar Matthieu Sozeau2014-07-10
|
* Fix a oversight in 5bf9e67b .Gravatar Arnaud Spiwack2014-07-10
| | | | | | About 8 months after making this commit, I realised that I forgot to change a tclORELSE into a tclOR (which was the whole point of the commit to begin with). Shame on me. It does not seem to have much of an effect on efficiency, though. It may be a hair faster, but mostly indistinguishably so.
* Revert patch making the oracle be used for the transparent state in evarconv,Gravatar Matthieu Sozeau2014-07-09
| | | | | which made CoRN (and probably Ergo) fail. Another option should be found for making a constant not unfoldable by tactics/refinement.
* Locate: also display some information about module aliasingGravatar Pierre Letouzey2014-07-09
| | | | | Typically, if module M has a constant t and module P contains "Include M", then "Locate t" will now mention that P.t is an alias of M.t
* Arith: full integration of the "Numbers" modular frameworkGravatar Pierre Letouzey2014-07-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - The earlier proof-of-concept file NPeano (which instantiates the "Numbers" framework for nat) becomes now the entry point in the Arith lib, and gets renamed PeanoNat. It still provides an inner module "Nat" which sums up everything about type nat (functions, predicates and properties of them). This inner module Nat is usable as soon as you Require Import Arith, or just Arith_base, or simply PeanoNat. - Definitions of operations over type nat are now grouped in a new file Init/Nat.v. This file is meant to be used without "Import", hence providing for instance Nat.add or Nat.sqrt as soon as coqtop starts (but no proofs about them). - The definitions that used to be in Init/Peano.v (pred, plus, minus, mult) are now compatibility notations (for Nat.pred, Nat.add, Nat.sub, Nat.mul where here Nat is Init/Nat.v). - This Coq.Init.Nat module (with only pure definitions) is Include'd in the aforementioned Coq.Arith.PeanoNat.Nat. You might see Init.Nat sometimes instead of just Nat (for instance when doing "Print plus"). Normally it should be ok to just ignore these "Init" since Init.Nat is included in the full PeanoNat.Nat. I'm investigating if it's possible to get rid of these "Init" prefixes. - Concerning predicates, orders le and lt are still defined in Init/Peano.v, with their notations "<=" and "<". Properties in PeanoNat.Nat directly refer to these predicates in Peano. For instantation reasons, PeanoNat.Nat also contains a Nat.le and Nat.lt (defined via "Definition le := Peano.le", we cannot yet include an Inductive to implement a Parameter), but these aliased predicates won't probably be very convenient to use. - Technical remark: I've split the previous property functor NProp in two parts (NBasicProp and NExtraProp), it helps a lot for building PeanoNat.Nat incrementally. Roughly speaking, we have the following schema: Module Nat. Include Coq.Init.Nat. (* definition of operations : add ... sqrt ... *) ... (** proofs of specifications for basic ops such as + * - *) Include NBasicProp. (** generic properties of these basic ops *) ... (** proofs of specifications for advanced ops (pow sqrt log2...) that may rely on proofs for + * - *) Include NExtraProp. (** all remaining properties *) End Nat. - All other files in directory Arith are now taking advantage of PeanoNat : they are now filled with compatibility notations (when earlier lemmas have exact counterpart in the Nat module) or lemmas with one-line proofs based on the Nat module. All hints for database "arith" remain declared in these old-style file (such as Plus.v, Lt.v, etc). All the old-style files are still Require'd (or not) by Arith.v, just as before. - Compatibility should be almost complete. For instance in the stdlib, the only adaptations were due to .ml code referring to some Coq constant name such as Coq.Init.Peano.pred, which doesn't live well with the new compatibility notations.
* Fixing the previous patch to keep transparent states in sync.Gravatar Pierre-Marie Pédrot2014-07-09
|
* Recovering transparent state from kernel oracles in constant time.Gravatar Pierre-Marie Pédrot2014-07-09
|
* Fixing bug #3270. Patch by Robbert Krebbers.Gravatar Pierre-Marie Pédrot2014-07-08
|
* Exporting Proof.split in proofview.Gravatar Pierre-Marie Pédrot2014-07-08
|
* Revert "time tac" (committed by mistake).Gravatar Hugo Herbelin2014-07-07
| | | | This reverts commit abad0a15ac44cb5b53b87382bb4d587d9800a0f6.
* time tacGravatar Hugo Herbelin2014-07-07
|
* Updating README wrt coq-club and ftp.Gravatar Hugo Herbelin2014-07-07
|
* Fix g_coqast for explicit applications.Gravatar Matthieu Sozeau2014-07-07
|
* Coq_makefile: fix cmx compilation when there are both ml and mllibGravatar Pierre Boutillier2014-07-07
|
* In flex-flex cases, the undefinedness of an evar can not be preseved after ↵Gravatar Matthieu Sozeau2014-07-07
| | | | | | converting the stacks. Take care of this by recalling unification.
* Missing check of evar instantiation, resulting in missing constraints (bug ↵Gravatar Matthieu Sozeau2014-07-07
| | | | from MathClasses).
* In dest_prod_assum, allow non-toplevel let-reductions (fixes a bug found in ↵Gravatar Matthieu Sozeau2014-07-07
| | | | MathClasses).
* Using IStream coiterator to explicit the captured state of tactic matching ↵Gravatar Pierre-Marie Pédrot2014-07-05
| | | | results.
* Cleanup code related to the constraint solving, which sits now outside theGravatar Matthieu Sozeau2014-07-03
| | | | kernel in library/universes.ml.
* Properly compute the transitive closure of the system of constraintsGravatar Matthieu Sozeau2014-07-03
| | | | | generated by a mutual inductive definition (bug found in CFGV). Actually this code can move out of the kernel.
* Restore proper order of effects in letin_tac_gen. Fixes CFGV again.Gravatar Matthieu Sozeau2014-07-03
|
* Fix eta expansion of primitive records (HoTT bug #78), which now fails ↵Gravatar Matthieu Sozeau2014-07-03
| | | | | | cleanly when called on partially applied constructors. Also protect evar_conv from that case.
* Fix Coq_makefile in presence of mlpackGravatar Pierre Boutillier2014-07-03
|
* coqdoc is minimaly -Q awareGravatar Pierre Boutillier2014-07-03
|
* Adding a coiterator to IStream.Gravatar Pierre-Marie Pédrot2014-07-03
|
* More efficient implementation of Ltac match, by inlining a stream map.Gravatar Pierre-Marie Pédrot2014-07-03
|
* When defining a monomorphic Program, do not allow arbitrary instantiationsGravatar Matthieu Sozeau2014-07-03
| | | | | | of the universe context in the obligations, it gets gradually fixed globally by each one of them. Fixes bug found in Misc/Overloading.
* Bug 3405: Coq_makefile: Implicit rules only for listed files in Make fileGravatar Pierre Boutillier2014-07-03
|
* In setoid_rewrite, force resolution of the contraints generated by rewriting ↵Gravatar Matthieu Sozeau2014-07-02
| | | | | | | only. Do not mix it with resolution of user-introduced subgoals of typeclass type (bug found in ATBR).
* Fix a Not_found anomaly raised by solve_evar_evar, we were breaking theGravatar Matthieu Sozeau2014-07-02
| | | | invariant that the evar arguments to that function always have to be undefined.
* Indeed simpl never is really honored now.Gravatar Matthieu Sozeau2014-07-02
|
* Add toplevel commands to declare global universes and constraints.Gravatar Matthieu Sozeau2014-07-01
|
* Patch from Enrico Tassi to get Drop compatible with stm.Gravatar Enrico Tassi2014-07-01
|
* Continuing ff9f94634 on making code and doc agree on "Set Equality Schemes"Gravatar Hugo Herbelin2014-07-01
|
* Making code and doc agree on "Set Equality Schemes" (see also bug #2550).Gravatar Hugo Herbelin2014-07-01
|
* Fixing the place where to insert a space in "Tactic failure"Gravatar Hugo Herbelin2014-07-01
| | | | | message. Otherwise, a heading space was missing when calling tclFAIL from ML tactics.
* More informative message when Mltop.load_object fails.Gravatar Hugo Herbelin2014-07-01
|
* Useless keeping of dirpath in tactic aliases.Gravatar Pierre-Marie Pédrot2014-06-30
|
* Clarifying 'No such bound variable' message in apply, as suggested in #2387Gravatar Hugo Herbelin2014-06-30
|
* Tests for bugs #2834 and #2994.Gravatar Hugo Herbelin2014-06-30
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 18:34:18 +0000