| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-04-15 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-04-14 | Cleaning up the implementation of search entries in Hints. | Pierre-Marie Pédrot | |
| 2015-04-14 | Opaque implementation of auto tactics. | Pierre-Marie Pédrot | |
| We provide an eliminator ensuring that the AST will be used to build a tactic, so that we can stuff arbitrary things inside. An escape function is also provided for backward compatibility. | |||
| 2015-04-13 | Remove declarations of matched variables in change as an extension of | Matthieu Sozeau | |
| the context... overlooked by my last commit. Fixes relation-algebra. | |||
| 2015-04-13 | More documented representation of hint objects. | Pierre-Marie Pédrot | |
| 2015-04-12 | Making the hint entry type opaque. | Pierre-Marie Pédrot | |
| 2015-04-10 | Fix compilation broken by Matthieu's last commit. | Pierre Letouzey | |
| Btw, also unset the READABLE_ML4 option, which probably caused this issue. No, we normally do *not* want to see the internals of .ml generated out of a .ml4 (except during some specific debug sessions). It is *so* easy otherwise to edit the wrong .ml by mistake and forget to edit the original .ml4. | |||
| 2015-04-10 | Fix #3590 for good this time, by changing the API, change's argument now | Matthieu Sozeau | |
| takes a variable substitution for matched variables in the (lhs) pattern, and uses the existing ist structure to pretype the rhs correcly, without having to deal with the volatile evars. | |||
| 2015-04-10 | Eauto hints respect their priority. Fixes bug #3199. | Pierre-Marie Pédrot | |
| This patch changes the semantics of eauto w.r.t. to extern hints, so it may break some code out there. There is no compatibility flag because this is a real bug, and we do not really want the users to depend on this. Moreover, there are still some fishy parts in the current implementation that should be rewritten for the next release. | |||
| 2015-04-10 | Making the hints for the auto tactics private. | Pierre-Marie Pédrot | |
| They are all generated by the Hints module, and making them purely opaque is not worthwhile because we project them a lot. This ensures that they all get generated following a uniform process. | |||
| 2015-04-09 | Merge branch 'v8.5' into trunk | Pierre Letouzey | |
| 2015-04-09 | Fix caching of local hintdb in typeclasses eauto. | Matthieu Sozeau | |
| 2015-04-06 | refresh metas in rewrite hints loaded from .vo files (fix bug #3815) | Nickolai Zeldovich | |
| Meta variables in rewrite rules are named by integers that are allocated sequentially at runtime (fresh_meta in tactics/term_dnet.ml). This causes a problem when some rewrite rules (with meta variables) are generated by coqc, saved in a .vo file, and then imported into another coqc/coqtop process. The new process will allocate its own meta variable numbers starting from 0, colliding with existing imported meta variable numbers. One manifestation of this issue was various failures of [rewrite_strat]; see bug #3815 for examples. This change fixes the problem, by replacing all meta variable numbers in imported rewrite rules at import time. This seems to fix the various failures reported in bug #3815. Thanks to Jason Gross for tracking down the commit that introduced this bug in the first place (71a9b7f2). | |||
| 2015-04-01 | Removing a probably incorrect on-the-fly require in a tactic. | Pierre-Marie Pédrot | |
| Also removed the require function it was using, as it is absent from the remaining of the code. | |||
| 2015-03-23 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-03-22 | Aliasing give_up with admit | Enrico Tassi | |
| 2015-03-11 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-03-11 | admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032) | Enrico Tassi | |
| - no more inconsistent Axiom in the Prelude - STM can now process Admitted proofs asynchronously - the quick chain can stock "Admitted" jobs in .vio files - the vio2vo step checks the jobs but does not stock the result in the opaque tables (they have no slot) - Admitted emits a warning if the proof is complete - Admitted uses the (partial) proof term to infer section variables used (if not given with Proof using), like for Qed - test-suite: extra line Require TestSuite.admit to each file making use of admit - test-suite/_CoqProject: to pass to CoqIDE and PG the right -Q flag to find TestSuite.admit | |||
| 2015-03-07 | Reverting r10021 which enforces early assumptions on freshness which | Hugo Herbelin | |
| seem to be overly strong in practice (see discussion related to #4035). | |||
| 2015-03-07 | Continuing a8ad3abc15a2 and 60810aaec on freshness of name in tactic "evar". | Hugo Herbelin | |
| Not inventing a new fresh name if a non-fresh name is explicitly given, as in v8.4. | |||
| 2015-03-04 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-03-03 | Fix bug #3590, keeping evars that are not turned into named metas by | Matthieu Sozeau | |
| pattern_of_constr in an evar_map, as they can appear in the context of said named metas, which is used by change. Not sure what to do in the PEvar case, which never matches anyway according to Constr_matching.matches. | |||
| 2015-02-28 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-02-27 | Removing the unused field ltacrecvars of tactic internalization. | Pierre-Marie Pédrot | |
| 2015-02-27 | Hack so that refine_no_check accepts an argument which is a match on an | Hugo Herbelin | |
| inductive type with let-in in the arity (until logic.ml disappears). | |||
| 2015-02-27 | Somehow fixing bug #3467. | Pierre-Marie Pédrot | |
| The notations using tactics in term seem now not to respect globalized names. It is not obvious that this is the expected behaviour, but at least it does not die with an anomaly. | |||
| 2015-02-26 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-02-26 | Fixing bug #3298. | Pierre-Marie Pédrot | |
| 2015-02-26 | Fixing printing of ordinals. | Pierre-Marie Pédrot | |
| 2015-02-24 | [info_auto] & [info_trivial]: warning message to help users find [Info]. | Arnaud Spiwack | |
| 2015-02-24 | [info] tactical warning: do not suggest [info_auto] and [info_trivial]. | Arnaud Spiwack | |
| Since they don't work anymore. | |||
| 2015-02-23 | Merge branch 'v8.5' into trunk | Enrico Tassi | |
| 2015-02-23 | Fix some typos in comments. | Guillaume Melquiond | |
| 2015-02-23 | Less compatibility layer in Eauto. | Pierre-Marie Pédrot | |
| 2015-02-23 | Partially porting eauto to the new tactic API. | Pierre-Marie Pédrot | |
| 2015-02-23 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-02-20 | Fixing error message when H already exists in tactic subexpression eqn:H. | Hugo Herbelin | |
| 2015-02-20 | A fix for #3993 (not fully applied term to destruct when eqn is given). | Hugo Herbelin | |
| 2015-02-18 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-02-18 | Fix bug #3938 | Matthieu Sozeau | |
| 2015-02-16 | Fixing bug #3944. | Pierre-Marie Pédrot | |
| 2015-02-15 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-02-14 | Fixing bug #4016. | Pierre-Marie Pédrot | |
| When setoid rewriting in a hypothesis, we push the newly introduced declaration after the last declaration it depends on. | |||
| 2015-02-13 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-02-12 | Univs: fix bug #4031: wrong folding of sigma in change. | Matthieu Sozeau | |
| 2015-02-12 | Fix bug #2775: Correct handling of universes in leminv. | Matthieu Sozeau | |
| 2015-02-12 | Fixing compilation for 3.12. | Pierre-Marie Pédrot | |
| 2015-02-12 | Tentative fix for bug #4027. | Pierre-Marie Pédrot | |
| 2015-02-11 | Missing space in error message | Matěj Grabovský | |
| 2015-02-11 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |