aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
| | | | * | | | | | | overlay for UniMathGravatar Enrico Tassi2017-05-23
| | | | | | | | | | |
| | | | * | | | | | | coq_makefile: avoid spurious ./ in generated .conf fileGravatar Enrico Tassi2017-05-23
| | | | | | | | | | |
| | | | * | | | | | | Restore 8.5, 8.6 compatibility of STDTIME, TIMECMDGravatar Jason Gross2017-05-23
| | | | | | | | | | |
| | | | * | | | | | | coq_makefile: don't quote extra arguments (-arg)Gravatar Enrico Tassi2017-05-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Restores compatibility with 8.6
| | | | * | | | | | | Make install a single colon target for retro compatibilityGravatar Enrico Tassi2017-05-23
| | | | | | | | | | |
| | | | * | | | | | | enters coq_makefile2Gravatar Enrico Tassi2017-05-23
| | | | | | | | | | |
| | | | * | | | | | | test suite for coq_makefile2Gravatar Enrico Tassi2017-05-23
| | | | | | | | | | |
| | | | * | | | | | | coqdep: remove optimization making makefiles harder to writeGravatar Enrico Tassi2017-05-23
| | | | | | | | | | |
| | | | * | | | | | | ocamlfind: coqtop -config prints ocamlfind as found by ./configureGravatar Enrico Tassi2017-05-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Used to guess again the ocamlfind location at Coq's execution time. An option to override the value (inferred at ./configure time) is available. So, what is the point of guessing it? Either it stays there, or the user is doing a hack, and has a flag to do it.
| | | | * | | | | | | coqdep: set FOR_PACK variable for files that need to be packedGravatar Enrico Tassi2017-05-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This enables one to have just one rule to compile .ml -> .cmx. By using $(FOR_PACK) in such rule one passes to ocamlopt -for-pack ModName only when necessary. Before this coq_makefile had to generate 2 different rules, depending if the module was mentioned in an .mlpack.
| | | | * | | | | | | print_config: print COQ_SRC_SUBDIRSGravatar Enrico Tassi2017-05-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This way a makefile can just iterate on this list, intead of having a bunch of -I hardcoded in there by coq_makefile
| | | | * | | | | | | Document --print-version in UsageGravatar Enrico Tassi2017-05-23
| | | | | | | | | | |
| | | | * | | | | | | Put the list of Coq sources subdirectories in one placeGravatar Enrico Tassi2017-05-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | and avoid duplication
| | | | * | | | | | | Usage.print_config moved to EnvarsGravatar Enrico Tassi2017-05-23
| | | | | | | | | | |
| | | | * | | | | | | CoqProject_file: document in API deprecated featuresGravatar Enrico Tassi2017-05-23
| | | | | | | | | | |
| | | | * | | | | | | CoqProject_file: API and code cleanup (tuples -> records)Gravatar Enrico Tassi2017-05-23
| | | | | | | | | | |
| | | | * | | | | | | ide/project_file.ml4 -> lib/coqProject_file.ml4 + .mliGravatar Enrico Tassi2017-05-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The .mli only acknowledges the current API. I'm not guilty your honor!
| | | | * | | | | | | ide/project_fie.ml4: include standard banner with copyrightGravatar Enrico Tassi2017-05-23
| | | | | | | | | | |
| | | | * | | | | | | test suite for coq_makefileGravatar Enrico Tassi2017-05-23
| | | | | | | | | | |
| | | | * | | | | | | configure: -local set coqdoc destination dir to ./doc rather than ""Gravatar Enrico Tassi2017-05-23
| |_|_|/ / / / / / / |/| | | | | | | | |
| | | | | | | | * | Bigint.euclid: clarify which sign convention is usedGravatar Pierre Letouzey2017-05-23
| | | | | | | | | |
* | | | | | | | | | Merge PR#661: Added a test for #4765 (an example of printing abbreviation ↵Gravatar Maxime Dénès2017-05-23
|\ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | with binders)
* \ \ \ \ \ \ \ \ \ \ Merge PR#659: Mention ./configure in INSTALL.docGravatar Maxime Dénès2017-05-23
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR#657: [test-suite] Add tests for goal printing.Gravatar Maxime Dénès2017-05-23
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR#646: Revised behavior on ill-formed identifiersGravatar Maxime Dénès2017-05-23
|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR#660: Change wrong bullet message.Gravatar Maxime Dénès2017-05-23
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR#518: Faster universe unificationGravatar Maxime Dénès2017-05-23
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | * | | | | | | | [vernac] Remove `Save thm id.` command.Gravatar Emilio Jesus Gallego Arias2017-05-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We'd like to cleanup the `proof_end` type so we can have a smaller path in proof save. Note that the construction: ``` Goal Type. ⋮ Save id. ``` has to be handled by the STM in the same path as Defined (but with an opaque flag), as `Save id` will alter the environment and cannot be processed in parallel. We thus try to simply such paths a bit, as complexity of `lemmas.ml` seems like an issue these days. The form `Save Theorem id` doesn't really seem used, and moreover we should really add a type of "Goal", and unify syntax. It is often the case that beginners try `Goal addnC n : n + 0 = n." etc...
| | | | | | | | * | | | | | | | [vernac] Remove `Save.` command.Gravatar Emilio Jesus Gallego Arias2017-05-23
| |_|_|_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It has been deprecated for a while in favor of `Qed`.
| | | | | | | | | | | | | * | refl_omega: some code refactoringGravatar Pierre Letouzey2017-05-22
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | * | refl_omega.v: explicitely identify atom indexes and omega varsGravatar Pierre Letouzey2017-05-22
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | * | ReflOmegaCore: misc cleanup, <? instead of bgt, etcGravatar Pierre Letouzey2017-05-22
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | * | ROmega : O_STATE turned into a O_SUMGravatar Pierre Letouzey2017-05-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We benefit from the fact that we normalize now *all* hypotheses even the one defining the "stated" variable: it is produced as ...def of v... = v and normalized as -v + ...def of v... = 0 which is precisely what we should add to the initial equation during a O_STATE.
| | | | | | | | | | | | | * | ROmega: less contructors in the final omega traceGravatar Pierre Letouzey2017-05-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Now that O_SUM is properly optimized (cf. the [fusion] function), we could use it to encode CONTRADICTION and NEGATE_CONTRADICT(_INV). This way, the trace has almost the same size, but ReflOmegaCore.v is shorter and easier to maintain.
| | | | | | | | | | | | | * | ROmega : merge O_CONSTANT* into a single O_BAD_CONSTANTGravatar Pierre Letouzey2017-05-22
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | * | ReflOmegaCore: reverse some integer mult (coefs k1,k2 will often be simple)Gravatar Pierre Letouzey2017-05-22
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | * | ReflOmegaCore: comment, reorganize, permut some constructors, etcGravatar Pierre Letouzey2017-05-22
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | * | romega: add a tactic named unsafe_romega (for debugging, or bold users)Gravatar Pierre Letouzey2017-05-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In this variant, the proof term produced by romega isn't verified at the tactic run-time (no vm_compute). In theory, [unsafe_romega] should behave exactly as [romega], but faster. Now, if there's a bug in romega, we'll be notified only at the following Qed. This could be interesting for debugging purpose : you could inspect the produced buggish term via a Show Proof.
| | | | | | | | | | | | | * | romega: no more normalization trace, replaced by some Coq-side computationGravatar Pierre Letouzey2017-05-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a major change : - Generated proofs are quite shorter, since only the resolution trace remains. - No time penalty mesured (it even tends to be slightly faster this way). - Less infrastructure in ReflOmegaCore and refl_omega. - Warning: the normalization functions in ML and in Coq should be kept in sync, as well as the variable order. - Btw: get rid of ML constructor Oufo
| | | | | | | | | | | | | * | romega/const_omega : a few improvements (less try with, no gen equality)Gravatar Pierre Letouzey2017-05-22
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | * | romega: use N instead of nat for TvarGravatar Pierre Letouzey2017-05-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In a coming commit, we'll normalize terms by a Coq function that will compare Tvar's instead of blindly applying a trace, so let's speed-up these comparisons.
| | | | | | | | | | | | | * | romega: shorter trace (no more term lengths)Gravatar Pierre Letouzey2017-05-22
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | * | refl_omega: refactoring of normalize_equationGravatar Pierre Letouzey2017-05-22
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | * | ReflOmegaCore: lots of dead code + a few refactored proofsGravatar Pierre Letouzey2017-05-22
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | * | romega: if it bugs again, at least do it with a short and quick errorGravatar Pierre Letouzey2017-05-22
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | * | refl_omega: comment the lack of lifts when dealing with arrowsGravatar Pierre Letouzey2017-05-22
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | * | romega: discard constructor D_mono (shorter trace + fix a bug)Gravatar Pierre Letouzey2017-05-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | For the bug, see new test test_romega10 in test-suite/success/ROmega0.v.
| | | | | | | | | | | | | * | refl_omega: more refactoring (e.g. IntSets instead of sorted lists)Gravatar Pierre Letouzey2017-05-22
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | * | refl_omega: refactoring (e.g. useless args in destructurate_pos_hyp)Gravatar Pierre Letouzey2017-05-22
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | * | ReflOmegaCore: discard useless cosntructor P_NOPGravatar Pierre Letouzey2017-05-22
| | | | | | | | | | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 06:23:59 +0000