diff options
| author | Hugo Herbelin | 2016-12-05 11:57:58 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2017-03-23 22:13:57 +0100 |
| commit | 45a411377244da33111cf5d7002df70de912bc64 (patch) | |
| tree | c01b496bbe54b7299fe8e7cafa279fcc55ddf05b /parsing | |
| parent | 8f5d447769a41cd251701272a6ff71a7a20de658 (diff) | |
Factorizing/unifying code in dealing with binders.
Note: This reveals a little bug yet to fix in g_vernac.ml4. In
Definition f '((x,y):id nat * id nat) '((x',y'):id nat * id nat) := Eval unfold id in x+y = x'+y'.
the "id" are wrongly unfolded and in
Definition f '(x,y) '(x',y') := x+y = x'+y' : Prop.
an unexpected cast remains in the body of f.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 14 |
1 files changed, 10 insertions, 4 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 18807113c9..ba441a662f 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -243,16 +243,22 @@ GEXTEND Gram (* Simple definitions *) def_body: [ [ bl = binders; ":="; red = reduce; c = lconstr -> - let (bl, c) = expand_pattern_binders mkCLambdaN bl c in - (match c with - CCast(_,c, CastConv t) -> DefineBody (bl, red, c, Some t) + if List.exists (function LocalPattern _ -> true | _ -> false) bl + then + (* FIXME: "red" will be applied to types in bl and Cast with remain *) + let c = mkCLambdaN (!@loc) bl c in + DefineBody ([], red, c, None) + else + (match c with + | CCast(_,c, CastConv t) -> DefineBody (bl, red, c, Some t) | _ -> DefineBody (bl, red, c, None)) | bl = binders; ":"; t = lconstr; ":="; red = reduce; c = lconstr -> let ((bl, c), tyo) = if List.exists (function LocalPattern _ -> true | _ -> false) bl then + (* FIXME: "red" will be applied to types in bl and Cast with remain *) let c = CCast (!@loc, c, CastConv t) in - (expand_pattern_binders mkCLambdaN bl c, None) + (([],mkCLambdaN (!@loc) bl c), None) else ((bl, c), Some t) in DefineBody (bl, red, c, tyo) |