aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
Commit message (Expand)AuthorAge
* CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-29
|\
| * Implement support for universe binder lists in Instance and Program Fixpoint/...Gravatar Matthieu Sozeau2016-01-23
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Getting rid of the awkward unpack mechanism from Genarg.Gravatar Pierre-Marie Pédrot2016-01-17
* | Temporary commit getting rid of Obj.magic unsafety for Genarg.Gravatar Pierre-Marie Pédrot2016-01-17
* | Removing constr generic argument.Gravatar Pierre-Marie Pédrot2016-01-14
* | Removing ident and var generic arguments.Gravatar Pierre-Marie Pédrot2016-01-14
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-13
|\|
| * Fixing #4467 (continued).Gravatar Hugo Herbelin2016-01-13
| * Fixing #4467 (missing shadowing of variables in cases pattern).Gravatar Hugo Herbelin2016-01-12
* | CLEANUP: removing unused fieldGravatar Matej Kosik2016-01-11
* | mergeGravatar Matej Kosik2016-01-11
|\ \
| * | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
* | | Remove some unused functions.Gravatar Guillaume Melquiond2016-01-02
* | | Merge branch 'v8.5' into trunkGravatar Guillaume Melquiond2015-12-31
|\ \ \ | | |/ | |/|
* | | Do not compose List.length with List.filter.Gravatar Guillaume Melquiond2015-12-31
| * | Do not dump a glob reference when its location is ghost. (Fix bug #4469)Gravatar Guillaume Melquiond2015-12-31
* | | Removing the special status of open_constr generic argument.Gravatar Pierre-Marie Pédrot2015-12-28
* | | Tentative API fix for tactic arguments to be fed to tclWITHHOLES.Gravatar Pierre-Marie Pédrot2015-12-27
* | | Do not compose "str" and "to_string" whenever possible.Gravatar Guillaume Melquiond2015-12-22
* | | Removing ad-hoc interpretation rules for tactic notations and their genarg.Gravatar Pierre-Marie Pédrot2015-12-21
* | | Sharing toplevel representation for several generic types.Gravatar Pierre-Marie Pédrot2015-12-21
* | | Changing the toplevel type of the int_or_var generic type to int.Gravatar Pierre-Marie Pédrot2015-12-21
* | | Removing the now useless genarg generic argument.Gravatar Pierre-Marie Pédrot2015-12-21
| |/ |/|
* | CLEANUP: the definition of the "Constrexpr.case_expr" type was simplifiedGravatar Matej Kosik2015-12-18
* | Getting rid of some hardwired generic arguments.Gravatar Pierre-Marie Pédrot2015-12-17
|/
* Fix a bug in externalisation which prevented printing of projectionsGravatar Matthieu Sozeau2015-12-02
* Make the pretty printer resilient to incomplete nametab (progress on #4363).Gravatar Enrico Tassi2015-11-26
* Fixing bug #3554: Anomaly: Anonymous implicit argument.Gravatar Pierre-Marie Pédrot2015-11-11
* Documenting a bit more interpretation functions in passing.Gravatar Hugo Herbelin2015-10-26
* Fix some typos.Gravatar Guillaume Melquiond2015-10-13
* Properly handle {|...|} patterns when patterns are not asymmetric. (Fix bug #...Gravatar Guillaume Melquiond2015-09-16
* Fixing #4318 (anomaly when applying args to a recursive notation in patterns).Gravatar Hugo Herbelin2015-08-21
* Fixing bug #3811: "Universe annotations confused inside generalizing binders".Gravatar Pierre-Marie Pédrot2015-07-29
* Fixing #4305 (compatibility wrt 8.4 in not interpreting anGravatar Hugo Herbelin2015-07-27
* Make sure that scope classes are displayed by Print Scopes. (Fix bug #4262)Gravatar Guillaume Melquiond2015-07-08
* Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"Gravatar Lionel Rieg2015-06-26
* Fix bug #4159Gravatar Matthieu Sozeau2015-05-27
* Fixing computation of implicit arguments by position in fixpoints (#4217).Gravatar Hugo Herbelin2015-05-01
* Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
* Fixing #3376 and #4191 (wrong index of maximally-inserted implicit argumentGravatar Hugo Herbelin2015-04-21
* Function now supports puniveresGravatar jforest2015-04-14
* grammar: export hypidentGravatar Enrico Tassi2015-03-30
* Normalize scope names before storing them in vo files. (Fix for bug #4162)Gravatar Guillaume Melquiond2015-03-27
* Fixing equality of notation_constrs. Fixes bug #4136.Gravatar Pierre-Marie Pédrot2015-03-24
* Revert "Useless check when loading notations through import."Gravatar Pierre-Marie Pédrot2015-03-24
* admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Gravatar Enrico Tassi2015-03-11
* Removing the unused field ltacrecvars of tactic internalization.Gravatar Pierre-Marie Pédrot2015-02-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 19:25:57 +0000