| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-07-30 | Fix discrimination net which was not recognizing primitive projections. | Matthieu Sozeau | |
| 2014-07-29 | Untyped terms in tactic: add the possibility to use a typed term inside an ↵ | Arnaud Spiwack | |
| untyped term. | |||
| 2014-07-29 | Untyped terms in tactic: function [type_term c] to give a typed version of [c]. | Arnaud Spiwack | |
| 2014-07-29 | Add a type of untyped term to Ltac's value. | Arnaud Spiwack | |
| It is meant to avoid intermediary retyping when a term is built in Ltac. See #3218. The implementation makes a small modification in Constrintern: now the main internalisation function can take an extra substitution from Ltac variables to glob_constr and will apply the substitution during the internalisation. | |||
| 2014-07-29 | Clean up obsolete comment. | Arnaud Spiwack | |
| 2014-07-28 | CPS-style tactic matching. We use the tactic monad as the target of the CPS. | Pierre-Marie Pédrot | |
| This allows for tail-rec calls, prevents unwanted capture of closures and results in an overall more efficient evaluation. | |||
| 2014-07-27 | Code cleaning in Tacenv. | Pierre-Marie Pédrot | |
| 2014-07-27 | Qualified ML tactic names. The plugin name is used to discriminate | Pierre-Marie Pédrot | |
| potentially conflicting tactics names from different plugins. | |||
| 2014-07-25 | Removing dead code relative to or_metaid. | Pierre-Marie Pédrot | |
| 2014-07-25 | Add a tactic [swap i j] to swap the position of goals [i] and [j]. | Arnaud Spiwack | |
| If [i] or [j] is negative goals are counted from the end. | |||
| 2014-07-25 | Adds a cycle tactic to reorder goals in a loop. | Arnaud Spiwack | |
| [cycle 1] puts the first goal last, [cycle -1] puts the last goal first, [cycle n] is like [do n cycle 1], [cycle -n] is like [do n cycle -1]. | |||
| 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. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |