aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/patternops.mli
Commit message (Collapse)AuthorAge
* [api] Misctypes removal: miscellaneous aliases.Gravatar Emilio Jesus Gallego Arias2018-06-12
|
* [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Gravatar Emilio Jesus Gallego Arias2018-05-04
| | | | | | | | | | | | | In #6092, `global_reference` was moved to `kernel`. It makes sense to go further and use the current kernel style for names. This has a good effect on the dependency graph, as some core modules don't depend on library anymore. A question about providing equality for the GloRef module remains, as there are two different notions of equality for constants. In that sense, `KerPair` seems suspicious and at some point it should be looked at.
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|
* Fixing #5401 (printing of patterns with bound anonymous variables).Gravatar Hugo Herbelin2017-10-28
| | | | This fixes also #5731, #6035, #5364.
* [general] Remove Econstr dependency from `intf`Gravatar Emilio Jesus Gallego Arias2017-10-25
| | | | | To this extent we factor out the relevant bits to a new file, ltac_pretype.
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
|
* Quick hack to fix interpretation of patterns in Ltac.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | | | | | | | Interpretation of patterns in Ltac is essentially flawed. It does a roundtrip through the pretyper, and relies on suspicious flagging of evars in the evar source field to recognize original pattern holes. After the pattern_of_constr function was made evar-insensitive, it expanded evars that were solved by magical side-effects of the pretyper, even if it hadn't been asked to perform any heuristics. We backtrack on the insensitivity of the pattern_of_constr function. This may have a performance penalty in other dubious code, e.g. hints. In the long run we should get rid of the pattern_of_constr function.
* Patternops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| |
* | Reduce dependencies of interface files.Gravatar Guillaume Melquiond2016-01-02
|/
* Fix bug #4433, removing hack on evars appearing in a pattern from aGravatar Matthieu Sozeau2015-11-19
| | | | | constr, and the associated signature, not needed anymore. Update CHANGES, no evar_map is produced by pattern_of_constr anymore.
* Fix bug #3590, keeping evars that are not turned into named metas byGravatar Matthieu Sozeau2015-03-03
| | | | | | pattern_of_constr in an evar_map, as they can appear in the context of said named metas, which is used by change. Not sure what to do in the PEvar case, which never matches anyway according to Constr_matching.matches.
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
| | | | | | | | so as to reproduce correctly the reduction behavior of existing projections, i.e. delta + iota. Make [projection] an abstract datatype in Names.ml, most of the patch is about using that abstraction. Fix unification.ml which tried canonical projections too early in presence of primitive projections.
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
| | | | | | | | With ocaml 4.01, the 'unused open' warning also checks the mli :-) Beware: some open are reported as useless when compiling with camlp5, but are necessary for compatibility with camlp4. These open are now marked with a comment.
* Replacing lists by maps in matching interpretation.Gravatar ppedrot2013-06-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16561 85f007b7-540e-0410-9357-904b9bb8a0f7
* Merging Context and Sign.Gravatar ppedrot2013-04-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16463 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modulification of identifierGravatar ppedrot2012-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a constr_pattern_eqGravatar ppedrot2012-11-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15995 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updating headers.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
* global_reference migrated from Libnames to new Globnames, less deps in ↵Gravatar letouzey2012-05-29
| | | | | | grammar.cma git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15384 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pattern as a mli-only file, operations in PatternopsGravatar letouzey2012-05-29
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15376 85f007b7-540e-0410-9357-904b9bb8a0f7