| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-09-15 | Moving Ltac printers to ltac/ folder. | Pierre-Marie Pédrot | |
| 2016-09-15 | Generalizing the notion of constr substitution to generic arguments. | Pierre-Marie Pédrot | |
| This removes a dependency on wit_tactic in Constrintern. | |||
| 2016-09-14 | Moving Ltac-specific parsing API to ltac/ folder. | Pierre-Marie Pédrot | |
| 2016-09-14 | Moving the tactic-in-term extension from G_constr to G_ltac. | Pierre-Marie Pédrot | |
| 2016-09-14 | Allowing to extend the Print Grammar command generically. | Pierre-Marie Pédrot | |
| We also move the Ltac-specific grammar to its folder. | |||
| 2016-09-11 | Move Ltac-specific components from G_proofs to G_ltac. | Pierre-Marie Pédrot | |
| 2016-09-09 | Removing the last uses of Pptactic in the lower layers. | Pierre-Marie Pédrot | |
| 2016-09-08 | Unplugging Pptactic from Ppvernac. | Pierre-Marie Pédrot | |
| 2016-09-08 | Making Proof_global terminator generic in external tactics. | Pierre-Marie Pédrot | |
| 2016-09-08 | Making Hints generic in the use of external tactics. | Pierre-Marie Pédrot | |
| 2016-09-08 | Unplugging Tacexpr in several interface files. | Pierre-Marie Pédrot | |
| 2016-09-08 | Making Vernacexpr independent from Tacexpr. | Pierre-Marie Pédrot | |
| 2016-09-08 | Merge PR #244. | Pierre-Marie Pédrot | |
| 2016-09-07 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2016-09-07 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
| 2016-09-07 | CoqIDE: Errors are sticky (fix #4368) | Enrico Tassi | |
| 2016-09-07 | Removing useless tactic compatibility layer in Rewrite. | Pierre-Marie Pédrot | |
| 2016-09-07 | STM: if_verbose on "Checking task ..." (fix #4058) | Enrico Tassi | |
| 2016-09-07 | ltacprof: rec-calls are coaleshed | Enrico Tassi | |
| 2016-09-07 | micromega : more robust generation of proof terms | Frédéric Besson | |
| - Assert a purely arihtmetic sub-goal that is proved independently by reflexion. (This reduces the stress on the conversion test) - Does not use 'abstract' anymore (more natural proof-term) - Fix a parsing bug (certain terms in Prop where not recognized) | |||
| 2016-09-06 | A proposal to unify the messages given by Test and Print Options (#5062). | Hugo Herbelin | |
| 2016-09-06 | STM: queries give back a dummy safe_id in case of error (#5041) | Enrico Tassi | |
| 2016-09-06 | STM: sideff: report safe_id correctly (fix #4968) | Enrico Tassi | |
| 2016-09-06 | STM: nested Abort is like nested Qed (fix #4756) | Enrico Tassi | |
| There was an "optimization", since Abort is an empty side effect. But that optimization had an impact on the DAG shape. Now a nested proof, no matter if it is kept or dropped, is handled the same. | |||
| 2016-09-05 | coqide: use Document instead of tags to detect sentences to `Skip (#4829) | Enrico Tassi | |
| When one jumps from a focused area to a point after the focused zone, sentences that are already processed (in the Doc.context of the focused area) have not to be processed again (they are tagged as `Skip). Detection of such sentences was based on tags (i.e. colors) that is shaky. Now we use the sentence-marks as stored in the document data structure. | |||
| 2016-09-05 | Test file for #5065 - Anomaly: Not a proof by induction | Maxime Dénès | |
| 2016-09-05 | Fix #5065: Anomaly: Not a proof by induction | Maxime Dénès | |
| Using abstract can create beta-redexes or let-ins in the head of the proof terms. The code projecting out mutual lemmas was not robust enough. | |||
| 2016-09-05 | Fast path in push_rel_context_to_named_context. | Pierre-Marie Pédrot | |
| Essentially, we do not reconstruct the named_context_val when the rel_context is empty. | |||
| 2016-09-05 | profile_ltac: rewritten to be purely functional and STM aware | Enrico Tassi | |
| Changes: - data structures are purely functional (so retracting do work) - profiling data flows towards master using the feedback bus - master aggregates the data on printing | |||
| 2016-09-05 | xml_printer: use sensible names for putc and puts | Enrico Tassi | |
| They used to be called output and output' ... | |||
| 2016-09-05 | feedback: support multiple feedback listeners | Enrico Tassi | |
| So that a module can add his own and look at the traffic | |||
| 2016-09-05 | Summary: simpler API for process-local storage | Enrico Tassi | |
| 2016-09-04 | Do not normalize evars in Eauto.e_give_exact. | Pierre-Marie Pédrot | |
| This is not needed, as the terms are then checked up to unification or convertibility. | |||
| 2016-09-03 | Fixing what is probably a typo in Strict Proofs mode (#5062). | Hugo Herbelin | |
| 2016-09-02 | Fast path in whd_evar. | Pierre-Marie Pédrot | |
| Before computing the whd_evar-form of the arguments of an evar, we first check that it is indeed defined. | |||
| 2016-09-02 | Silence the CAMLP5 warnings on command line. | Pierre-Marie Pédrot | |
| They were mostly useless, and people complained about it. Not that because there is no API to make CAMLP4 silent, a CAMLP4-based Coq will still spit out its share of noisy warnings. | |||
| 2016-09-02 | Remove useless debug code. | Guillaume Melquiond | |
| 2016-09-02 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2016-09-02 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
| 2016-09-01 | Fix test-suite after Frédéric's 6231f07b2. | Maxime Dénès | |
| 2016-09-01 | Fixed Bug #5003 : more careful generalisation of dependent terms. | Frédéric Besson | |
| 2016-09-01 | More efficient data structure to check if a native file is loaded. | Maxime Dénès | |
| Spotted by PMP. | |||
| 2016-09-01 | Notation_ops.subst_glob_vars: substituting also in evar kind for | Hugo Herbelin | |
| consistency of the use of names. | |||
| 2016-09-01 | Short documentation, filling TODO's in evd.mli. | Hugo Herbelin | |
| 2016-09-01 | Fixing call to "lazy beta iota" in "refine" (restoring v8.4 behavior). | Hugo Herbelin | |
| (It was reducing also in hypotheses.) | |||
| 2016-09-01 | Moving log of "TacReduce"/"reduce" to Tactics.reduce so that internal | Hugo Herbelin | |
| calls are logged too. Using appropriate printer for reparsability of the output. | |||
| 2016-09-01 | Fixing name of internal refine ("simple refine"). | Hugo Herbelin | |
| 2016-08-31 | Fix Bug #5005 : micromega tactics is now robust to failure of 'abstract'. | Frédéric Besson | |
| If 'abstract' fails e.g. if there are existentials. The tactic runs an abstract-free alternative. | |||
| 2016-08-31 | Fix bug #5043: [Admitted] lemmas pick up section variables. | Pierre-Marie Pédrot | |
| We add a flag Keep Admitted Variables that allows to recover the legacy v8.4 behaviour of admitted lemmas. The statement of such lemmas did not depend on the current context variables. | |||
| 2016-08-30 | Fix bug #5051: Large outputs are garbled. | Pierre-Marie Pédrot | |
| Instead of relying on the current position of the cursor, we rather use a dedicated mark in the message view. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |