| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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. | |||
| 2014-06-07 | Adding a new Control file centralizing the control options of Coq. | Pierre-Marie Pédrot | |
| 2014-06-06 | Preserve compatibility on examples such as "intros []." on goals such | Hugo Herbelin | |
| as "forall x:nat*nat, x=x", which resulted in "forall n n0 : nat, (n, n0) = (n, n0)" before commit 37f68259ab0a33c3b5b41de70b08422d9bcd3bec on "Fixing introduction patterns * and ** ". | |||
| 2014-06-06 | Fixes the lost evars when interpreting a change with pattern tactic. | Arnaud Spiwack | |
| 2014-06-06 | Moving the [split] tactic out of the AST. | Pierre-Marie Pédrot | |
| 2014-06-04 | Collecting in Namegen those conventional default names that are used in ↵ | Hugo Herbelin | |
| different places | |||
| 2014-06-04 | - Fix hashing of levels to get the "right" order in universe contexts etc... | Matthieu Sozeau | |
| - Add a tentative syntax for specifying universes: Type{"i"} and foo@{Type{"i"},Type{"j"}}. These are always rigid. - Use level-to-level substitutions where the more general level-to-universe substitutions were previously used. | |||
| 2014-06-03 | The tactic interpreter now uses a new type of tactics, through | Pierre-Marie Pédrot | |
| the GTac module. A ['a Gtac.t] is a special case of tactic that may depend on the current goals, or not. Internally, it construct a list of results, one for each focussed goal, if the tactic is actually dependent. This allows for an interpretation of whole-goal tactic that does work, which was not the case for the previous implementation, which did to many Proofview.Goal.enter. | |||
| 2014-06-02 | Removing symmetry from the atomic tactics. | Pierre-Marie Pédrot | |
| 2014-05-31 | More on injection over a projectable "existT". - Fixing syntax "injection ↵ | Hugo Herbelin | |
| ... as ..." which was not working. - Now applying the simplification on any "existT" generated by "injection" (possible source of incompatibilities). | |||
| 2014-05-31 | Fixing introduction patterns * and ** when used in a branch so that they do ↵ | Hugo Herbelin | |
| not introduce beyond what is under control of the branch. See test-suite intros.v for an example. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |