aboutsummaryrefslogtreecommitdiff
path: root/interp/topconstr.mli
AgeCommit message (Collapse)Author
2018-05-30[api] Remove deprecated objects in engine / interp / libraryEmilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-22[ast] Improve precision of Ast location recognition in serialization.Emilio Jesus Gallego Arias
We follow the suggestions in #402 and turn uses of `Loc.located` in `vernac` into `CAst.t`. The impact should be low as this change mostly affects top-level vernaculars. With this change, we are even closer to automatically map a text document to its AST in a programmatic way.
2017-11-19[parser] Remove unnecessary statically initialized hook.Emilio Jesus Gallego Arias
Addded by c6d9d4fb142ef42634be25b60c0995b541e86629 ["Adding ability to put any pattern in binders, prefixed by a quote."] its current placement as well as the hook don't make a lot of sense. In particular, they prevent parts of Coq working without linking the parser. To this purpose, we need to consolidate the `Constrexpr` utilities. While we are at it we do so and remove the `Topconstr` module which is fully redundant with `Constrexpr_ops`.
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-04-25[location] Make location optional in Loc.locatedEmilio Jesus Gallego Arias
This completes the Loc.ghost removal, the idea is to gear the API towards optional, but uniform, location handling. We don't print <unknown> anymore in the case there is no location. This is what the test suite expects. The old printing logic for located items was a bit inconsistent as it sometimes printed <unknown> and other times it printed nothing as the caller checked for `is_ghost` upstream.
2017-03-24Renaming local_binder into local_binder_expr.Hugo Herbelin
This is a bit long, but it is to keep a symmetry with constr_expr.
2016-09-21Fix an error-prone error API.Pierre-Marie Pédrot
2016-08-19Unify location handling of error functions.Emilio Jesus Gallego Arias
In some cases prior to this patch, there were two cases for the same error function, one taking a location, the other not. We unify them by using an option parameter, in the line with recent changes in warnings and feedback. This implies a bit of clean up in some places, but more importantly, is the preparation for subsequent patches making `Loc.location` opaque, change that could be use to improve modularity and allow a more functional implementation strategy --- for example --- of the beautifier.
2016-04-27Reformatting + removal of some useless data + some cut-eliminationHugo Herbelin
in interning of patterns. No semantic changes (except the type of ids_of_cases_indtype).
2016-03-12A more explicit name to the asymmetric boolean flag.Hugo Herbelin
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
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.
2013-09-02Removing more association lists in Constrintern.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16757 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-13Modules and ppvernac, sequel of Enrico's commit 16261letouzey
After some investigation, I see no reason to try to hack the nametab in ppvernac, since everything happens there at a lower level (constr_expr). So the offending code that Enrico protected with a State.with_state_protection is now gone. By the way, moved some types from Declaremods to Vernacexpr to avoid some dependencies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16300 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-14Modulification of identifierppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-08Updating headers.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
were closed (i.e. the only remaining ones are those of printing/parsing). Meanwhile, a simplified interface is provided in loc.mli. This also permits to put Pp in Clib, because it does not depend on CAMLP4/5 anymore. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15475 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29remove many excessive open Util & Errors in mli'sletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15392 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29Basic stuff about constr_expr migrated from topconstr to constrexpr_opsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15382 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29Stuff about notation_constr (ex-aconstr) now in notation_ops.mlletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15381 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstrletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15375 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
Corresponding operations in locusops.ml and miscops.ml The type of occurrences is now a clear algebraic one instead of a bool*list hard to understand. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15372 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evdletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15371 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-15Notations are back in the "in" clause of pattern matching.pboutill
Fixes the test-suite. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15324 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-12"A -> B" is a notation for "forall _ : A, B".pboutill
No good reason for that except uniformity so revert this commit if you find a reason against it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15146 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-20Fixing bug #2724 (using notations with binders in cases patternsherbelin
was provoking an anomaly instead of a regular error). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15070 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-02Glob_term.predicate_pattern: No number of parameters with letins.pboutill
Detyping is wrong about it and as far as I understand no one but Constrextern uses it. Constrextern has now the same machinery for all patterns. Revert if I miss something. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15022 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-02Noise for nothingpboutill
Util only depends on Ocaml stdlib and Utf8 tables. Generic pretty printing and loc functions are in Pp. Generic errors are in Errors. + Training white-spaces, useless open, prlist copies random erasure. Too many "open Errors" on the contrary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-29In the syntax of pattern matching, "in" clauses are patterns.pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15000 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-19Boolean Option Patterns Compatibilitypboutill
switch between "all arguments no parameters" and "explicit params and args" for constructor arguments in patterns. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14919 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-16Parameters in pattern first step.pboutill
In interp/constrintern.ml, '_' for constructor parameter are required if you use AppExpl ('@Constr') and added in order to be erased at the last time if you do not use '@'. It makes the use of notation in pattern more permissive. For example, -8<------ Inductive I (A: Type) : Type := C : A -> I A. Notation "x <: T" := (C T x) (at level 38). Definition uncast A (x : I A) := match x with | x <: _ => x end. -8<------ was forbidden. Backward compatibility is strictly preserved expect for syntactic definitions: While defining "Notation SOME = @Some", SOME had a special treatment and used to be an alias of Some in pattern. It is now uniformly an alias of @Some ('_' must be provided for parameters). In interp/constrextern.ml, except if all the parameters are implicit and all the arguments explicit (This covers all the cases of the test-suite), pattern are generated with AppExpl (id est '@') (so with '_' for parameters) in order to become compatible in any case with future behavior. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14909 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-28Remove dynamic stuff from constr_expr and glob_constrglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14621 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-30Quick improvement of some error messages related to module applicationherbelin
(localization of the error and hopefully improved messages) [Is there a reason why the restriction is not enforced at the parsing level? Anyway, treating it at interpretation time allows more appropriate messages] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14422 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-22Add a syntax entry for fully applied constructor patternpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14292 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-12Rather quick hack to avoid using notations involving "Type" whenherbelin
Universes Printing is on. Code of Topconstr.match_ becomes a bit cluttered, used abbreviation to shorten it (just) a little. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14189 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-02-11Annotations at functor applications:letouzey
- The experimental syntax "<30>F M" is transformed into "F M [inline at level 30]" - The earlier syntax !F X should now be written "F X [no inline]" (note that using ! is still possible for compatibility) - A new annotation "F M [scope foo_scope to bar_scope]" allow to substitute foo_scope by bar_scope in all arguments scope of objects in F. BigN and BigZ are cleaned from the zillions of Arguments Scope used earlier. Arguments scope for lemmas are fixed for instances of Numbers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13839 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-31A fine-grain control of inlining at functor application via priority levelsletouzey
As said in CHANGES: << The inlining done during application of functors can now be controlled more precisely. In addition to the "!F G" syntax preventing any inlining, we can now use a priority level to select parameters to inline : "<30>F G" means "only inline in F the parameters whose levels are <= 30". The level of a parameter can be fixed by "Parameter Inline(30) foo". When levels aren't given, the default value is 100. One can also use the flag "Set Inline Level ..." to set a level. >> Nota : the syntax "Parameter Inline(30) foo" is equivalent to "Set Inline Level 30. Parameter Inline foo.", and "Include <30>F G" is equivalent to "Set Inline Level 30. Include F G." For instance, in ZBinary, eq is @Logic.eq and should rather be inlined, while in BigZ, eq is (fun x y => [x]=[y]) and should rather not be inlined. We could achieve this behavior by setting a level such as 30 to the parameter eq, and then tweaking the current level when applying functors. This idea of levels might be too restrictive, we'll see, but at least the implementation of this change was quite simple. There might be situation where parameters cannot be linearly ordered according to their "inlinablility". For these cases, we would need to mention names to inline or not at a functor application, and this is a bit more tricky (and might be a pain to use if there are many names). No documentation for the moment, since this feature is experimental and might still evolve. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13807 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-24More {raw => glob} changes for consistencyglondu
perl -pi -e 's/(\W|_)raw((?:sort|_prop|terms?|_branch|_red_flag|pat tern|_constr_of|_of_pat)(?:\W|_))/\1glob_\2/g;s/glob__/glob_/g;s/(\ W)R((?:Prop|Type|Fix|CoFix|StructRec|WfRec|MeasureRec)\W)/\1G\2/g;s /glob_terms?/glob_constr/g' **/*.ml* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13756 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-23Rename rawterm.ml into glob_term.mlglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13744 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-23Change of nomenclature: rawconstr -> glob_constrglondu
There was a discrepancy of the notions "raw" and "globalized" between constrs and tactics, and some confusion of the notions in e.g. genarg.mli (see all globwit_* there). This commit is a first step towards unification of terminology between constrs and tactics. Changes in module names will be done separately. In extraargs.ml4, the "ARGUMENT EXTEND raw" and related stuff, even affected by this change, has not been touched and highlights another confusion in "ARGUMENT EXTEND" in general that will be addressed later. The funind plugin doesn't respect the same naming conventions as the rest, so leave some "raw" there for now... they will be addressed later. This big commit has been generated with the following command (wrapped here, but should be on a *single* line): perl -pi -e 's/(\W(?:|pp|pr_l)|_)raw((?:constrs?|type|vars|_binder| _context|decl|_decompose|_compose|_make)(?:\W|_))/\1glob_\2/g;s/glo b__/glob_/g;s/prraw/prglob/g;s/(\W)R((?:Ref|Var|Evar|PatVar|App|Lam bda|Prod|LetIn|Cases|LetTuple|If|Rec|Sort|Hole|Cast|Dynamic)\W)/\1G \2/g' `git ls-files|grep -v dev/doc/changes.txt` git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13743 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-24Updated all headers for 8.3 and trunkherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-22Extension of the recursive notations mechanismherbelin
- Added support for recursive notations with binders - Added support for arbitrary large iterators in recursive notations - More checks on the use of variables and improved error messages - Do side-effects in metasyntax only when sure that everything is ok - Documentation Note: it seems there were a small bug in match_alist (instances obtained from matching the first copy of iterator were not propagated). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13316 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-22Constrintern: unified push_name_env and push_loc_name_env; madeherbelin
location dumping for binders uniformly treated in constrintern.ml (and renamed the optional arg of interp_context from fail_anonymous to global_level since the flag now also decides whether to dump binders as global or local ones); added locations for the variables occurring in the "as in" clauses; git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13314 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
Applied it to fix mli file headers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13176 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-14Added printing of recursive notations in cases pattern (supported by wish 2248).herbelin
Note that the code is no longer in constrextern.ml but in topconstr.ml where the code for reversing notations of term already was. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13132 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-08Fix treatment of {struct x} annotations in presence of generalizedmsozeau
binders. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13086 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-29Various minor improvements of comments in mli for ocamldocletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12976 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
- Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 08:02:04 +0000