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 --- plugins/funind/g_indfun.ml4 | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 088b4a0cde..8b90824fd2 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -151,11 +151,9 @@ GEXTEND Gram ; END -type 'a function_rec_definition_loc_argtype = ((Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) Loc.located, 'a) Genarg.abstract_argument_type +type function_rec_definition_loc_argtype = (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) Loc.located -let (wit_function_rec_definition_loc : Genarg.tlevel function_rec_definition_loc_argtype), - (globwit_function_rec_definition_loc : Genarg.glevel function_rec_definition_loc_argtype), - (rawwit_function_rec_definition_loc : Genarg.rlevel function_rec_definition_loc_argtype) = +let (wit_function_rec_definition_loc : function_rec_definition_loc_argtype Genarg.uniform_genarg_type) = Genarg.create_arg None "function_rec_definition_loc" VERNAC COMMAND EXTEND Function ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")] -> -- cgit v1.2.3