aboutsummaryrefslogtreecommitdiff
path: root/interp/constrintern.ml
AgeCommit message (Expand)Author
2020-11-20Enforcing when a binding variable has no explicit type in constr_notation.Hugo Herbelin
2020-11-20A step towards supporting pattern cast deeplier.Hugo Herbelin
2020-11-20Add preliminary support for notations with large class (non-recursive) binders.Hugo Herbelin
2020-11-20Rewriting convoluted code of set_var_scope in constrintern.ml.Hugo Herbelin
2020-11-20Merge PR #13360: Fix incorrect name refreshing when interning a generalized b...coqbot-app[bot]
2020-11-17Merge PR #13390: Intern application arguments in left-to-right ordercoqbot-app[bot]
2020-11-17Merge PR #12653: Syntax for specifying cumulative inductivescoqbot-app[bot]
2020-11-16Fix incorrect name refreshing when interning a generalized binderGaëtan Gilbert
2020-11-16Merge PR #12685: Propagating scope information in indirect application to a r...Pierre-Marie Pédrot
2020-11-16Syntax for specifying cumulative inductivesGaëtan Gilbert
2020-11-15Intern application arguments in left-to-right orderGaëtan Gilbert
2020-11-15Fixes #11816: using {wf ...} in a local fixpoint is an error, not an anomaly.Hugo Herbelin
2020-11-15Propagating scope information in indirect application to a reference.Hugo Herbelin
2020-11-12Merge PR #13289: Cosmetic cleaning of uState.ml: a bit of doc, more unity in ...Pierre-Marie Pédrot
2020-11-06Merge PR #13255: Fixes #13244: support for coercions in Searchcoqbot-app[bot]
2020-11-05Minor cut elimination in the code of constrintern.ml.Hugo Herbelin
2020-11-05Accept local variables in mixed terms and binders of notations.Hugo Herbelin
2020-11-05Passing full interning env to pattern interning, for better control.Hugo Herbelin
2020-11-05Notations: Giving a consistent role to global references occurring patterns.Hugo Herbelin
2020-11-04Typing patterns and using type constraints in Search.Hugo Herbelin
2020-11-04Adding a typed interpretation of patterns.Hugo Herbelin
2020-11-04Factorizing UState.make* through UState.from_env, to highlight the similarity.Hugo Herbelin
2020-11-04Moving interpretation of user-level universes in constrintern.ml.Hugo Herbelin
2020-10-30Renaming Numeral into NumberPierre Roux
2020-10-10Add location in existential variable names (CEvar/GEvar).Hugo Herbelin
2020-09-30interp_context_evars: removed unused [shift] argumentGaëtan Gilbert
2020-08-15Document semantic restriction on patternsJim Fehrle
2020-07-17Merge PR #12631: Fix record pattern interpretation with implicit argumentsEmilio Jesus Gallego Arias
2020-07-06Primitive persistent arraysMaxime Dénès
2020-07-03Fix #11121: Simultaneous definition of term and notation in custom grammarMaxime Dénès
2020-07-02Fix record pattern interpretation with implicit argumentsGaëtan Gilbert
2020-05-15[interp] Register printers for InternalizationError instead of ad-hoc hanlding.Emilio Jesus Gallego Arias
2020-05-15[misc] Better preserve backtraces in several modulesEmilio Jesus Gallego Arias
2020-05-14Merge PR #11922: No more local reduction functions in Reductionops.Maxime Dénès
2020-05-13Extending support for mixing binders and terms in abbreviations.Hugo Herbelin
2020-05-10No more local reduction functions in Reductionops.Pierre-Marie Pédrot
2020-04-21Fixing #3451: coqdoc links for projections of tuples rather than for construc...Hugo Herbelin
2020-04-21Constrintern: another reworking of the interning of records.Hugo Herbelin
2020-04-21Constrintern.ml: simplifying the interning of record tuples.Hugo Herbelin
2020-04-15Coqdoc: Exporting location and unique id for binding variables.Hugo Herbelin
2020-04-15Making type interning_data abstract in constrintern.ml.Hugo Herbelin
2020-04-15Small convenient code factorization in constrintern.ml.Hugo Herbelin
2020-04-13Close #11935: section variables do not have universe instances.Gaëtan Gilbert
2020-03-31Remove check_hidden_implicit_parameters (not needed anymore)Gaëtan Gilbert
2020-03-31Remove special case for implicit inductive parametersMaxime Dénès
2020-03-22Centralizing all kinds of numeral string management in numTok.ml.Hugo Herbelin
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-02-25Fixing residual bug of #11120.Hugo Herbelin
2020-02-22Fixes #4690: do not allow @f in notations when f is a notation variable.Hugo Herbelin
2020-02-22Inherit arguments scopes in pattern notations bound to some @id.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 05:29:47 +0000