aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2013-05-28Setting "appcontext" as the default behaviour in Ltac matching.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16537 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-28Fixing warning of deprecated Argument Scopes.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16536 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-28Getting rid of LtacLocated exception transformer.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16535 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-28Fixing debug of empty Ltac matching goal.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16534 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-28Pushing lazy lists into Ltac. Now, the control flow is explicitppedrot
in Tacinterp, and it allows to remove a lot of entangled exception matchings in MatchGoal. Performance should not be affected, because the structures manipulated are somehow similar. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16533 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-28Adding a persistent stream data structure.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16532 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-24Code cleaning in Matching.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16531 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-23Fixing #3042ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16530 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-16Fixing Pp.strbrk which was reversing words.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16529 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-16std_ppcmds is persistent, errors can be printed twicegareuselesinge
The patch is very simple and naive, there is no lazy involved. This makes a difference only for strbrk. An extra patch may be necessary if there is a noticeable slowdown. In any case the data type used is opaque, to ease any future optimization. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16528 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-14Mini documentation (evar_absorb_arguments).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16527 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-14Delayed the computation of parameters in sort polymorphism ofherbelin
inductive types. This saves some computation, but also allows incidentally to retype terms with evars without failing if an inductive type as an argument whose type is an evar. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16526 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-14"change ... in ..." and "simpl ... in ..." now consider nestedherbelin
occurrences (possible source of incompatibilities since this alters the numbering of occurrences). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16525 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-14Fixing a regression in unification introduced in r16205 (error raisedherbelin
by solve_candidates was not anymore handled at the expected time). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16524 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-14Gmap is now useless, hail to Map!ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16523 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-14Removing the use of Gmap from Auto.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16522 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-14Removing Gmap from Classops. Fold order only mattered for printing.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16521 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-14Removing useless uses of Gmap.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16520 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-14Removing Fmap from libraries, it is not used anymore.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16519 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-14Replacing compatibility layer for Fmap in Typeclasses. Code wasppedrot
actually almost fold-order irrelevant (only changes printing order). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16518 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-14More semantical-friendly function.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16517 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-14Replacing Id.check with Id.is_valid, as its sole use was underppedrot
an ugly try ... with construct. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16516 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-12Removing Fset, since it is not used anymore.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16515 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-12Removing the use of Fset/Fmap from Trie. There was actually onlyppedrot
one place depending on fold order, which was easy to bypass. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16514 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-12Documenting the previous commit.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16513 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-12Granting wish #3014:ppedrot
Hint Rewrite should allow multiple databases. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16512 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-12Removing Gmap from Extraction pluginppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16511 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-12Use the Hook module here and there.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16510 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-12Added a generic notion of hook. Hooks are functions to be setppedrot
exactly once at runtime, often to reduce the mutual dependency of modules. This module permits to track them more easily. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16509 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-11Fixing a source of evars leak, revealed by contrib QuicksortComplexityherbelin
after r16499 which replaced a check for visible undefined evars (check_evars) by a check for undefined evars in the evar map (check_evars_are_solved). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16508 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-10Removing Gmap from Tacinterp.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16507 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-10Little oversight in commit r16489 (fix for bug #3036).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16506 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-09Documenting the Tries module, uniformizing the names according toppedrot
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
2013-05-09Updating some output tests in test-suite:herbelin
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
2013-05-09Use definition_entry to declare local definitionsgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16502 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-09Cosmetic changegareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16501 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-09Getting rid of module Gmapl.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16500 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-09A uniformization step around understand_* and interp_* functions.herbelin
- 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
2013-05-09A few comments in evarconv.mli.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16498 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-09Uniformization: isevars -> evdref/sigma/evdherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16497 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-09Fixing r16487 on sharing evars between multiple parameters (missing List.rev).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16496 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-09Removing unused module Nbtermdn.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16495 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-09Removing Gmap from Notations.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16494 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-09Xml_datatype.mli ships the xml typegareuselesinge
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
2013-05-09add Loadpath to printers.mllibgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16492 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-08Uniformizing the [if_warn] flag used for warning printing and putppedrot
it into the standard logger instead. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16491 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-08Protection against "Bad recursive type" in w_unify0 (bug #3036).herbelin
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
2013-05-08Alert when using ".." outside a Notation command.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16488 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-08Declaration of multiple hypotheses or parameters now share typingherbelin
information for inference of implicit arguments. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16487 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-08Share more information between constructors and arity of an inductiveherbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-12 17:20:30 +0000