aboutsummaryrefslogtreecommitdiff
path: root/interp
AgeCommit message (Expand)Author
2015-09-16Properly handle {|...|} patterns when patterns are not asymmetric. (Fix bug #...Guillaume Melquiond
2015-08-21Fixing #4318 (anomaly when applying args to a recursive notation in patterns).Hugo Herbelin
2015-07-29Fixing bug #3811: "Universe annotations confused inside generalizing binders".Pierre-Marie Pédrot
2015-07-27Fixing #4305 (compatibility wrt 8.4 in not interpreting anHugo Herbelin
2015-07-08Make sure that scope classes are displayed by Print Scopes. (Fix bug #4262)Guillaume Melquiond
2015-06-26Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"Lionel Rieg
2015-05-27Fix bug #4159Matthieu Sozeau
2015-05-01Fixing computation of implicit arguments by position in fixpoints (#4217).Hugo Herbelin
2015-04-23Remove almost all the uses of string concatenation when building error messages.Guillaume Melquiond
2015-04-21Fixing #3376 and #4191 (wrong index of maximally-inserted implicit argumentHugo Herbelin
2015-04-14Function now supports puniveresjforest
2015-03-30grammar: export hypidentEnrico Tassi
2015-03-27Normalize scope names before storing them in vo files. (Fix for bug #4162)Guillaume Melquiond
2015-03-24Fixing equality of notation_constrs. Fixes bug #4136.Pierre-Marie Pédrot
2015-03-24Revert "Useless check when loading notations through import."Pierre-Marie Pédrot
2015-03-11admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Enrico Tassi
2015-02-27Removing the unused field ltacrecvars of tactic internalization.Pierre-Marie Pédrot
2015-02-21Continuing experimentation on what part of the instance of an evarHugo Herbelin
2015-02-12Univs: fix bug #3978: carry around the universe context used toMatthieu Sozeau
2015-01-17Univs: proper printing of global and local universe names (onlyMatthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2014-12-30Fixing #3892: Ensure that notation variables do not capture namesHugo Herbelin
2014-12-16Getting rid of Exninfo hacks.Pierre-Marie Pédrot
2014-12-11Tentatively more informative report of failure when inferringHugo Herbelin
2014-12-04Reactivating option "Set Printing Existential Instances" for asking printing ...Hugo Herbelin
2014-11-27Reverting the following block of three commits:Hugo Herbelin
2014-11-26Experimenting always forcing convertibility on strict implicit argumentsHugo Herbelin
2014-11-19Printing function for [uconstr].Arnaud Spiwack
2014-11-16Enforcing a stronger difference between the two syntaxes "simplHugo Herbelin
2014-10-22Fixing what really looks like a bug in the initial implementation ofHugo Herbelin
2014-10-20A patch for printing "match" when constructors are defined with let-inHugo Herbelin
2014-09-30Add syntax for naming new goals in refine: writing ?[id] instead of _Hugo Herbelin
2014-09-29Notation: option to attach extra pretty printing rules to notationsEnrico Tassi
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
2014-09-18Fix debug printing with primitive projections.Matthieu Sozeau
2014-09-17Revert specific syntax for primitive projections, avoiding uglyMatthieu Sozeau
2014-09-16More on printing references applied to implicit arguments.Hugo Herbelin
2014-09-12Uniformisation of the order of arguments env and sigma.Hugo Herbelin
2014-09-12Parsing evar instances.Hugo Herbelin
2014-09-12Referring to evars by names. Added a parser for evars (but parsing ofHugo Herbelin
2014-09-10Parsing and printing of primitive projections, fix buggy behavior whenMatthieu Sozeau
2014-09-09- Fix printing and parsing of primitive projections, including the SetMatthieu Sozeau
2014-09-08Fix bug #3591: print differently eta-expanded projection implicit application...Matthieu Sozeau
2014-09-08Parsing of Type@{max(i,j)}.Matthieu Sozeau
2014-09-04Print [Variant] types with the keyword [Variant].Arnaud Spiwack
2014-08-29Simplification of Genarg unpackers.Pierre-Marie Pédrot
2014-08-18Lazy interpretation of patterns so that expressions such as "intros H H'/H"Hugo Herbelin
2014-08-18Adding a new intro-pattern for "apply in" on the fly. Using syntaxHugo Herbelin
2014-08-18Spotted a source of failure of the constr printer in debugger.Hugo Herbelin
2014-08-14Fix non-printing of coercions for primitive projections (fixes bug #3433).Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:00:58 +0000