diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-06-06 14:59:02 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-06-06 14:59:02 +0000 |
| commit | b23c6c6f1158dc247615ded5867c290f18aab1b9 (patch) | |
| tree | f0ed29a89e1672fa29549716f78316bf382c8d2c /plugins/setoid_ring | |
| parent | fafd64a1322205c3c4e3cae0680e03ea341b1cd8 (diff) | |
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
Diffstat (limited to 'plugins/setoid_ring')
| -rw-r--r-- | plugins/setoid_ring/newring.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index b6b69ec2d..5556912eb 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -129,8 +129,8 @@ let closed_term_ast l = let l = List.map (fun gr -> ArgArg(Loc.ghost,gr)) l in TacFun([Some(Id.of_string"t")], TacAtom(Loc.ghost,TacExtend(Loc.ghost,"closed_term", - [Genarg.in_gen Genarg.globwit_constr (GVar(Loc.ghost,Id.of_string"t"),None); - Genarg.in_gen (Genarg.wit_list1 Genarg.globwit_ref) l]))) + [Genarg.in_gen (Genarg.glbwit Genarg.wit_constr) (GVar(Loc.ghost,Id.of_string"t"),None); + Genarg.in_gen (Genarg.glbwit (Genarg.wit_list1 Genarg.wit_ref)) l]))) (* let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term" *) |