aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2013-02-24New -no-native-compiler flag for configure, globally disabling the nativemdenes
compiler (implemented on Matthieu's request). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16240 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-24Reduced the noise level when dynlinking in bytecode mode or whenmdenes
-no-native-compiler flag is on. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16239 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-22Tentative heuristic fix to handle lexer failures from CoqIDE whenppedrot
cutting XML phrases carelessly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16238 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-22Cosmetic changes to CoqIDE finder widget.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16237 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-21Names: con_modpath and con_label access back the user kn partletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16236 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-21Added missing documentation of Set Printing Existential Instances.herbelin
Also started a preliminary documentation about evars (where to have it in the doc is somehow open). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16234 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-21A slightly more efficient test of well-typedness of restriction ofherbelin
evars (though this might be slighty more costly). This incidentally solves Appel's part of bug #2830 even though a conceptual problem around the interaction of unification with the proof engine has to be solved. Indeed, what to do when unification, called as part of a tactic, solves or refines the current goal by side effect. Somehow, unifyTerms or tclEVARS should take this possibility into consideration, either by forbidding the refinement of the current goal by side effect, or by acknowledging this refinement by producing new subgoals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16232 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-21Added Evarsolve to the list of modules to open for debugging.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16231 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-20Fixing an annoying bug in CoqIDE which causes the very first lineppedrot
to be untagged whenever trying to modify the first offset. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16230 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-20Fixing #2763ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16229 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-20More handling of scrollbars in CoqIDE completionppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16228 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-20CoqIDE: Including autocompletion in word proposalsppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16227 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-20Corrects bug #2959 (error during Qed leads to assertion failure).aspiwack
Well-placed [Proof.transaction]-s do the trick. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16225 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-20Adding scrollbars to CoqIDE autocompletionppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16224 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-19New autocompletion mechanism in CoqIDE. Now provides many answersppedrot
through a popup. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16223 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-19avoid (Int.equal (cmp ...) 0) when a boolean equality existsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16222 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-19Dir_path --> DirPathletouzey
Ok, this is merely a matter of taste, but up to now the usage in Coq is rather to use capital letters instead of _ in the names of inner modules. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16221 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-19module_path --> ModPath.t, kernel_name --> KerName.tletouzey
For the moment, the compatibility names about these new modules are still used in the rest of Coq. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16220 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-19Mod_subst: an extra assertletouzey
It seems that the Equiv delta_hint in a resolver have a particular shape: a kn can apparently only be shifted to another kn with same label this way. We validate this fact via an assert, since this isn't obvious (due to recursive calls in Mod_subst and Modops), and since this implies the important fact that user and canonical parts of kernel pairs have necessarily the same label (and section dirpath). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16219 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-19Classops : avoid some use of Gmapletouzey
Gmap uses Pervasives.compare which may interact badly with structures like pairs of kernel names For the moment, we consider elements in classes and coercions only according to their user kernel name: this provides maximal compatibility. But it could be interesting to try using comparision according to canonical kernel names... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16218 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-19Names: revised representation of constants and mutual_inductiveletouzey
- a module KernelPair for improving sharing between constant and mind - shorter representation than a pair when possible - exports comparisions on constant and mind and ... - a kn_equal function instead of Int.equal (kn_ord ...) 0 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16217 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-18Mod_subst: improve sharing during kn substitutionsletouzey
When user and canonical parts are physically equal, let's avoid computing both their substitutions : this is a waste of time and also potentially of memory sharing. For instance two identical sub-calls to subst_mp0 may produce answers that are = but not ==. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16216 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-18Removing Exc_located and using the new exception enrichementppedrot
mechanism to retrieve the same information. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16215 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-18Adding more primitives to Exninfoppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16214 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-18Updating the backtrace handling mechanism to accomodate the newppedrot
exception information addition facility. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16213 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-18Added exception enrichment. Now one can define additional arbitraryppedrot
information worn by exceptions. The implementation is quite hackish but it should work nonetheless. Basically, it adds an additional cell to exceptions arguments, in which you can put whatever you want. By typing invariants, you may not reach this cell by normal means, so it should be safe. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16212 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-18use List.rev_map whenever possibleletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16211 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-18Minor code cleanups, especially take advantage of Dir_path.is_emptyletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16210 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-18Extraction: same as commit 16203, hopefully without NotASort exnsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16209 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-17Displaying environment and unfolding aliases in "cannot_unify"herbelin
error. Maybe displaying environment is making output overly verbose, but this can also be considered an IDE issue, which would e.g. provide a button to hide/display environment of the error message... Also added some "make_all_name_different" which should probably prevent some anomalies "index to an anonymous variable" at error reporting time. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16208 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-17A more informative message when the elimination predicate forherbelin
destruct, rewrite, etc. is not well-typed. Also added support for a more informative message when the elimination predicate is not well-formed while using the smart "second-order" unification algorithm. However the "abstract_list_all" algorithm seems to remain more informative though, so we still use this algorithm for reporting about ill-typed predicates. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16207 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-17Locating errors from consider_remaining_unif_problems if possibleherbelin
(useful when consider_remaining_unif_problems not called via pretyping.ml, as e.g. from command.ml). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16206 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-17Added propagation of evars unification failure reasons for betterherbelin
error messages. The architecture of unification error handling changed, not helped by ocaml for checking that every exceptions is correctly caught. Report or fix if you find a regression. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16205 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-17Revised the Ltac trace mechanism so that trace breaking due toherbelin
interleaving of ltac and ml code is not visible (this particularly applies to ltac notation ring, which calls ml-level ring_lookup and Ring again at the ltac level, resulting in non-localisation of "ring" errors). Added also missing LtacLocated checks in Class_instance and Proofview. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16204 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-14Fix extraction of inductive types that Coq auto-detects to be in Propletouzey
Typical example : Inductive t := T : t -> t. Earlier, the extraction was using a shortcut to get the sort of t (via some mind_arity stuff), but this was producing a less precise answer (here InType) than a full Retyping.get_sort_family_of (here InProp since t is a singleton type, with no content). The extraction of t was hence awkward, since the type of the constructor T was computed with the precise method, and its argument was optimized out. Now the whole t is considered logical by the extraction. NB: to avoid this clever but highly non-intuitive behavior of Coq placing the above t in Prop, for the moment you have to fix its sort, for instance: Inductive t : Set := T : t -> t. Using Type instead of Set still activates Coq's minimal sort detection... Instead, you could also use one specific TypeX obtained via Definition TypeX := Type. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16203 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-13CoqIDE: Adding escape reaction to replace widgetppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16202 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-13Fixing autocompletion lock in CoqIDEppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16200 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-13make validate repaired via a temporary fix for #2949letouzey
The offending functor in NZOrder wasn't actually used, so I've commented it for now. Btw, the Not_found in coqchk is now turned into something slightly more informative git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16199 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-12Checker: re-sync vo structures after Maxime's commit 16136letouzey
make validate still fails, but that's another issue (#2949) we're still working on... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16198 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-11Fixing bug in native compiler with let patterns in fixpoint definitions.mdenes
Typical example: Fixpoint f (m : nat) (o := true) (n : nat) {struct n} := n. Was raising an "index out of bounds" exception at compile-time. Nota: this construction is still incorrectly handled by the VM. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16197 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-10Useless use of hooks in VernacDefinition. In addition, this wasppedrot
polluting the AST first-order structure. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16196 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-10Splitted Evarutil in two filesppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16195 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-10Moved code from Pretype_error to Evarutilppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16194 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-05Revert "Ordered evars by level of dependency in the merging phase of ↵herbelin
unification" Though this commit provides with more "natural" instances of metas found by unification, it breaks a few contribs. The best approach to try is maybe now to instead plug apply on evarconv.ml, rather than on unification.ml! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16191 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-05Fixed bug #2981 (anomaly NotASort in Retyping due to collision betweenherbelin
variable names). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16185 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-03Fixing coqchk compilation after commit r16183ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16184 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-01v8.4: Granting bug/wish #2976 (turning anomaly on input_value into nice message)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16183 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-29Fixed #2970 (made that remember's eqn name is interpretable as an ltac var).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16181 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-29Added a file for testing regression of bug #2955 (anomaly in simpl inherbelin
the presence of aliased modules). Bug was actually fixed in trunk (thanks to PMP's monomorphization (and change of semantics) of equality over evaluable references. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16180 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-29No reason a priori for using unfiltered env for printingherbelin
goal. Filtered env is intended to be type-safe. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16177 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 04:58:27 +0000