aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Revert "time tac" (committed by mistake).Gravatar Hugo Herbelin2014-07-07
| | | | This reverts commit abad0a15ac44cb5b53b87382bb4d587d9800a0f6.
* time tacGravatar Hugo Herbelin2014-07-07
|
* Updating README wrt coq-club and ftp.Gravatar Hugo Herbelin2014-07-07
|
* Fix g_coqast for explicit applications.Gravatar Matthieu Sozeau2014-07-07
|
* Coq_makefile: fix cmx compilation when there are both ml and mllibGravatar Pierre Boutillier2014-07-07
|
* In flex-flex cases, the undefinedness of an evar can not be preseved after ↵Gravatar Matthieu Sozeau2014-07-07
| | | | | | converting the stacks. Take care of this by recalling unification.
* Missing check of evar instantiation, resulting in missing constraints (bug ↵Gravatar Matthieu Sozeau2014-07-07
| | | | from MathClasses).
* In dest_prod_assum, allow non-toplevel let-reductions (fixes a bug found in ↵Gravatar Matthieu Sozeau2014-07-07
| | | | MathClasses).
* Using IStream coiterator to explicit the captured state of tactic matching ↵Gravatar Pierre-Marie Pédrot2014-07-05
| | | | results.
* Cleanup code related to the constraint solving, which sits now outside theGravatar Matthieu Sozeau2014-07-03
| | | | kernel in library/universes.ml.
* Properly compute the transitive closure of the system of constraintsGravatar Matthieu Sozeau2014-07-03
| | | | | generated by a mutual inductive definition (bug found in CFGV). Actually this code can move out of the kernel.
* Restore proper order of effects in letin_tac_gen. Fixes CFGV again.Gravatar Matthieu Sozeau2014-07-03
|
* Fix eta expansion of primitive records (HoTT bug #78), which now fails ↵Gravatar Matthieu Sozeau2014-07-03
| | | | | | cleanly when called on partially applied constructors. Also protect evar_conv from that case.
* Fix Coq_makefile in presence of mlpackGravatar Pierre Boutillier2014-07-03
|
* coqdoc is minimaly -Q awareGravatar Pierre Boutillier2014-07-03
|
* Adding a coiterator to IStream.Gravatar Pierre-Marie Pédrot2014-07-03
|
* More efficient implementation of Ltac match, by inlining a stream map.Gravatar Pierre-Marie Pédrot2014-07-03
|
* When defining a monomorphic Program, do not allow arbitrary instantiationsGravatar Matthieu Sozeau2014-07-03
| | | | | | of the universe context in the obligations, it gets gradually fixed globally by each one of them. Fixes bug found in Misc/Overloading.
* Bug 3405: Coq_makefile: Implicit rules only for listed files in Make fileGravatar Pierre Boutillier2014-07-03
|
* In setoid_rewrite, force resolution of the contraints generated by rewriting ↵Gravatar Matthieu Sozeau2014-07-02
| | | | | | | only. Do not mix it with resolution of user-introduced subgoals of typeclass type (bug found in ATBR).
* Fix a Not_found anomaly raised by solve_evar_evar, we were breaking theGravatar Matthieu Sozeau2014-07-02
| | | | invariant that the evar arguments to that function always have to be undefined.
* Indeed simpl never is really honored now.Gravatar Matthieu Sozeau2014-07-02
|
* Add toplevel commands to declare global universes and constraints.Gravatar Matthieu Sozeau2014-07-01
|
* Patch from Enrico Tassi to get Drop compatible with stm.Gravatar Enrico Tassi2014-07-01
|
* Continuing ff9f94634 on making code and doc agree on "Set Equality Schemes"Gravatar Hugo Herbelin2014-07-01
|
* Making code and doc agree on "Set Equality Schemes" (see also bug #2550).Gravatar Hugo Herbelin2014-07-01
|
* Fixing the place where to insert a space in "Tactic failure"Gravatar Hugo Herbelin2014-07-01
| | | | | message. Otherwise, a heading space was missing when calling tclFAIL from ML tactics.
* More informative message when Mltop.load_object fails.Gravatar Hugo Herbelin2014-07-01
|
* Useless keeping of dirpath in tactic aliases.Gravatar Pierre-Marie Pédrot2014-06-30
|
* Clarifying 'No such bound variable' message in apply, as suggested in #2387Gravatar Hugo Herbelin2014-06-30
|
* Tests for bugs #2834 and #2994.Gravatar Hugo Herbelin2014-06-30
|
* Completing test for bug report #2830Gravatar Hugo Herbelin2014-06-30
|
* Little coqide bug, when coqtop outputs empty lines, as e.g. when calling ↵Gravatar Hugo Herbelin2014-06-30
| | | | coqide --help.
* Synchronized names from the "as" clause with the skeleton of theGravatar Hugo Herbelin2014-06-30
| | | | | | elimination scheme in induction/destruct also for those names which correspond to neither the induction hypotheses nor the recursive arguments.
* refresh INSTALLGravatar Pierre Boutillier2014-06-30
|
* Coq_makefile takes advantages of -I -Q -R cleanupGravatar Pierre Boutillier2014-06-30
|
* coqc is -Q awareGravatar Pierre Boutillier2014-06-30
|
* Coqdep: update include strategiesGravatar Pierre Boutillier2014-06-30
| | | | | | | | | | | | | | | -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.
* Coq_makefile: -extra[-phony] correction + docGravatar Pierre Boutillier2014-06-30
|
* When building on-the-fly elimination principles, set the predicates universe ↵Gravatar Matthieu Sozeau2014-06-29
| | | | | | | 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.
* Really honor the [simpl never] flag in whd_simpl, it was still doing ↵Gravatar Matthieu Sozeau2014-06-29
| | | | | | | reductions in case the constant was hiding a direct match for example. Also avoid two lookups of ReductionBehavior per constant application in simpl.
* Move Params definition in generalize rewriting out of a section so thatGravatar Matthieu Sozeau2014-06-29
| | | | | its universe doesn't get constrained unnecessarily (bug found in MathClasse). Also avoid using rewrite itself in a proof in Morphisms.
* Quick fix of bug #2996 continued (case of inductive types).Gravatar Hugo Herbelin2014-06-28
|
* Small refinement about whether it is tolerated for compatibility thatGravatar Hugo Herbelin2014-06-28
| | | | | | 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.
* Quickly fixing bug #2996: typing functions now check when referring toGravatar Hugo Herbelin2014-06-28
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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 *)
* Moved code for finding subterms (pattern, induction, set, generalize, ...)Gravatar Hugo Herbelin2014-06-28
| | | | | | | 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.
* Extra check for indirect dependency when abstracting a term which isGravatar Hugo Herbelin2014-06-28
| | | | | not a variable, in the future objective to factorize code between "generalize dependent" and "set", "destruct", etc.
* Made the subterm finding function make_abstraction independent of theGravatar Hugo Herbelin2014-06-28
| | | | proof engine. Moved it to unification.ml.
* Typo in stm error message.Gravatar Hugo Herbelin2014-06-28
|
* Updating CHANGES w.r.t. opacity in type inference + layout of file.Gravatar Hugo Herbelin2014-06-28
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 21:35:27 +0000