aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/printer.ml
Commit message (Collapse)AuthorAge
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ↵Gravatar xclerc2013-09-19
| | | | | | with OCaml 3.12.1). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16787 85f007b7-540e-0410-9357-904b9bb8a0f7
* At least made the evar type opaque! There are still 5 remaining unsafeGravatar ppedrot2013-09-18
| | | | | | | | | | | | casts of ints to evars. - 2 in Evarutil and Goal which are really needed, even though the Goal one could (and should) be removed; - 2 in G_xml and Detyping that are there for completeness sake, but that might be made anomalies altogether; - 1 in Newring which is quite dubious at best, and should be fixed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16786 85f007b7-540e-0410-9357-904b9bb8a0f7
* Partly replacing list-based access functions in Evd. This is stillGravatar ppedrot2013-09-03
| | | | | | | unsatisfactory as some functions implicitly require some ordering on the evars, but this is already better. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16759 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some cleanup in AutoGravatar ppedrot2013-09-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16758 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nicer code concerning dirpaths and modpath around LibGravatar letouzey2013-08-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16727 85f007b7-540e-0410-9357-904b9bb8a0f7
* State Transaction MachineGravatar gareuselesinge2013-08-08
| | | | | | | | | | | | | | | | | | | | | The process_transaction function adds a new edge to the Dag without executing the transaction (when possible). The observe id function runs the transactions necessary to reach to the state id. Transaction being on a merged branch are not executed but stored into a future. The finish function calls observe on the tip of the current branch. Imperative modifications to the environment made by some tactics are now explicitly declared by the tactic and modeled as let-in/beta-redexes at the root of the proof term. An example is the abstract tactic. This is the work described in the Coq Workshop 2012 paper. Coq is compile with thread support from now on. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16674 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing useless uses of Gmap.Gravatar ppedrot2013-05-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16520 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
* Improving error message in explain_cannot_find_well_typed_abstraction:Gravatar herbelin2013-04-17
| | | | | | | | | | 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
* Minor code cleaning in CArray / CList.Gravatar ppedrot2013-03-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16351 85f007b7-540e-0410-9357-904b9bb8a0f7
* Robust display of NotConvertibleTypeField errors (fix #3008, #2995)Gravatar letouzey2013-03-21
| | | | | | | | | | | | | | Since the nametab isn't aware of everything needed to print mismatched types (cf the bug test-cases), we create a robust term printer that known how to print a fully-qualified name when [shortest_qualid_of_global] has failed. These Printer.safe_pr_constr and alii are meant to never fail (at worse they display "??", for instance when the env isn't rich enough). Moreover, the environnement may have changed between the raise of NotConvertibleTypeField and its display, so we store the original env in the exception. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16342 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restrict (try...with...) to avoid catching critical exn (part 13)Gravatar letouzey2013-03-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16290 85f007b7-540e-0410-9357-904b9bb8a0f7
* More monomorphization.Gravatar ppedrot2013-03-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16260 85f007b7-540e-0410-9357-904b9bb8a0f7
* use List.rev_map whenever possibleGravatar letouzey2013-02-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16211 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added propagation of evars unification failure reasons for betterGravatar herbelin2013-02-17
| | | | | | | | 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
* No reason a priori for using unfiltered env for printingGravatar herbelin2013-01-29
| | | | | | 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
* Renaming evar_env/evar_unfiltered_env into evar_filtered_env/evar_envGravatar herbelin2013-01-29
| | | | | | for better uniformity of naming policy. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16172 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modulification of LabelGravatar ppedrot2012-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16097 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
* Moved Intset and Intmap to Int namespace.Gravatar ppedrot2012-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16067 85f007b7-540e-0410-9357-904b9bb8a0f7
* Print univ constraints generated by a constant or inductive (when flag is set)Gravatar barras2012-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15989 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleaning and small optimization in CList.Gravatar ppedrot2012-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15988 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed #2926:Gravatar ppedrot2012-10-29
| | | | | | | Extend "Print Opaque Dependencies" for transparent dependencies as well git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15935 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15844 85f007b7-540e-0410-9357-904b9bb8a0f7
* As r15801: putting everything from Util.array_* to CArray.*.Gravatar ppedrot2012-09-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15804 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
* Slight modification to the printing of goals when in emacs mode.Gravatar courtieu2012-07-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15635 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing test-suiteGravatar pboutill2012-07-20
| | | | | | | | - bug in r15614: hnf was identity - fix Print Assumptions - bug in r15624: Dump glob of Print About only for Glob git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15630 85f007b7-540e-0410-9357-904b9bb8a0f7
* A friendlier printing of remaining goals when no goal is focused.Gravatar aspiwack2012-07-11
| | | | | | | Only their conclusion is printed (with a "subgoal n" header) like every goal but the first in the usual case. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15591 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing Print Assumption displayGravatar ppedrot2012-07-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15590 85f007b7-540e-0410-9357-904b9bb8a0f7
* Small change in the printing of proofs for use by coqide.Gravatar aspiwack2012-07-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15577 85f007b7-540e-0410-9357-904b9bb8a0f7
* Another correction to the dependent existential variable printingGravatar aspiwack2012-07-10
| | | | | | | | for emacs mode. Hopefully fixes Bug 2678 this time. Much saner and more compact code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15573 85f007b7-540e-0410-9357-904b9bb8a0f7
* Change how the number of open goals is printed.Gravatar aspiwack2012-07-04
| | | | | | | | | | If you are focused on 3 subgoals, and unfocusing would reveal 2 extra subgoals, and unfocusing again would reveal 4 extra subgoals, then coqtop will tell you: 3 focused subgoals (unfocused: 2-4) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15508 85f007b7-540e-0410-9357-904b9bb8a0f7
* When focused on an empty list of goal (after finishing a subproof introducedGravatar aspiwack2012-07-04
| | | | | | | by a bullet or a brace, for instance), the message "This subproof is complete […]" is now rendered before the list of goals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15507 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing test-suite after last storm in Pp.Gravatar pboutill2012-06-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15433 85f007b7-540e-0410-9357-904b9bb8a0f7
* Replacing some str with strbrkGravatar ppedrot2012-06-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15422 85f007b7-540e-0410-9357-904b9bb8a0f7
* More uniformisation in Pp.warn functions.Gravatar ppedrot2012-05-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15399 85f007b7-540e-0410-9357-904b9bb8a0f7
* place all pretty-printing files in new dir printing/Gravatar letouzey2012-05-29
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15391 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-19 23:39:37 +0000