aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Little oversight in commit r16489 (fix for bug #3036).Gravatar herbelin2013-05-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16506 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documenting the Tries module, uniformizing the names according toGravatar ppedrot2013-05-09
| | | | | | Map/Set style and renaming the file accordingly as Trie. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16504 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updating some output tests in test-suite:Gravatar herbelin2013-05-09
| | | | | | | | | | | | | | InitSyntax, PrintInfos: consequence of r16467 which improved printing of sigT Notations2: consequence of r16470 on using notations while asked to print the body of an abbreviation Notations: fix from r16417 was incomplete (and by the way associated to a wrong commit message) names: related to commit r16205 which aligned "In environment" with the variables of the environment (maybe should it be better to still have "In environment" printed after "Error: " but I don't know how to do it with a forced newline). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16503 85f007b7-540e-0410-9357-904b9bb8a0f7
* Use definition_entry to declare local definitionsGravatar gareuselesinge2013-05-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16502 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cosmetic changeGravatar gareuselesinge2013-05-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16501 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
* A uniformization step around understand_* and interp_* functions.Gravatar herbelin2013-05-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Clarification of the existence of three algorithms for solving unconstrained evars: - the type-class mechanism - the heuristics for solving pending conversion problems and multi-candidates - Declare Implicit Tactic (when called from tactics) Main function for solving unconstrained evars (when not using understand): Pretyping.solve_remaining_evars - Clarification of the existence of three corresponding kinds of errors when reporting about unsolved evars: Main function for checking resolution of evars independently of the understand functions: Pretyping.check_evars_are_solved - Introduction of inference flags in pretyping for governing which combination of the algorithms to use when calling some understand function; there is also a flag of expanding or not evars and for requiring or not the resolution of all evars - Less hackish way of managing Pretyping.type_constraint: all three different possibilities are now represented by three different constructors - Main semantical changes done: - solving unconstrained evars and reporting is not any longer mixed: one first tries to find unconstrained evars by any way possible; one eventually reports on the existence of unsolved evars using check_evars_are_solved - checking unsolved evars is now done by looking at the evar map, not by looking at the evars occurring in the terms to pretype; the only observed consequence so far is in Cases.v because of subterms (surprisingly) disappering after compilation of pattern-matching - the API changed, see dev/doc/changes.txt Still to do: - Find more uniform naming schemes: - for distinguishing when sigma is passed as a reference or as a value (are used: suffix _evars, prefix e_) - for distinguishing when evars are allowed to remain uninstantiated or not (are used: suffix _evars, again, suffix _tcc, infix _open_) - be more consistent on the use of names evd/sigma/evars or evdref/evars - By the way, shouldn't "understand" be better renamed into "infer" or "preinfer", or "pretype". Grammatically, "understanding a term" looks strange. - Investigate whether the inference flags in tacinterp.ml are really what we want (e.g. do we really want that heuristic remains activated when typeclasses are explicitly deactivated, idem in Tacinterp.interp_open_constr where flags are strange). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16499 85f007b7-540e-0410-9357-904b9bb8a0f7
* A few comments in evarconv.mli.Gravatar herbelin2013-05-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16498 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformization: isevars -> evdref/sigma/evdGravatar herbelin2013-05-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16497 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing r16487 on sharing evars between multiple parameters (missing List.rev).Gravatar herbelin2013-05-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16496 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing unused module Nbtermdn.Gravatar ppedrot2013-05-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16495 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing Gmap from Notations.Gravatar ppedrot2013-05-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16494 85f007b7-540e-0410-9357-904b9bb8a0f7
* Xml_datatype.mli ships the xml typeGravatar gareuselesinge2013-05-09
| | | | | | | This breaks the dependency of Xml_parser, Xml_printer and Xml_utils on Serialize. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16493 85f007b7-540e-0410-9357-904b9bb8a0f7
* add Loadpath to printers.mllibGravatar gareuselesinge2013-05-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16492 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformizing the [if_warn] flag used for warning printing and putGravatar ppedrot2013-05-08
| | | | | | it into the standard logger instead. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16491 85f007b7-540e-0410-9357-904b9bb8a0f7
* Protection against "Bad recursive type" in w_unify0 (bug #3036).Gravatar herbelin2013-05-08
| | | | | | | | | | | | | | Morally, unification wants to unify "fun x:Meta => Meta" with "fun x:nat => match x with ... end". Retyping is asked to type "match x with ... end" in the context "x:Meta" where the type of x has de facto been lost. Retyping fails. I don't see an easy remedy since w_unify0 builds the unifier lazily, and I'm not sure it is worth to propagate the unifier to retyping so that it knows it. After all, the call to retyping in w_unify0 is not so critical. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16489 85f007b7-540e-0410-9357-904b9bb8a0f7
* Alert when using ".." outside a Notation command.Gravatar herbelin2013-05-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16488 85f007b7-540e-0410-9357-904b9bb8a0f7
* Declaration of multiple hypotheses or parameters now share typingGravatar herbelin2013-05-08
| | | | | | information for inference of implicit arguments. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16487 85f007b7-540e-0410-9357-904b9bb8a0f7
* Share more information between constructors and arity of an inductiveGravatar herbelin2013-05-08
| | | | | | type in order to solve implicit arguments. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16486 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moved isolated test params_ind.v to Inductive.v.Gravatar herbelin2013-05-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16485 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing ocamldoc compilation.Gravatar ppedrot2013-05-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16483 85f007b7-540e-0410-9357-904b9bb8a0f7
* Small cleaning of Evd interface.Gravatar ppedrot2013-05-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16482 85f007b7-540e-0410-9357-904b9bb8a0f7
* fake_ide: xml parser does not check for EOFGravatar gareuselesinge2013-05-06
| | | | | | Exactly as Coqide's parser does. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16481 85f007b7-540e-0410-9357-904b9bb8a0f7
* New module Xml_printer (dual to Xml_parser)Gravatar gareuselesinge2013-05-06
| | | | | | | Code for printing XML moved from xml_utils.ml to xml_printer.ml and improved to generate less garbage using Buffer.t systematically. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16480 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: view -> zoom in / out / fitGravatar gareuselesinge2013-05-06
| | | | | | | | This commit adds zoom facilities that are useful for demos (quickly increate font size) and daily use (set size so that 80 colums fit the window width). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16479 85f007b7-540e-0410-9357-904b9bb8a0f7
* States: frozen states can hold closuresGravatar gareuselesinge2013-05-06
| | | | | | | | States.freeze takes ~marshallable:bool, so that (only) when we want to marshal data to disk/network we can ask the freeze functions of the summary to force lazy values. The flag is propagated to Lib and Summary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16478 85f007b7-540e-0410-9357-904b9bb8a0f7
* Summary: support selective freezeGravatar gareuselesinge2013-05-06
| | | | | | One can freeze/unfreeze a portion of the summary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16477 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ideutils: comment on missing Glib utf8 handling functionGravatar gareuselesinge2013-05-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16476 85f007b7-540e-0410-9357-904b9bb8a0f7
* Close the .glob file after having saved .voGravatar gareuselesinge2013-05-06
| | | | | | | | | This is a no op for standard Coq, but is important for Paral-ITP, since saving the library to disk forces all frozen computations, and some of them may spit out glob data, so the file descriptor must be valid. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16475 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix typo in manualGravatar gareuselesinge2013-05-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16474 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improving printing of 'rew' notationGravatar herbelin2013-05-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16473 85f007b7-540e-0410-9357-904b9bb8a0f7
* Hack to solve a "Bad recursive type" anomaly.Gravatar herbelin2013-05-05
| | | | | | | | | | | | | | Retyping expects its argument already well-typed. However, if unification problems are not fully solved, a term to match can have an evar type together with the constraint that this evar has to be convertible to some given inductive type. One could have tried to have a more eager resolution of unification constraint but I'm afraid of the cost in comparing c=c' in general in "?x[c] = c'" unification problems, so I instead added a hack in retyping to recover the constraint. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16471 85f007b7-540e-0410-9357-904b9bb8a0f7
* Now printing body of abbreviations (i.e. notation with a name) withGravatar herbelin2013-05-05
| | | | | | | | | | full usage of notations instead of the previous cheap way to prevent circularity in printing by deactivating all notations. (Since "->" became a notation, printing abbreviations without notations at all had become even more inconvenient). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16470 85f007b7-540e-0410-9357-904b9bb8a0f7
* Little fix for Nsatz: hypotheses not directly relevant to the nsatzGravatar herbelin2013-05-05
| | | | | | | | | | problem are cleared (in case they denote applicative terms with at least 6 arguments). However some of them are used for type class instance inference (e.g. hypotheses of type Integral_domain). This commits prevents clearing these hypotheses. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16469 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improvement of r16204 on reporting tactic error locations: if the mainGravatar herbelin2013-05-05
| | | | | | | | error is not located, then do not use locations from Tactic Notation (TacAlias) or TACTIC EXTEND (TacExtend) code since they are relative to the defining code of these extensions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16468 85f007b7-540e-0410-9357-904b9bb8a0f7
* Relaxing the constraint on eta-expanding on the fly while looking forGravatar herbelin2013-05-05
| | | | | | | | | | | notation to use at printing time. We now allow to print "sigT P" as "{x:_ & P x}", generating a "_" for the missing type, when the notation is defined by 'Notation "{ x : A & P }" := (sigT (fun x:A => P))'. Do better, and change the notation to "(sigT (A:=A) (fun x => P))" so that the type is known even when eta-expansion is needed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16467 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reporting the change on matching partial applications in patterns ofGravatar herbelin2013-05-05
| | | | | | | the form "_ pat1 ... patn", and considering it experimental at this stage. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16466 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing a redundant function from Evd.Gravatar ppedrot2013-05-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16465 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix wrong computation of dependency signature in cases raising an uncaught ↵Gravatar msozeau2013-04-30
| | | | | | exception later. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16464 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
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
| | | | | | | | | | | | | | | | | 1. sorts.ml: A small file utility for sorts; 2. constr.ml: Really low-level terms, essentially kind_of_constr, smart constructor and basic operators; 3. vars.ml: Everything related to term variables, that is, occurences and substitution; 4. context.ml: Rel/Named context and all that; 5. term.ml: derived utility operations on terms; also includes constr.ml up to some renaming, and acts as a compatibility layer, to be deprecated. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16462 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a unit test for bug #2230.Gravatar ppedrot2013-04-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16460 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix compilation (vernac.ml, missing ;)Gravatar gareuselesinge2013-04-25
| | | | | | I did forget a ; while dealing with conflicts in git-svn rebase git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16458 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix: tooltip correctly handles the absence of info (empty string)Gravatar gareuselesinge2013-04-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16457 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: Globalization feedback (proof of concept)Gravatar gareuselesinge2013-04-25
| | | | | | | | | | | | | | | | | | | | A new feedback message for globalization infos can be sent by Coq to Coqide. Coqide stores the information in the proof of concept module wg_Tooltip, that also sets things up so that these infos are displayed as a tooltip when the mouse is over the text they are attached to. These infos are available only on locked text, and on the text just processed in the case of an error (on this piece of text, they vanish as the error tag vanishes as soon as the user edits the text). wg_Tooltip stocks these infos as lazy string. This is not needed in the proof of concept, but is necessary to scale up: Coq may not generate the full piece of info when the message is sent (because of high computational cost or big size) and just send an id; later on, when/if the user asks for the piece of info, the gui requests the info explicitly using the id. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16456 85f007b7-540e-0410-9357-904b9bb8a0f7
* lablgtk2 misses Glib.Utf8.pos_to_offset, workaround in ideutilsGravatar gareuselesinge2013-04-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16455 85f007b7-540e-0410-9357-904b9bb8a0f7
* Flag ide_slave moved into Flags moduleGravatar gareuselesinge2013-04-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16454 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: new tag "tooltip" for the Script windowGravatar gareuselesinge2013-04-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16453 85f007b7-540e-0410-9357-904b9bb8a0f7
* raise UnsafeSuccess -> feedback AddedAxiomGravatar gareuselesinge2013-04-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16452 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: new feedback mechanism for structured contentGravatar gareuselesinge2013-04-25
| | | | | | | | | | | | | | | | | This amounts to a new type of message called "feedback" and defined in Interface to hold structured data. Coq sends feedback messages asynchronously (they are all fetched, like regular messages, together with the main response to a call) and they are related to a specific sentence by an id. Other changes: - CoqOps pushes the sentence to be processed onto the cmd_stack before processing it and pulls it back if Coq.intep fails, in this way the handler for feedback messages can just look at the cmd_stack to find the offset of the sentence to eventually apply the new Gtk.tag. - The class coqops takes in input a coqtop to set its feedback_handle. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16451 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-22 08:04:27 +0000