| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-07-25 | A slightly more fine grained way to check whether a TACTIC EXTEND is global ↵ | Arnaud Spiwack | |
| or local to goals. Checks if the arguments need anything from the goal by looking at their tags, if not, the tactic is global. | |||
| 2014-07-24 | Distinguish tactics t1;t2 and t1;[t2..]. | Arnaud Spiwack | |
| They used to be the same (and had a single entry in the AST). But now that t2 can be a multi-goal tactic, t1;[t2..] has the semantics of executing t2 in each goal independently. | |||
| 2014-07-22 | Small code sharing in TacticMatching. | Pierre-Marie Pédrot | |
| 2014-07-21 | Correct eauto which was not dealing properly with polymorphic constants. | Matthieu Sozeau | |
| 2014-07-14 | Redo PMP's patch to rewriting to make it purely functional using state passing. | Matthieu Sozeau | |
| 2014-07-13 | Adding a "time" tactical for benchmarking purposes. In case the tactic | Hugo Herbelin | |
| backtracks, print time spent in each of successive calls. | |||
| 2014-07-10 | check_for_interrupt: better (but slower) in threading mode | Enrico Tassi | |
| Experimenting with PIDE I discovered that yield is not sufficient to have a rescheduling, hence the delay. | |||
| 2014-07-10 | Fix a oversight in 5bf9e67b . | Arnaud Spiwack | |
| 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. | |||
| 2014-07-07 | Revert "time tac" (committed by mistake). | Hugo Herbelin | |
| This reverts commit abad0a15ac44cb5b53b87382bb4d587d9800a0f6. | |||
| 2014-07-07 | time tac | Hugo Herbelin | |
| 2014-07-05 | Using IStream coiterator to explicit the captured state of tactic matching ↵ | Pierre-Marie Pédrot | |
| results. | |||
| 2014-07-03 | Restore proper order of effects in letin_tac_gen. Fixes CFGV again. | Matthieu Sozeau | |
| 2014-07-03 | More efficient implementation of Ltac match, by inlining a stream map. | Pierre-Marie Pédrot | |
| 2014-07-02 | In setoid_rewrite, force resolution of the contraints generated by rewriting ↵ | Matthieu Sozeau | |
| only. Do not mix it with resolution of user-introduced subgoals of typeclass type (bug found in ATBR). | |||
| 2014-07-01 | Fixing the place where to insert a space in "Tactic failure" | Hugo Herbelin | |
| message. Otherwise, a heading space was missing when calling tclFAIL from ML tactics. | |||
| 2014-06-30 | Useless keeping of dirpath in tactic aliases. | Pierre-Marie Pédrot | |
| 2014-06-30 | Synchronized names from the "as" clause with the skeleton of the | Hugo Herbelin | |
| elimination scheme in induction/destruct also for those names which correspond to neither the induction hypotheses nor the recursive arguments. | |||
| 2014-06-28 | Small refinement about whether it is tolerated for compatibility that | Hugo Herbelin | |
| or-and intropatterns bind a limited number of patterns: if * or ** are used, the bound has to be used (since there is no heavy compatibility to respect for * and **). This fixes test-suite/success/intros.v. | |||
| 2014-06-28 | Moved code for finding subterms (pattern, induction, set, generalize, ...) | Hugo Herbelin | |
| 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. | |||
| 2014-06-28 | Extra check for indirect dependency when abstracting a term which is | Hugo Herbelin | |
| not a variable, in the future objective to factorize code between "generalize dependent" and "set", "destruct", etc. | |||
| 2014-06-28 | Made the subterm finding function make_abstraction independent of the | Hugo Herbelin | |
| proof engine. Moved it to unification.ml. | |||
| 2014-06-27 | Add an init_setoid check in rewrite to avoid trying to get undefined references. | Matthieu Sozeau | |
| Fixes the behavior of reflexivity/symmetry etc... when Setoid is not loaded. | |||
| 2014-06-26 | Properly refresh the local hintdb database in case an external tactic changed | Matthieu Sozeau | |
| the hypotheses in eauto. | |||
| 2014-06-25 | Incorrect folding of evars in let_tac_gen made remember fail to store | Matthieu Sozeau | |
| correct constraints (bug found in CFGV). | |||
| 2014-06-25 | In rewrite, wrong computation of the sort of the term to be rewritten in | Matthieu Sozeau | |
| generated an uncaught Not_found. This raises an anomaly now and the sort is properly computed now (fixes a bug in CoLoR). | |||
| 2014-06-25 | In exact check, use e_type_of to ensure that universe constraints necessary | Matthieu Sozeau | |
| to typecheck the term are not forgotten. (relieves tactic implementors from calling e_type_of themselves, e.g. in congruence). Fixes a bug found in Containers. | |||
| 2014-06-24 | Fix program cases and inversion tactic to correctly record universe constraints. | Matthieu Sozeau | |
| Fixes FingerTree contrib. | |||
| 2014-06-24 | Clenvtac.clenv_refine in the new monad. Not satisfactory though, because it | Pierre-Marie Pédrot | |
| exhibits the "useless goal" behaviour: there is code out there depending on the fact that goals cannot be solved by side effects. | |||
| 2014-06-24 | Clenvtac.res_pf is in the new tactic monad. | Pierre-Marie Pédrot | |
| 2014-06-23 | Clenvtac.unify is in the new monad. | Pierre-Marie Pédrot | |
| 2014-06-23 | Removing opens to Clenvtac to track its use more easily. | Pierre-Marie Pédrot | |
| 2014-06-23 | Oops, I fixed the .ml's | Matthieu Sozeau | |
| 2014-06-23 | Fix semantics of change p with c to typecheck c at each specific occurrence ↵ | Matthieu Sozeau | |
| of p, avoiding unwanted universe constraints in presence of universe polymorphic constants. Fixing HoTT bugs # 36, 54 and 113. | |||
| 2014-06-22 | Less goal-entering. | Pierre-Marie Pédrot | |
| 2014-06-21 | Reindex section variables for typeclass resolution if their type changed. | Matthieu Sozeau | |
| Fixes bug #3331. | |||
| 2014-06-20 | Allow more relaxed conversion between the types of the two terms of a rewrite | Matthieu Sozeau | |
| equation, fix uncaught exception in setoid_rewrite (bug #3336). | |||
| 2014-06-20 | Add an e_type_of to avoid losing universe constraints. | Matthieu Sozeau | |
| 2014-06-19 | Adding a raw_goals primitive for Tacinterp. | Pierre-Marie Pédrot | |
| 2014-06-19 | - Fix bug in unification, not only named metas are turned into evars (e.g. ↵ | Matthieu Sozeau | |
| in Ssreflect). - Fix is_applied_rewrite_relation to look for propositional relations. | |||
| 2014-06-18 | Proofs now take and return an evar_universe_context, simplifying interfaces | Matthieu Sozeau | |
| and avoiding explicit substitutions and merging of contexts, e.g. in obligations.ml. The context produced by typechecking a statement is passed in the proof, allowing the universe name context to be correctly folded as well. Mainly an API cleanup. | |||
| 2014-06-17 | Removing dead code. | Pierre-Marie Pédrot | |
| 2014-06-17 | Improve hotspot in Auto. | Pierre-Marie Pédrot | |
| 2014-06-13 | Check resolution of Metas turned into Evars by pose_all_metas_as_evars | Hugo Herbelin | |
| in unification.ml in case prefix 'e' of "apply" and co is not given. | |||
| 2014-06-12 | Passing some tactics to the new monad type. | Pierre-Marie Pédrot | |
| 2014-06-11 | Fix bug #3291, stack overflow in rewrite. | Matthieu Sozeau | |
| 2014-06-11 | Fix bug #3289 | Matthieu Sozeau | |
| 2014-06-11 | In generalized rewrite, avoid retyping completely and constantly the ↵ | Matthieu Sozeau | |
| conclusion, and results of unifying the lemma with subterms. Using Retyping.get_type_of instead results in 3x speedup in Ncring_polynom. | |||
| 2014-06-11 | fix handling of side effects in abstract (fixes QArithSternBrocot) | Enrico Tassi | |
| The right fix should probably be to remove the build_constant_by_tactic function and only use the build_by_tactic one | |||
| 2014-06-08 | Moving hook code from Future to Lemmas. This seemed to disrupt compilation of | Pierre-Marie Pédrot | |
| the checker, and it was not used before that anyway. | |||
| 2014-06-08 | Enforce a correct exception handling in declaration_hooks | Enrico Tassi | |
| This should finally get rid of the following class of bugs: Qed fails, STM undoes to the beginning of the proof because the exception is not annotated with the correct state, PG gets out of sync because errors always refer to the last command in PGIP. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |