From b23c6c6f1158dc247615ded5867c290f18aab1b9 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Thu, 6 Jun 2013 14:59:02 +0000
Subject: Uniformizing generic argument types.

Now, instead of having three unrelated types describing a dynamic
type at each level (raw, glob, top), we have a "('a, 'b, 'c) genarg_type"
whose parameters describe the reified type at each level.

This has various advantages:

- No more code duplication to handle the three level separately;
- Safer code: one is not authorized to mix unrelated types when what
was morally expected was a genarg_type.
- Each level-specialized representation can be accessed through
well-typed projections: rawwit, glbwit and topwit.

Documenting a bit Genarg b.t.w.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16564 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/top_printers.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 8db7de46cb..6184501550 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -410,7 +410,7 @@ let _ =
     Vernacinterp.vinterp_add "PrintConstr"
       (function
          [c] when genarg_tag c = ConstrArgType && true ->
-           let c = out_gen rawwit_constr c in
+           let c = out_gen (rawwit wit_constr) c in
            (fun () -> in_current_context constr_display c)
        | _ -> failwith "Vernac extension: cannot occur")
   with
@@ -427,7 +427,7 @@ let _ =
     Vernacinterp.vinterp_add "PrintPureConstr"
       (function
          [c] when genarg_tag c = ConstrArgType && true ->
-           let c = out_gen rawwit_constr c in
+           let c = out_gen (rawwit wit_constr) c in
            (fun () -> in_current_context print_pure_constr c)
        | _ -> failwith "Vernac extension: cannot occur")
   with
-- 
cgit v1.2.3