Commit 970eea5e authored by Guillaume Melquiond's avatar Guillaume Melquiond

Allow elision of module substitution right-hand sides.

parent 2f6f8384
......@@ -260,10 +260,15 @@ clone_subst:
single_clone_subst:
| TYPE qualid ty_var* EQUAL ty { CStsym ($2,$3,$5) }
| TYPE qualid { CStsym ($2, [], PTtyapp ($2, [])) }
| CONSTANT qualid EQUAL qualid { CSfsym ($2,$4) }
| CONSTANT qualid { CSfsym ($2,$2) }
| FUNCTION qualid EQUAL qualid { CSfsym ($2,$4) }
| FUNCTION qualid { CSfsym ($2,$2) }
| PREDICATE qualid EQUAL qualid { CSpsym ($2,$4) }
| PREDICATE qualid { CSpsym ($2,$2) }
| VAL qualid EQUAL qualid { CSvsym ($2,$4) }
| VAL qualid { CSvsym ($2,$2) }
| AXIOM qualid { CSaxiom ($2) }
| LEMMA qualid { CSlemma ($2) }
| GOAL qualid { CSgoal ($2) }
......
......@@ -129,14 +129,14 @@ theory Set
axiom Equal_is_eq : forall s1 s2 : set 'a. equal s1 s2 -> s1 = s2
*)
clone export SetGen with type set = set,
predicate mem = mem, lemma extensionality,
constant empty = empty, lemma empty_def,
function add = add, lemma add_def,
function remove = remove, lemma remove_def,
function union = union, lemma union_def,
function inter = inter, lemma inter_def,
function diff = diff, lemma diff_def
clone export SetGen with type set,
predicate mem, lemma extensionality,
constant empty, lemma empty_def,
function add, lemma add_def,
function remove, lemma remove_def,
function union, lemma union_def,
function inter, lemma inter_def,
function diff, lemma diff_def
end
......@@ -165,7 +165,7 @@ theory Fset
type set 'a
val constant empty : set 'a
clone export SetGen with type set = set, function empty = empty
clone export SetGen with type set, function empty
function cardinal (set 'a) : int
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment