| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-07-07 | In flex-flex cases, the undefinedness of an evar can not be preseved after ↵ | Matthieu Sozeau | |
| converting the stacks. Take care of this by recalling unification. | |||
| 2014-07-07 | Missing check of evar instantiation, resulting in missing constraints (bug ↵ | Matthieu Sozeau | |
| from MathClasses). | |||
| 2014-07-07 | In dest_prod_assum, allow non-toplevel let-reductions (fixes a bug found in ↵ | Matthieu Sozeau | |
| MathClasses). | |||
| 2014-07-05 | Using IStream coiterator to explicit the captured state of tactic matching ↵ | Pierre-Marie Pédrot | |
| results. | |||
| 2014-07-03 | Cleanup code related to the constraint solving, which sits now outside the | Matthieu Sozeau | |
| kernel in library/universes.ml. | |||
| 2014-07-03 | Properly compute the transitive closure of the system of constraints | Matthieu Sozeau | |
| generated by a mutual inductive definition (bug found in CFGV). Actually this code can move out of the kernel. | |||
| 2014-07-03 | Restore proper order of effects in letin_tac_gen. Fixes CFGV again. | Matthieu Sozeau | |
| 2014-07-03 | Fix eta expansion of primitive records (HoTT bug #78), which now fails ↵ | Matthieu Sozeau | |
| cleanly when called on partially applied constructors. Also protect evar_conv from that case. | |||
| 2014-07-03 | Fix Coq_makefile in presence of mlpack | Pierre Boutillier | |
| 2014-07-03 | coqdoc is minimaly -Q aware | Pierre Boutillier | |
| 2014-07-03 | Adding a coiterator to IStream. | Pierre-Marie Pédrot | |
| 2014-07-03 | More efficient implementation of Ltac match, by inlining a stream map. | Pierre-Marie Pédrot | |
| 2014-07-03 | When defining a monomorphic Program, do not allow arbitrary instantiations | Matthieu Sozeau | |
| of the universe context in the obligations, it gets gradually fixed globally by each one of them. Fixes bug found in Misc/Overloading. | |||
| 2014-07-03 | Bug 3405: Coq_makefile: Implicit rules only for listed files in Make file | Pierre Boutillier | |
| 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-02 | Fix a Not_found anomaly raised by solve_evar_evar, we were breaking the | Matthieu Sozeau | |
| invariant that the evar arguments to that function always have to be undefined. | |||
| 2014-07-02 | Indeed simpl never is really honored now. | Matthieu Sozeau | |
| 2014-07-01 | Add toplevel commands to declare global universes and constraints. | Matthieu Sozeau | |
| 2014-07-01 | Patch from Enrico Tassi to get Drop compatible with stm. | Enrico Tassi | |
| 2014-07-01 | Continuing ff9f94634 on making code and doc agree on "Set Equality Schemes" | Hugo Herbelin | |
| 2014-07-01 | Making code and doc agree on "Set Equality Schemes" (see also bug #2550). | Hugo Herbelin | |
| 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-07-01 | More informative message when Mltop.load_object fails. | Hugo Herbelin | |
| 2014-06-30 | Useless keeping of dirpath in tactic aliases. | Pierre-Marie Pédrot | |
| 2014-06-30 | Clarifying 'No such bound variable' message in apply, as suggested in #2387 | Hugo Herbelin | |
| 2014-06-30 | Tests for bugs #2834 and #2994. | Hugo Herbelin | |
| 2014-06-30 | Completing test for bug report #2830 | Hugo Herbelin | |
| 2014-06-30 | Little coqide bug, when coqtop outputs empty lines, as e.g. when calling ↵ | Hugo Herbelin | |
| coqide --help. | |||
| 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-30 | refresh INSTALL | Pierre Boutillier | |
| 2014-06-30 | Coq_makefile takes advantages of -I -Q -R cleanup | Pierre Boutillier | |
| 2014-06-30 | coqc is -Q aware | Pierre Boutillier | |
| 2014-06-30 | Coqdep: update include strategies | Pierre Boutillier | |
| -I is (only) the ml one -I -as is fixed -Q is understood -R is not a recursive ml include anymore $COQENV, user_contrib, ... are not recursively included coqlib/theories and coqlib/plugins are still recursively included (for now). (This may deserves an option) Closes Bug 2910: If there is a "Require a." in a b.v and a a.vo in path but no a.v, coqdep does not complains about a missing a.v. | |||
| 2014-06-30 | Coq_makefile: -extra[-phony] correction + doc | Pierre Boutillier | |
| 2014-06-29 | When building on-the-fly elimination principles, set the predicates universe ↵ | Matthieu Sozeau | |
| variable as algebraic so it can disappear from the proof (it always gets substituted away from the term). This means less spurious universes remaining in proof terms. | |||
| 2014-06-29 | Really honor the [simpl never] flag in whd_simpl, it was still doing ↵ | Matthieu Sozeau | |
| reductions in case the constant was hiding a direct match for example. Also avoid two lookups of ReductionBehavior per constant application in simpl. | |||
| 2014-06-29 | Move Params definition in generalize rewriting out of a section so that | Matthieu Sozeau | |
| its universe doesn't get constrained unnecessarily (bug found in MathClasse). Also avoid using rewrite itself in a proof in Morphisms. | |||
| 2014-06-28 | Quick fix of bug #2996 continued (case of inductive types). | Hugo Herbelin | |
| 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 | Quickly fixing bug #2996: typing functions now check when referring to | Hugo Herbelin | |
| a global reference that the current (goal) env contains all the section variables that the global reference expects to be present. Note that the test for inclusion might be costly: everytime a conversion happens in a section variable copied in a goal, this conversion has to be redone when referring to a constant dependent on this section variable. It is unclear to me whether we should not instead give global names to section variables so that they exist even if they are not listed in the context of the current goal. Here are two examples which are still problematic: Section A. Let B := True : Type. Definition C := eq_refl : B = True. Theorem D : Type. clearbody B. set (x := C). unfold C in x. (* inconsistent context *) or Section A. Let B : Type. exact True. Qed. Definition C := eq_refl : B = True. (* Note that this violated the Qed. *) Theorem D : Type. set (x := C). unfold C in x. (* inconsistent context *) | |||
| 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-28 | Typo in stm error message. | Hugo Herbelin | |
| 2014-06-28 | Updating CHANGES w.r.t. opacity in type inference + layout of file. | Hugo Herbelin | |
| 2014-06-28 | Small short optimization of instantiation in Evd. | Hugo Herbelin | |
| 2014-06-28 | More open in base_include | Hugo Herbelin | |
| 2014-06-27 | Fast path in Canonical structure detection. We do not always compute the normal | Pierre-Marie Pédrot | |
| form of a potential canonical argument anymore, and we check that it may be part of a canonical structure first. | |||
| 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 | Avoid using a deprecated lemma in the standard library. | Guillaume Melquiond | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |