diff options
| author | Maxime Dénès | 2017-05-25 11:16:35 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-05-25 11:16:35 +0200 |
| commit | f2fec63025d933f56dabf114a51720b1aae626c1 (patch) | |
| tree | 7f729302601fef48e6c59534a7904c7dfb92df2d /plugins/funind/invfun.ml | |
| parent | 28f8da9489463b166391416de86420c15976522f (diff) | |
| parent | 94e783390ef9ad9d26a54add2287e0a3e58d1b70 (diff) | |
Merge PR#402: Uniform attribute handling in interfaces
Diffstat (limited to 'plugins/funind/invfun.ml')
| -rw-r--r-- | plugins/funind/invfun.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 6c0c28905e..8c972cd7cf 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -30,8 +30,8 @@ module RelDecl = Context.Rel.Declaration let pr_binding prc = function - | loc, NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c) - | loc, AnonHyp n, c -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c) + | loc, (NamedHyp id, c) -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c) + | loc, (AnonHyp n, c) -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c) let pr_bindings prc prlc = function | ImplicitBindings l -> @@ -273,7 +273,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes List.map (fun decl -> List.map - (fun id -> Loc.ghost, IntroNaming (IntroIdentifier id)) + (fun id -> Loc.tag @@ IntroNaming (IntroIdentifier id)) (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum evd (RelDecl.get_type decl))))) ) branches |