aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2013-05-05Hack to solve a "Bad recursive type" anomaly.herbelin
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
2013-05-05Now printing body of abbreviations (i.e. notation with a name) withherbelin
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
2013-05-05Little fix for Nsatz: hypotheses not directly relevant to the nsatzherbelin
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
2013-05-05Improvement of r16204 on reporting tactic error locations: if the mainherbelin
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
2013-05-05Relaxing the constraint on eta-expanding on the fly while looking forherbelin
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
2013-05-05Reporting the change on matching partial applications in patterns ofherbelin
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
2013-05-03Removing a redundant function from Evd.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16465 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-30Fix wrong computation of dependency signature in cases raising an uncaught ↵msozeau
exception later. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16464 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-29Merging Context and Sign.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16463 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
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
2013-04-27Added a unit test for bug #2230.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16460 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-25Fix compilation (vernac.ml, missing ;)gareuselesinge
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
2013-04-25Fix: tooltip correctly handles the absence of info (empty string)gareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16457 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-25Coqide: Globalization feedback (proof of concept)gareuselesinge
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
2013-04-25lablgtk2 misses Glib.Utf8.pos_to_offset, workaround in ideutilsgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16455 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-25Flag ide_slave moved into Flags modulegareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16454 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-25Coqide: new tag "tooltip" for the Script windowgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16453 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-25raise UnsafeSuccess -> feedback AddedAxiomgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16452 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-25Coqide: new feedback mechanism for structured contentgareuselesinge
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
2013-04-25Fix indentationgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16450 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-23Fix issues with "Reset Initial" in scripts given to coqtop -lletouzey
Doing coqtop -l on a file starting with Reset Initial used to fail. To avoid that, we now always place an initial DOT in the libstack. Backtrack.reset_initial has been adapted accordingly: during an interactive session following a Load via coqtop -l (or .coqrc), a Reset Initial will bring back at the start of the interactive session, *not* undoing the initial Load. Note : Reset Initial might hence not be equivalent anymore to BackTo 1. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16449 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-23Egramcoq+Lexer : no need for an init_functionletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16448 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-23Indfun : use States.with_state_protection instead of freeze/unfreezeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16447 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-23Egramcoq: clean an ugly code snippetletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16446 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-23minor cleanup in coqtop.mlletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16445 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-23coqtop -compile: avoid with_heavy_rollback when non-interactiveletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16444 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-23Coqtop -compile : avoid saving init state when compiling just one fileletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16443 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-23Remove deprecated option -no-hash-consing (currently doing nothing)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16442 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-22code simplifications concerning Summaryletouzey
- 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
2013-04-22Declaremods: some more minor cleanupletouzey
Some code cleaning and factorisation , comments, indentations, ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16440 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-19Fix compilation of fake_idegareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16439 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-19interface.mli and serialize.ml reworked to avoid copy/paste of typesgareuselesinge
With this commit the types involved in the protocol between Coq and Coqide are written once and for all in interface.mli serialize.ml is monkey code that contains a reified version of these types and the related machinery needed to marshal values in these types to/from xml in a modular way. This file should be automatically generated from the spec of the protocol in an ideal world. Phantom types are used to statically check that the reified form of the types is in sync with the one declared in interface.mli The benefit of this commit is that changing the protocol is easier: one changes the types in interface.mli and lets ocamlc spot all the places that needs to be modified. This is a necessity if one plays with the protocol very often, like in my Paral-ITP branch. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16438 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-18coqc and coqmktop migrated in tools/, get rid of scripts/ subdirletouzey
No need to place these binaries apart, and anyway they aren't (shell) scripts since ages. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16432 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-18Coqdep: add an -exclude-dir option (wish mentionned in #3025)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16431 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-18Coqc: accept -exclude-dir + some others + cleanup (fix #3025)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16430 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-18Finer fix for bug 3017, mark unresolvability only of goals that aremsozeau
instances of metas in clenvtac. Makes Math-Classes compile again. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16429 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-18Only arguments declared as implicit can be renamedgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16427 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-18Fix #3001 (rename arg of global cst inside section)gareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16426 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-17Renaming SearchAbout into Search and Search into SearchHead.herbelin
I hope I did not forget any place to change. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16423 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-17Matching patterns: fixed allow_partial_app which was not working onherbelin
unnamed Metas; also added matching an applicative prefix (with non-meta head) of a term against a pattern, to be used by "Search" (i.e. SearchHead). This allows "Search" and "SearchPattern" to behave as in 8.4. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16422 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-17Fix of r16257 in r16205 for "errors raised by check_evar_instance wereherbelin
no longer trapped by solve_simple_eqn" was incomplete because "try ... with E as e | e when f e -> ..." means "try ... with (E as e | e) when f e -> ..." and not "try ... with E as e | (e when f e) -> ...". This was the cause for examples 2615.v and 2670.v failing since March 1. The need for "as e" should have warned me. Sorry for the mistake. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16420 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-17Coqmktop: dynlink is now mandatory due to Maxime's native-compilerletouzey
Some cleanup btw, for instance Dynlink.init is deprecated since at least ocaml 3.11 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16419 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-17Coqc: repair localisation of errors in filesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16418 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-17Using Parameter instead of Variable in test-suite/outputherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16417 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-17Improving error message in explain_cannot_find_well_typed_abstraction:herbelin
make head bound variables distinct from the variables in environment, so that the naming scheme is the same when, say, printing "fun x:B => foo x" in environment "x:A" (main error with explicit "fun") and when printing (secondary error in the "reason" message) "foo x" in environment "x:A, x:B" (i.e. with "fun" discharged in environment). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16415 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-17Like in r16346, do not filter local definitions (here in theherbelin
type-based second-order unification algorithm). In type-based second-order unification algorithm, protect local definitions in instances of evars to wrongly be considered as potentially flexible. Altogether, this fixes the anomaly in #3003 (even if some additional work has to be done to improve the resulting error message, see next commit). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16414 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-17Added group properties of eq_refl, eq_sym, eq_transherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16413 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-16Fixing #2968. This is quite brittle though, because we are messingppedrot
with the exception catching system of Ltac which is not really known for its safety, so that it may break a few things. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16411 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-16Added regression test for bug #3023 which was solved by Matthieu'sherbelin
commit r16134 (eta was missing in Flexible/Rigid and SemiFlexible/Rigid conversion problems). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16409 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-16More in IArrayppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16408 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-04 07:01:53 +0000