diff options
author | 2008-03-08 14:52:02 +0000 | |
---|---|---|
committer | 2008-03-08 14:52:02 +0000 | |
commit | 6164aabc75035ca21474b51ceab4e25d47395ff7 (patch) | |
tree | ebbd1dacc3ee8feb9c86a1e8edf6518ae8cf5e86 /toplevel/record.ml | |
parent | 16ae29315ae0f88c4926b97f8fe22bffe65aa3e1 (diff) |
Fix bugs that were reopened due to the change of setoid
implementation. Mostly syntax changes when declaring parametric
relations, but also some declarations were relying on "default"
relations on some carrier. Added a new DefaultRelation type class that
allows to do that, falling back to the last declared Equivalence
relation by default. This will be bound to Add Relation in the next
commit.
Also, move the "left" and "right" notations in Program.Utils to "in_left" and
"in_right" to avoid clashes with existing scripts.
Minor change to record to allow choosing the name of the argument for
the record in projections to avoid possible incompatibilities.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10639 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/record.ml')
-rw-r--r-- | toplevel/record.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/toplevel/record.ml b/toplevel/record.ml index b94dffe1a..b04557304 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -131,15 +131,14 @@ let instantiate_possibly_recursive_type indsp paramdecls fields = substl_rel_context (subst@[mkInd indsp]) fields (* We build projections *) -let declare_projections indsp coers fields = +let declare_projections indsp ?name coers fields = let env = Global.env() in let (mib,mip) = Global.lookup_inductive indsp in let paramdecls = mib.mind_params_ctxt in let r = mkInd indsp in let rp = applist (r, extended_rel_list 0 paramdecls) in let paramargs = extended_rel_list 1 paramdecls in (*def in [[params;x:rp]]*) - let x = Name (next_ident_away mip.mind_typename (ids_of_context (Global.env()))) in - (* Termops.named_hd (Global.env()) r Anonymous *) + let x = match name with Some n -> Name n | None -> Termops.named_hd (Global.env()) r Anonymous in let fields = instantiate_possibly_recursive_type indsp paramdecls fields in let lifted_fields = lift_rel_context 1 fields in let (_,kinds,sp_projs,_) = |