aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/reserve.ml
Commit message (Collapse)AuthorAge
* Namegen primitives now apply on evar constrs.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | Incidentally, this fixes a printing bug in output/inference.v where the displayed name of an evar was the wrong one because its type was not evar-expanded enough.
* Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
| | | | Suggested by @ppedrot
* Unify location handling of error functions.Gravatar Emilio Jesus Gallego Arias2016-08-19
| | | | | | | | | | | | | | 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.
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵Gravatar Pierre Letouzey2016-07-03
| | | | | | module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
|
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Revert specific syntax for primitive projections, avoiding uglyGravatar Matthieu Sozeau2014-09-17
| | | | | | | | contortions in internalization/externalization. It uses a fully typed version of detyping, requiring the environment, to move from primitive projection applications to regular applications of the eta-expanded version. The kernel is unchanged, and only constrMatching needs compatibility code now.
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
| | | | | instances still to do). Using heuristics to name after the quantifier name it comes. Also added a "sigma" to almost all printing functions.
* Remove some dead-code (thanks to ocaml warnings)Gravatar Pierre Letouzey2014-03-05
| | | | The removed code isn't used locally and isn't exported in the signature
* 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.
* Better behaviour for sets of reserved names.Gravatar Pierre-Marie Pédrot2014-03-01
|
* Never suppress the typing constraint of bound variables whose name wasGravatar Pierre-Marie Pédrot2014-03-01
| | | | reserved with Implicit Type.
* Notations can now accept dummy arguments. If ever a bound variable is notGravatar Pierre-Marie Pédrot2013-12-22
| | | | | | used, they are automatically flagged as only parsing. CAVEAT: unused arguments are not typechecked, because they are dropped before the interpretation phase.
* Adding generic solvers to term holes. For now, no resolution mechanism norGravatar Pierre-Marie Pédrot2013-11-27
| | | | parsing is plugged.
* Replacing uses of association lists by maps in notations.Gravatar ppedrot2013-08-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16655 85f007b7-540e-0410-9357-904b9bb8a0f7
* Getting rid of module Gmapl.Gravatar ppedrot2013-05-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16500 85f007b7-540e-0410-9357-904b9bb8a0f7
* code simplifications concerning SummaryGravatar letouzey2013-04-22
| | | | | | | | | | | | | | | - Most of the time, the table registered via Summary.declare_summary is just a single reference. A new function Summary.ref now allows to both declare this ref and register it to summary in one shot. - Clarifications concerning the role of [init_function]. For statically registered tables that don't need a special initializer, just do nothing there (see the new Summary.nop function). Beware: now that Summary exports a function named "ref", any code that do an "open Summary" will probably fail to compile. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16441 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
* Monomorphization (interp)Gravatar ppedrot2012-11-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15999 85f007b7-540e-0410-9357-904b9bb8a0f7
* More cleaning on Utils and CList. Some parts of the code beingGravatar ppedrot2012-09-17
| | | | | | peculiarly messy, I hope I did not introduce too many bugs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15815 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some documentation and cleaning of CList and Util interfaces.Gravatar ppedrot2012-09-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15805 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
| | | | | | | | | List module. That way, an "open Util" in the header permits using any function of CList in the List namespace (and in particular, this permits optimized reimplementations of the List functions, as, for example, tail-rec implementations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15801 85f007b7-540e-0410-9357-904b9bb8a0f7
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
| | | | | | | | | | compiler warnings). I was afraid that such a brutal refactoring breaks some obscure invariant about linking order and side-effects but the standard library still compiles. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15800 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
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
| | | | | | | | | | 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
* 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
* Stuff about notation_constr (ex-aconstr) now in notation_ops.mlGravatar letouzey2012-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15381 85f007b7-540e-0410-9357-904b9bb8a0f7
* New files intf/constrexpr.mli and intf/notation_term.mli out of TopconstrGravatar letouzey2012-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15375 85f007b7-540e-0410-9357-904b9bb8a0f7
* Evar_kinds.mli containing former Evd.hole_kind, avoid deps on EvdGravatar letouzey2012-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15371 85f007b7-540e-0410-9357-904b9bb8a0f7
* Noise for nothingGravatar pboutill2012-03-02
| | | | | | | | | | | 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
* Add type annotations around all calls to Libobject.declare_objectGravatar letouzey2011-11-02
| | | | | | | | | | | | | | | | | These annotations are purely optional, but could be quite helpful when trying to understand the code, and in particular trying to trace which which data-structure may end in the libobject part of a vo. By the way, we performed some code simplifications : - in Library, a part of the REQUIRE objects was unused. - in Declaremods, we removed some checks that were marked as useless, this allows to slightly simplify the stored objects. To investigate someday : in recordops, the RECMETHODS is storing some evar_maps. This is ok for the moment, but might not be in the future (cf previous commit on auto hints). This RECMETHODS was not detected by my earlier tests : not used in the stdlib ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14627 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing failing printer when the type of a binder name with implicitGravatar herbelin2011-10-24
| | | | | | | associated type contain evars (call to aconstr_of_glob_constr was not protected against failure in the presence of evars). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14583 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rather quick hack to avoid using notations involving "Type" whenGravatar herbelin2011-06-12
| | | | | | | 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
* Added a table for using reserved names for binding names to typesGravatar herbelin2011-03-05
| | | | | | (in addition of types to names) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13887 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13744 85f007b7-540e-0410-9357-904b9bb8a0f7
* Change of nomenclature: rawconstr -> glob_constrGravatar glondu2010-12-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* Add information of localisation when an error involving an "implicitGravatar herbelin2010-11-07
| | | | | | types" occurs. Also improved the "unexpected type" error message. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13626 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
| | | | | | | | | | In particular, the unused lib/tlm.ml and lib/gset.ml are removed In addition, to simplify code, Libobject.record_object returning only the ('a->obj) function, which is enough almost all the time. Use Libobject.record_object_full if you really need also the (obj->'a). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13460 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
| | | | | | | | | | | - 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
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
* Death of "survive_module" and "survive_section" (the first one wasGravatar herbelin2009-08-13
| | | | | | | | | | only used to allow a module to be ended before the summaries were restored what can be solved by moving upwards the place where the summaries are restored). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12275 85f007b7-540e-0410-9357-904b9bb8a0f7
* Move Record desugaring to constrintern and add ability to use notationsGravatar msozeau2008-11-05
| | | | | | | | | for record fields (using "someproj : sometype where not := constr" syntax). Only one notation allowed currently and no redeclaration after the record declaration either (will be done for typeclasses). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11542 85f007b7-540e-0410-9357-904b9bb8a0f7
* Open notation for declaring record instances.Gravatar msozeau2008-10-23
| | | | | | | | | | | | | | | | | | | | It solves feature request 1852, makes me and Arnaud happy and will permit to factor some more code in typeclasses. - Records are introduced using the syntax "{| x := t; y := foo |}" and "with" clauses are currently parsed but not yet supported in the elaboration. You are invited to suggest other syntaxes :) - Missing fields are turned into holes, extra fields cause an error message. The current implementation finds the type of the record at pretyping time, from the typing constraint alone (and just expects an inductive with one constructor). It is then impossible to use scope information to parse the bodies: that may be wrong. The other solution I see is using the fields to detect the type earlier, before internalisation of the bodies, but then we get in name clash hell. - In funind/contrib/interface I mostly put [assert false] everywhere to avoid warnings. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11496 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Second pass on implementation of let pattern. Parse "let ' par [as x]?Gravatar msozeau2008-03-28
| | | | | | | | | | | | | | | | | | [in I] := t [return pred] in b", just as SSReflect does with let:. Change implementation: no longer a separate AST node, just add a case_style annotation on Cases to indicate it (if ML was dependently typed we could ensure that LetPatternStyle Cases have only one term to be matched and one branch, alas...). This factors out most code and we lose no functionality (win ! win !). Add LetPat.v test suite. - Slight improvement of inference of return clauses for dependent pattern matching. If matching a variable of non-dependent type under a tycon that mentions it while giving no return clause, the dependency will be automatically infered. Examples at the end of DepPat. Should get rid of most explicit returns under tycons. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10727 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add new LetPattern construct to replace dest. syntax: let| pat := t in b is ↵Gravatar msozeau2008-01-17
| | | | | | backwards compatible. Update CHANGES with things i've done. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10446 85f007b7-540e-0410-9357-904b9bb8a0f7
* Merged revisions ↵Gravatar msozeau2007-12-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,10398,10403-10408 via svnmerge from svn+ssh://msozeau@scm.gforge.inria.fr/svn/coq/branches/TypeClasses ........ r10358 | msozeau | 2007-12-10 15:42:53 +0100 (Mon, 10 Dec 2007) | 1 line Comment grammar error ........ r10359 | msozeau | 2007-12-10 16:04:09 +0100 (Mon, 10 Dec 2007) | 7 lines The initial Type Classes patch. This patch introduces type classes and instance definitions a la Haskell. Technically, it uses the implicit arguments mechanism which was extended a bit. The patch also introduces a notation for explicitely marking implicit, maximally inserted parameters. It includes the tactic redefinition code too (Ltac tac ::= foo redefines tac). ........ r10360 | msozeau | 2007-12-10 16:14:30 +0100 (Mon, 10 Dec 2007) | 1 line Fix interface ........ r10361 | msozeau | 2007-12-10 16:28:19 +0100 (Mon, 10 Dec 2007) | 1 line Fix more xlate code ........ r10362 | msozeau | 2007-12-11 02:00:53 +0100 (Tue, 11 Dec 2007) | 3 lines Update coqdoc for type classes, fix proof state not being displayed on Next Obligation. ........ r10365 | msozeau | 2007-12-11 14:22:35 +0100 (Tue, 11 Dec 2007) | 3 lines Bug fixes in Instance decls. ........ r10371 | msozeau | 2007-12-12 21:17:30 +0100 (Wed, 12 Dec 2007) | 3 lines Streamline typeclass context implementation, prepare for class binders in proof statements. ........ r10372 | msozeau | 2007-12-12 22:03:38 +0100 (Wed, 12 Dec 2007) | 1 line Minor cosmetic fixes: allow sorts as typeclass param instances without parens and infer more types in class definitions ........ r10373 | msozeau | 2007-12-13 00:35:09 +0100 (Thu, 13 Dec 2007) | 2 lines Better names in g_vernac, binders in Lemmas and Context [] to introduce a typeclass context. ........ r10377 | msozeau | 2007-12-13 18:34:33 +0100 (Thu, 13 Dec 2007) | 1 line Stupid bug ........ r10383 | msozeau | 2007-12-16 00:04:48 +0100 (Sun, 16 Dec 2007) | 1 line Bug fixes in name handling and implicits, new syntax for using implicit mode in typeclass constraints ........ r10384 | msozeau | 2007-12-16 15:53:24 +0100 (Sun, 16 Dec 2007) | 1 line Streamlined implementation of instances again, the produced typeclass is a typeclass constraint. Added corresponding implicit/explicit behaviors ........ r10394 | msozeau | 2007-12-18 23:42:56 +0100 (Tue, 18 Dec 2007) | 4 lines Various fixes for implicit arguments, new "Enriching" kw to just enrich existing sets of impl args. New syntax !a to force an argument, even if not dependent. New tactic clrewrite using a setoid typeclass implementation to do setoid_rewrite under compatible morphisms... very experimental. Other bugs related to naming in typeclasses fixed. ........ r10395 | msozeau | 2007-12-19 17:11:55 +0100 (Wed, 19 Dec 2007) | 3 lines Progress on setoids using type classes, recognize setoid equalities in hyps better. Streamline implementation to return more information when resolving setoids (return the results setoid). ........ r10398 | msozeau | 2007-12-20 10:18:19 +0100 (Thu, 20 Dec 2007) | 1 line Syntax change, more like Coq ........ r10403 | msozeau | 2007-12-21 22:30:35 +0100 (Fri, 21 Dec 2007) | 1 line Add right-to-left rewriting in class_setoid, fix some discharge/substitution bug, adapt test-suite to latest syntax ........ r10404 | msozeau | 2007-12-24 21:47:58 +0100 (Mon, 24 Dec 2007) | 2 lines Work on type classes based rewrite tactic. ........ r10405 | msozeau | 2007-12-27 18:51:32 +0100 (Thu, 27 Dec 2007) | 2 lines Better evar handling in pretyping, reorder theories/Program and add some tactics for dealing with subsets. ........ r10406 | msozeau | 2007-12-27 18:52:05 +0100 (Thu, 27 Dec 2007) | 1 line Forgot to add a file ........ r10407 | msozeau | 2007-12-29 17:19:54 +0100 (Sat, 29 Dec 2007) | 4 lines Generalize usage of implicit arguments in terms, up to rawconstr. Binders are decorated with binding info, either Implicit or Explicit for rawconstr. Factorizes code for typeclasses, topconstrs decorations are Default (impl|expl) or TypeClass (impl|expl) and implicit quantification is resolve at internalization time, getting rid of the arbitrary prenex restriction on contexts. ........ r10408 | msozeau | 2007-12-31 00:58:50 +0100 (Mon, 31 Dec 2007) | 4 lines Fix parsing of subset binders, bugs in subtac_cases and handling of mutual defs obligations. Add useful tactics to Program.Subsets. ........ git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10410 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plus de combinateurs sont passés de Util à Option. Le module Options Gravatar aspiwack2007-12-06
| | | | | | | | | devient Flags. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10348 85f007b7-540e-0410-9357-904b9bb8a0f7
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | lib/option.ml(i) . J'en profite pour rajouter des primitives de lifting des fonctions (à un ou deux arguments tous ou partie de type option). Il reste quelques opérations dans Util à propos desquelles je ne suis pas trop sûr, ou simplement que j'ai oublié, mais qui attendront demain car il est tard (comme some_in qui devrait devenir Option.make je suppose) . Elles s'expriment souvent facilement en fonction des autres, par exemple "option_compare x y" est égal à "Option.lift2 compare x y" . Le option_cons devrait faire son chemin dans le module parce qu'il est assez primitif et qu'il n'y a pas de fonction "cons" dans OCaml. J'en ai profité aussi pour remplacer les trop nombreux "failwith" par des erreurs locales au module, donc plus robustes. J'ai trouvé aussi une fonction qui était définie deux fois, et une définie dans un module particulier. Mon seul bémol (mais facile à traiter) c'est la proximité entre le nom de module Option et l'ancien Options. J'ai pas de meilleure idée de nom à l'heure qu'il est, ni pour l'un, ni pour l'autre. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10346 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add a parameter to QuestionMark evar kind to say it can be turned into an ↵Gravatar msozeau2007-03-19
| | | | | | | | | | obligations (even an opaque one). Change cast_type to include the converted-to type or nothing in case of a Coerce cast, required much minor changes. Various little subtac changes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9718 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 20:59:06 +0000